Symptom
Test Suite, Code Coverage, MVP Smoke, and Julia Integration fail on every PR (observed on #73, not introduced by it — present on origin/main) with:
warning: echidna@2.1.0: FLINT not found via pkg-config — trying bare -lflint.
error: rust-lld: error: unable to find library -lflint
error: could not compile `echidna` (lib test) due to 1 previous error
Root cause (corrected)
build.rs correctly gates the -lflint link behind #[cfg(feature = "flint")] — it is not unconditional.
The real cause is .github/workflows/rust-ci.yml, which runs everything with --all-features (lines 49, 52, 55, 136, 205):
cargo clippy --all-targets --all-features -- -D warnings
cargo test --lib --all-features
cargo test --test integration_tests --all-features
cargo doc --no-deps --all-features
cargo check --all-features
--all-features force-enables flint, spark, and chapel — all deliberately opt-in, system-library-dependent features (per Cargo.toml: FLINT = system libflint LGPL-3; SPARK = GNAT/libechidna_spark; chapel = Zig FFI lib). The default GitHub runner has none of these, so the link fails (flint first, by link order; spark/chapel would fail too).
These features each already have their own dedicated CI: chapel-ci.yml, the SPARK Theatre Gate (#84), live-provers.yml. The default rust-ci.yml should exercise only the pure-Rust feature set.
Fix (dedicated PR, off main)
In rust-ci.yml, replace --all-features with the safe pure-Rust optional set --features verisim for the clippy / unit-test / integration-test / doc / MSRV steps. (verisim is the only optional feature with no system dependency; live-provers ⊇ verisim.) flint/spark/chapel stay covered by their dedicated workflows.
Why baseline, not a PR defect
Present on origin/main; independent of any PR diff. Per estate guardrail (baseline-rot ≠ PR-defect): fix here in a dedicated PR, then blocked PRs (e.g. #73) pick it up on their next main merge. Distinct from the CI-infra jam #77.
Symptom
Test Suite,Code Coverage,MVP Smoke, andJulia Integrationfail on every PR (observed on #73, not introduced by it — present onorigin/main) with:Root cause (corrected)
build.rscorrectly gates the-lflintlink behind#[cfg(feature = "flint")]— it is not unconditional.The real cause is
.github/workflows/rust-ci.yml, which runs everything with--all-features(lines 49, 52, 55, 136, 205):--all-featuresforce-enablesflint,spark, andchapel— all deliberately opt-in, system-library-dependent features (perCargo.toml: FLINT = system libflint LGPL-3; SPARK = GNAT/libechidna_spark; chapel = Zig FFI lib). The default GitHub runner has none of these, so the link fails (flint first, by link order; spark/chapel would fail too).These features each already have their own dedicated CI:
chapel-ci.yml, the SPARK Theatre Gate (#84),live-provers.yml. The defaultrust-ci.ymlshould exercise only the pure-Rust feature set.Fix (dedicated PR, off
main)In
rust-ci.yml, replace--all-featureswith the safe pure-Rust optional set--features verisimfor the clippy / unit-test / integration-test / doc / MSRV steps. (verisimis the only optional feature with no system dependency;live-provers⊇verisim.)flint/spark/chapelstay covered by their dedicated workflows.Why baseline, not a PR defect
Present on
origin/main; independent of any PR diff. Per estate guardrail (baseline-rot ≠ PR-defect): fix here in a dedicated PR, then blocked PRs (e.g. #73) pick it up on their nextmainmerge. Distinct from the CI-infra jam #77.