Skip to content

Commit f8511a4

Browse files
ci(chapel): unblock Compile Chapel Metalayer + Build & Test Zig FFI Bridge (#131)
## Summary Fixes two pre-existing, independent breakages that have kept `Chapel Accelerator CI` red on every run since it was first authored (2026-04-20, commit e44815a) — zero successes in the 100-run history. | Job | Symptom | Root cause | Fix | |---|---|---|---| | `Compile Chapel Metalayer` | `chapel_ffi_exports.chpl:29: syntax error: near '{'` (cascading into parallel_proof_search.chpl) | `extern \"C\" { ... }` is Chapel's "extern blocks" feature, requiring Chapel built with LLVM + clang headers. The official `chapel-2.3.0-1.ubuntu24.amd64.deb` is not. | Drop the wrapper. The 35 prover-id / category-id `c_int` constants are also `#define`d in `src/zig_ffi/chapel_ffi_exports.h` — that's the canonical source for any non-Chapel consumer. The Chapel copies only need module-level scope. | | `Build & Test Zig FFI Bridge` | `build.zig:23: no field or member function named 'addLibrary' in 'Build'` | `build.zig` line 1 declares "Compatible with Zig 0.14+/0.15+" and uses the unified `Build.addLibrary` API. Workflow pinned `mlugg/setup-zig@… with: version: 0.13.0`. | Bump the two `version: 0.13.0` lines in chapel-ci.yml to `0.14.0` (matches what build.zig declares). | ## Test plan - [ ] CI: `Compile Chapel Metalayer` returns success on this branch. - [ ] CI: `Build & Test Zig FFI Bridge` returns success on this branch. - [ ] CI: `Rust Build with Chapel Feature` (Job 3) actually runs (was previously skipped because Job 2 failed). ## Note on scope None of these are required checks; this PR doesn't unblock anything blocking the merge queue. It makes Chapel L2.1 actually CI-verifiable for the first time — `handover/TODO.md`'s "L2.1 ✅ Done" status was based on local builds only. Surfaced during the 2026-05-30 dependabot-deadlock triage (alongside PR #128 + PR #130).
1 parent f8c6955 commit f8511a4

2 files changed

Lines changed: 59 additions & 53 deletions

File tree

.github/workflows/chapel-ci.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ jobs:
8686
- name: Install Zig
8787
uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
8888
with:
89-
version: 0.13.0
89+
version: 0.14.0
9090

9191
- name: Build Zig FFI library (with Chapel stubs)
9292
run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe
@@ -151,7 +151,7 @@ jobs:
151151
- name: Install Zig
152152
uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
153153
with:
154-
version: 0.13.0
154+
version: 0.14.0
155155

156156
- name: Install Rust
157157
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable

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)