Skip to content

Commit 0f0f817

Browse files
committed
chapel: drop extern "C" { } wrapper from chapel_ffi_exports
Companion to the chapel-ci.yml Zig-version bump in the previous commit on this branch. The wrapper required Chapel to be built with LLVM + clang headers, which the `chapel-2.3.0-1.ubuntu24.amd64.deb` is not — every Chapel-CI run since 2026-04-20 hit: chapel_ffi_exports.chpl:29: syntax error: near '{' The 35 prover-id / category-id `c_int` constants are also `#define`d on the C side in `src/zig_ffi/chapel_ffi_exports.h`, which is the canonical copy any non-Chapel consumer reads. Dropping the wrapper and keeping the declarations at module scope keeps the Chapel side working without the LLVM dependency. Added an in-file comment block above the constants pointing to the C header as the source of truth for non-Chapel consumers (so the two copies don't drift silently).
1 parent 2d9944f commit 0f0f817

1 file changed

Lines changed: 57 additions & 51 deletions

File tree

src/chapel/chapel_ffi_exports.chpl

Lines changed: 57 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -26,57 +26,63 @@ extern record CProofResult {
2626
// Prover ID constants (match ProverInfo.id and Zig ProverKind enum)
2727
// ---------------------------------------------------------------------------
2828

29-
extern "C" {
30-
// Interactive proof assistants
31-
const PROVER_AGDA: c_int = 0;
32-
const PROVER_COQ: c_int = 1;
33-
const PROVER_LEAN: c_int = 2;
34-
const PROVER_ISABELLE: c_int = 3;
35-
const PROVER_IDRIS2: c_int = 4;
36-
const PROVER_FSTAR: c_int = 5;
37-
const PROVER_HOL4: c_int = 6;
38-
const PROVER_HOLLIGHT: c_int = 7;
39-
const PROVER_NUPRL: c_int = 8;
40-
const PROVER_MINLOG: c_int = 9;
41-
42-
// SMT solvers
43-
const PROVER_Z3: c_int = 10;
44-
const PROVER_CVC5: c_int = 11;
45-
const PROVER_ALTERGO: c_int = 12;
46-
47-
// First-order ATPs
48-
const PROVER_VAMPIRE: c_int = 13;
49-
const PROVER_EPROVER: c_int = 14;
50-
const PROVER_SPASS: c_int = 15;
51-
52-
// Declarative provers
53-
const PROVER_METAMATH: c_int = 16;
54-
const PROVER_MIZAR: c_int = 17;
55-
const PROVER_PVS: c_int = 18;
56-
const PROVER_ACL2: c_int = 19;
57-
const PROVER_TLAPS: c_int = 20;
58-
const PROVER_TWELF: c_int = 21;
59-
const PROVER_IMANDRA: c_int = 22;
60-
61-
// Auto-active verifiers
62-
const PROVER_DAFNY: c_int = 23;
63-
const PROVER_WHY3: c_int = 24;
64-
65-
// Constraint solvers
66-
const PROVER_GLPK: c_int = 25;
67-
const PROVER_SCIP: c_int = 26;
68-
const PROVER_MINIZINC: c_int = 27;
69-
const PROVER_CHUFFED: c_int = 28;
70-
const PROVER_ORTOOLS: c_int = 29;
71-
72-
// Category constants
73-
const CATEGORY_INTERACTIVE: c_int = 0;
74-
const CATEGORY_SMT: c_int = 1;
75-
const CATEGORY_ATP: c_int = 2;
76-
const CATEGORY_DECLARATIVE: c_int = 3;
77-
const CATEGORY_AUTOACTIVE: c_int = 4;
78-
const CATEGORY_CONSTRAINT: c_int = 5;
79-
}
29+
// (Was originally `extern "C" { ... }`, but Chapel's extern-blocks feature
30+
// requires a Chapel install built with LLVM + clang headers; the official
31+
// `chapel-2.3.0-1.ubuntu24.amd64.deb` used in `chapel-ci.yml` is not. The
32+
// canonical C-visible copy lives in `src/zig_ffi/chapel_ffi_exports.h`
33+
// (`#define PROVER_AGDA 0`…), which is what every non-Chapel consumer
34+
// reads; the constants below only need module-level scope inside Chapel.
35+
// Keep the two copies in sync if values change.)
36+
37+
// Interactive proof assistants
38+
const PROVER_AGDA: c_int = 0;
39+
const PROVER_COQ: c_int = 1;
40+
const PROVER_LEAN: c_int = 2;
41+
const PROVER_ISABELLE: c_int = 3;
42+
const PROVER_IDRIS2: c_int = 4;
43+
const PROVER_FSTAR: c_int = 5;
44+
const PROVER_HOL4: c_int = 6;
45+
const PROVER_HOLLIGHT: c_int = 7;
46+
const PROVER_NUPRL: c_int = 8;
47+
const PROVER_MINLOG: c_int = 9;
48+
49+
// SMT solvers
50+
const PROVER_Z3: c_int = 10;
51+
const PROVER_CVC5: c_int = 11;
52+
const PROVER_ALTERGO: c_int = 12;
53+
54+
// First-order ATPs
55+
const PROVER_VAMPIRE: c_int = 13;
56+
const PROVER_EPROVER: c_int = 14;
57+
const PROVER_SPASS: c_int = 15;
58+
59+
// Declarative provers
60+
const PROVER_METAMATH: c_int = 16;
61+
const PROVER_MIZAR: c_int = 17;
62+
const PROVER_PVS: c_int = 18;
63+
const PROVER_ACL2: c_int = 19;
64+
const PROVER_TLAPS: c_int = 20;
65+
const PROVER_TWELF: c_int = 21;
66+
const PROVER_IMANDRA: c_int = 22;
67+
68+
// Auto-active verifiers
69+
const PROVER_DAFNY: c_int = 23;
70+
const PROVER_WHY3: c_int = 24;
71+
72+
// Constraint solvers
73+
const PROVER_GLPK: c_int = 25;
74+
const PROVER_SCIP: c_int = 26;
75+
const PROVER_MINIZINC: c_int = 27;
76+
const PROVER_CHUFFED: c_int = 28;
77+
const PROVER_ORTOOLS: c_int = 29;
78+
79+
// Category constants
80+
const CATEGORY_INTERACTIVE: c_int = 0;
81+
const CATEGORY_SMT: c_int = 1;
82+
const CATEGORY_ATP: c_int = 2;
83+
const CATEGORY_DECLARATIVE: c_int = 3;
84+
const CATEGORY_AUTOACTIVE: c_int = 4;
85+
const CATEGORY_CONSTRAINT: c_int = 5;
8086

8187
// ---------------------------------------------------------------------------
8288
// Helpers

0 commit comments

Comments
 (0)