ci: bump actions/setup-python from 6.2.0 to 7.0.0 #180
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: validate | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| # Weekly cron (Monday 06:17 UTC): the toolchain surface — apt z3/cvc4, | |
| # opam's newest resolvable rocq/dune/Mathlib caches, GitHub release | |
| # assets — moves under a quiet repo. A scheduled run turns "CI will be | |
| # red on the next push" (the dune-3.24 break sat unnoticed for 72 | |
| # days) into a red badge within a week. Odd minute to avoid the | |
| # top-of-hour queue. | |
| schedule: | |
| - cron: "17 6 * * 1" | |
| # Manual re-run without a push (no-op PRs are not needed to re-validate). | |
| workflow_dispatch: | |
| jobs: | |
| schemas: | |
| runs-on: ubuntu-latest | |
| # timeout-minutes on every job: ~2x the observed wall-clock of the | |
| # last green main run (schemas 10 s, sdk 1m54, cross-platform 2m18, | |
| # lean-bridge 15m09, rocq-bridge 6m20) so a hung solver or a | |
| # runaway Mathlib build fails the job instead of burning the | |
| # 6-hour default. Raise deliberately when a phase adds real work | |
| # (R1's live suite, R0.5's Mathlib bump). | |
| timeout-minutes: 10 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 | |
| with: | |
| python-version: "3.12" | |
| cache: pip | |
| cache-dependency-path: tools/requirements.txt | |
| - name: Install validator deps | |
| run: pip install -r tools/requirements.txt | |
| - name: Validate schemas and reference fixtures | |
| run: python tools/validate.py | |
| - name: Run cross-document soundness checks | |
| run: python tools/check.py | |
| - name: Run cross-doc checker negative tests | |
| run: python tools/test_check.py | |
| # Doc-count gate: every number README's Status section shows is | |
| # printed by tools/status_table.py from the committed JSON/source | |
| # files; the embedded copy must match byte-for-byte. Hand-typed | |
| # counts went stale within weeks every time (retros); this turns | |
| # that into a red schemas job. `--write` refreshes the block. | |
| - name: README status table up to date | |
| run: | | |
| python tools/status_table.py --check | |
| python tools/test_status_table.py | |
| - name: Run trust-gate parser tests (axiom-check C2/C3) | |
| run: python tools/test_check_axioms.py | |
| - name: Cross-canonical hash byte-equivalence (Python side) | |
| # Companion to sdk/test/test_canonical_hash.ml — both run | |
| # against tests/cross_canonical/expected.json so a drift on | |
| # either side surfaces as a failing test, never a silent | |
| # same-pass on a divergent format. | |
| run: python tools/test_canonical_hash.py | |
| # Pure text extraction (no bridge build): fail fast and cheap if the | |
| # Lean and Rocq Alethe walkers drift out of rule-set lockstep. | |
| - name: Check walker rule parity (Lean <-> Rocq) | |
| run: python tools/check_walker_parity.py | |
| - name: Run walker rule-parity tests | |
| run: python tools/test_walker_parity.py | |
| # Static replay-coverage gate (no bridge build, no solver): compare each | |
| # committed corpus trace's rule inventory against the walker's supported | |
| # set, and assert the report matches the committed corpus/coverage.json. | |
| # A coverage change (corpus grew, cvc5 refreshed, walker learned a rule) | |
| # must land as a reviewed diff to coverage.json. | |
| - name: Walker replay coverage (static gate) | |
| run: python tools/check_walker_coverage.py --check | |
| # The generated dynamic-replay theory must be in sync with the corpus. | |
| - name: Walker corpus replay theory up to date | |
| run: python tools/gen_corpus_replay.py --check | |
| # Walker scale profile (structural cost predictors per trace): a | |
| # trace-complexity change -- a refreshed cvc5 emitting a heavier | |
| # proof, or a new goal that balloons the arithmetic-leaf count -- | |
| # must land as a reviewed diff to corpus/profile.json. | |
| - name: Walker scale profile up to date | |
| run: python tools/profile_walker.py --check | |
| - name: Run walker coverage + replay-gen + profile tests | |
| run: | | |
| python tools/test_walker_coverage.py | |
| python tools/test_gen_corpus_replay.py | |
| python tools/test_profile_walker.py | |
| # Property-based fuzz of the resolution clause-algebra (set | |
| # semantics + soundness vs a truth-table oracle): the systematic | |
| # guard for the resolvent computation, including the dedup | |
| # invariant whose absence broke the pigeonhole scale point. Fixed | |
| # seed -> reproducible; the self-test includes a negative control | |
| # proving the suite detects the regression. | |
| - name: Fuzz walker resolution algebra | |
| run: | | |
| python tools/fuzz_resolution.py | |
| python tools/test_fuzz_resolution.py | |
| sdk: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1 | |
| with: | |
| ocaml-compiler: "5.4" | |
| dune-cache: true | |
| - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 | |
| with: | |
| python-version: "3.12" | |
| cache: pip | |
| cache-dependency-path: tools/requirements.txt | |
| - name: Install Python validator deps | |
| run: pip install -r tools/requirements.txt | |
| - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH) | |
| # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune | |
| # language; only `(using rocq 0.11)` parses there. But every | |
| # published rocq-runtime (<= 9.2.0) declares | |
| # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`), | |
| # so a dune-3.24 workspace cannot host the Rocq bridge at all. | |
| # dune-project therefore stays on `(using coq 0.8)` and pins | |
| # `(dune (< 3.24))` in every package. setup-ocaml installs the | |
| # newest dune; pin it here BEFORE the deps so `dune build` parses | |
| # dune-project. (The rocq-bridge job gets the same downgrade for | |
| # free from rocq-runtime's constraint and needs no pin step.) | |
| # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the | |
| # bound, migrate dune-project to `(lang dune 3.24)` + | |
| # `(using rocq 0.11)` and delete this step in all three jobs. | |
| run: opam install -y "dune<3.24" | |
| - name: Install SDK deps | |
| # The opam files (proof_broker.opam, proof_broker_rocq.opam) | |
| # live at repo root after the Phase 1 workspace merge; pre- | |
| # merge this read `./sdk`. Pointing at the .opam file | |
| # directly avoids a directory-scan-relies-on-cwd surprise. | |
| # Retry wrapper: GitHub release-asset fetches (ocaml-syntax- | |
| # shims et al.) return transient 502s under CDN load — a clean | |
| # dep set shouldn't fail a run on a flaky download. 3 attempts, | |
| # 15s backoff. | |
| run: | | |
| n=0 | |
| until opam install -y --deps-only --with-test ./proof_broker.opam; do | |
| n=$((n+1)) | |
| if [ "$n" -ge 3 ]; then echo "opam install failed after $n attempts" >&2; exit 1; fi | |
| echo "opam install attempt $n hit a transient fetch error; retrying in 15s..." >&2 | |
| sleep 15 | |
| done | |
| - name: Build SDK | |
| # `dune build sdk` constrains the build to the SDK subtree — | |
| # rocq-bridge is built in its own job (which installs rocq- | |
| # runtime + cvc5/z3); leaving it out here keeps this job's | |
| # dep surface minimal. | |
| run: opam exec -- dune build sdk | |
| - name: Install Vampire (pinned + checksummed) | |
| # The Vampire adapter's live tests (test_adapter_vampire) | |
| # shell out to the `vampire` binary; absent it they skip and | |
| # the suite still passes, but CI should actually exercise the | |
| # FOF/THF dispatch path, so install a pinned release. Audit | |
| # M8 discipline (mirrors the cvc5 step in the lean-bridge / | |
| # rocq-bridge jobs): pin the version AND verify the archive's | |
| # SHA-256 before it touches the runner so a compromised / | |
| # MITM'd release fails the job instead of silently changing | |
| # the prover. Keep VAMPIRE_VERSION in sync with | |
| # Adapter_vampire.version and examples/manifest-vampire.json. | |
| env: | |
| VAMPIRE_VERSION: "v5.0.1" | |
| VAMPIRE_SHA256: "6ff2f42ea7fb9753ee104efc3e623d5e39443190f7c82a63e1e1517bf9d2cde3" | |
| run: | | |
| curl -sSL "https://github.com/vprover/vampire/releases/download/${VAMPIRE_VERSION}/vampire-Linux-X64.zip" -o /tmp/vampire.zip | |
| echo "${VAMPIRE_SHA256} /tmp/vampire.zip" | sha256sum -c - | |
| unzip -q /tmp/vampire.zip -d /tmp/vampire | |
| sudo install -m 755 /tmp/vampire/vampire /usr/local/bin/vampire | |
| vampire --version | head -1 | |
| - name: Run SDK tests | |
| run: opam exec -- dune runtest sdk | |
| - name: Cross-tool agreement (OCaml round-trip → Python validator) | |
| run: python tools/test_cross_tool.py | |
| - name: FFI shim smoke test (C ↔ OCaml) | |
| run: bash sdk/ffi/test/run.sh | |
| sdk-cross-platform: | |
| # Cross-platform build + install verification. The primary `sdk` | |
| # job above runs on Linux x86 and is the prerequisite for the | |
| # bridge jobs; this matrix is independent — its purpose is to | |
| # surface platform-specific build breakage on macOS / ARM Linux | |
| # before users hit it, and to validate the `(install ...)` stanza | |
| # in sdk/ffi/dune that routes `proof_broker_ffi.so` to the package | |
| # lib directory. First half of the Phase 6 distribution scaffold | |
| # per `RETROSPECTIVES/phase-5.md` carried-forward "Cross-platform | |
| # OCaml runtime distribution". | |
| # | |
| # Audit H5: this job has no `needs:` *out*-edge, but the terminal | |
| # `ci-status` aggregate gate (bottom of file) depends on it, so a | |
| # macOS / ARM failure now DOES block merge — branch protection | |
| # should require only `ci-status`. `fail-fast: false` is kept so | |
| # one platform's failure still lets the others report. If the | |
| # GitHub macOS/ARM runner pool flakiness (see the macos-13 note | |
| # below) becomes a recurring spurious-red problem, the policy | |
| # decision is to move this job out of the `ci-status` needs list | |
| # — not to silently re-hide its failures. | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - os: ubuntu-24.04-arm | |
| label: linux-aarch64 | |
| # macos-14 (Apple Silicon, M1) is the only macOS runner in the | |
| # matrix today. macos-13 (Intel) was dropped after spending 4h | |
| # queued without a runner ever attaching — GitHub Actions' | |
| # Intel-macOS pool is severely backed up since Apple stopped | |
| # selling Intel hardware. The macOS-specific code path the | |
| # matrix exercises (install_name_tool dyld fix in | |
| # sdk/ffi/test/run.sh) is already covered by macos-14; | |
| # re-add macos-13 if Intel macOS becomes a deployment target. | |
| - os: macos-14 | |
| label: macos-aarch64 | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 20 | |
| name: sdk-cross-platform (${{ matrix.label }}) | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1 | |
| with: | |
| ocaml-compiler: "5.4" | |
| dune-cache: true | |
| - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH) | |
| # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune | |
| # language; only `(using rocq 0.11)` parses there. But every | |
| # published rocq-runtime (<= 9.2.0) declares | |
| # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`), | |
| # so a dune-3.24 workspace cannot host the Rocq bridge at all. | |
| # dune-project therefore stays on `(using coq 0.8)` and pins | |
| # `(dune (< 3.24))` in every package. setup-ocaml installs the | |
| # newest dune; pin it here BEFORE the deps so `dune build` parses | |
| # dune-project. (The rocq-bridge job gets the same downgrade for | |
| # free from rocq-runtime's constraint and needs no pin step.) | |
| # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the | |
| # bound, migrate dune-project to `(lang dune 3.24)` + | |
| # `(using rocq 0.11)` and delete this step in all three jobs. | |
| run: opam install -y "dune<3.24" | |
| - name: Install SDK deps | |
| # See retry rationale in the `sdk` job's Install SDK deps step. | |
| run: | | |
| n=0 | |
| until opam install -y --deps-only --with-test ./proof_broker.opam; do | |
| n=$((n+1)) | |
| if [ "$n" -ge 3 ]; then echo "opam install failed after $n attempts" >&2; exit 1; fi | |
| echo "opam install attempt $n hit a transient fetch error; retrying in 15s..." >&2 | |
| sleep 15 | |
| done | |
| - name: Build SDK (incl. install rules so proof_broker.install exists) | |
| # `dune build sdk` alone builds the sdk subtree but doesn't | |
| # generate proof_broker.install. Adding `proof_broker.install` | |
| # to the target list triggers the install-manifest generation, | |
| # but scoping with --only-packages is required: a bare | |
| # workspace target pulls in proof_broker_rocq too, which | |
| # transitively needs coqc (not installed in the matrix; the | |
| # rocq plugin is built only by the dedicated rocq-bridge job). | |
| run: | | |
| opam exec -- dune build --only-packages proof_broker \ | |
| sdk proof_broker.install | |
| - name: Code-sign proof_broker_ffi.so (macOS) | |
| if: runner.os == 'macOS' | |
| # Ad-hoc by default (no secrets needed — runs on every PR/fork); | |
| # Developer ID + hardened runtime + secure timestamp when the | |
| # MACOS_CERT_* / MACOS_SIGN_IDENTITY secrets are provisioned. | |
| # Signing the _build artifact *before* the smoke test and | |
| # `dune install` means every downstream consumer in this job | |
| # exercises a signed library — i.e. CI proves a signed .so | |
| # still dlopen-loads through the C shim, not just that signing | |
| # exits 0. `codesign --verify --strict` inside the script reds | |
| # the job on a broken signature. | |
| # | |
| # Secret gating (audit H5): the signing secrets are only | |
| # injected on `push` (post-merge, trusted ref). On ANY | |
| # `pull_request` — fork or same-repo — the expression resolves | |
| # to '' so the secrets never enter the environment of | |
| # PR-controlled code (macos-sign.sh is editable in the PR). | |
| # PRs therefore always exercise the ad-hoc path; the | |
| # Developer-ID path is validated on the protected branch only. | |
| env: | |
| MACOS_CERT_P12_BASE64: ${{ github.event_name == 'push' && secrets.MACOS_CERT_P12_BASE64 || '' }} | |
| MACOS_CERT_PASSWORD: ${{ github.event_name == 'push' && secrets.MACOS_CERT_PASSWORD || '' }} | |
| MACOS_SIGN_IDENTITY: ${{ github.event_name == 'push' && secrets.MACOS_SIGN_IDENTITY || '' }} | |
| run: bash sdk/ffi/packaging/macos-sign.sh _build/default/sdk/ffi/proof_broker_ffi.so | |
| - name: Run SDK tests | |
| run: opam exec -- dune runtest sdk | |
| - name: FFI shim smoke test (C ↔ OCaml) | |
| run: bash sdk/ffi/test/run.sh | |
| - name: Verify `dune install` lands proof_broker_ffi.so in lib/proof_broker/ | |
| # The install stanza in sdk/ffi/dune is the production-ready | |
| # path that decouples the Lean lakefile from the dev `_build` | |
| # tree. Verify it works on each target platform. | |
| # Same audit-H5 secret gating as the code-sign step: secrets | |
| # only on `push`, never in a pull_request context. | |
| env: | |
| MACOS_CERT_P12_BASE64: ${{ github.event_name == 'push' && secrets.MACOS_CERT_P12_BASE64 || '' }} | |
| MACOS_CERT_PASSWORD: ${{ github.event_name == 'push' && secrets.MACOS_CERT_PASSWORD || '' }} | |
| MACOS_SIGN_IDENTITY: ${{ github.event_name == 'push' && secrets.MACOS_SIGN_IDENTITY || '' }} | |
| run: | | |
| tmp=$(mktemp -d) | |
| opam exec -- dune install --prefix="$tmp" proof_broker | |
| test -f "$tmp/lib/proof_broker/proof_broker_ffi.so" | |
| echo "OK: proof_broker_ffi.so installed at $tmp/lib/proof_broker/" | |
| # The installed copy is what a consumer actually loads. dune | |
| # install copies bytes (signature travels with the Mach-O), | |
| # but re-sign + strict-verify here so the *distributed* | |
| # artifact is independently asserted, not just the _build one. | |
| if [ "$RUNNER_OS" = "macOS" ]; then | |
| bash sdk/ffi/packaging/macos-sign.sh "$tmp/lib/proof_broker/proof_broker_ffi.so" | |
| fi | |
| lean-bridge: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 40 | |
| needs: sdk | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| # Rebuild the OCaml shim because artifacts don't carry between jobs; | |
| # cheap because the dune cache hits and the OCaml part is small. | |
| - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1 | |
| with: | |
| ocaml-compiler: "5.4" | |
| dune-cache: true | |
| # Python is needed for the trust-footprint gate | |
| # (tools/check_axioms.py); the standard library is enough, no | |
| # third-party deps. | |
| - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 | |
| with: | |
| python-version: "3.12" | |
| - name: Install z3 + cvc4 (apt) | |
| # The Lean test suite under Test/Tactic.lean uses | |
| # `proof_broker [z3]`, `proof_broker [cvc4]`, `proof_broker [cvc5]`, | |
| # and `proof_broker_term [...]` style tactics that shell out to | |
| # the actual solver binaries at *compile time* during `lake | |
| # build`. Without these on PATH, the tactic emits an error, | |
| # Lean's error-recovery elaboration leaves a `sorry` in place, | |
| # and every `*_axiom_free` theorem ends up with `sorryAx` in | |
| # its trust footprint — failing the axiom-allowlist gate. | |
| # tier1_lia_axiom_free in particular is pinned to cvc4, gating | |
| # the original Tier 1 Farkas-extraction path. Mirrors the | |
| # rocq-bridge job's installs. | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y z3 cvc4 | |
| cvc4 --version | head -1 | |
| z3 --version | |
| - name: Install cvc5 (GitHub static release) | |
| # Audit M8: the cvc5 binary establishes the Lean-side trust | |
| # footprint (cert-gated tactics shell out to it at lake-build | |
| # time), so it must not be fetched unauthenticated. Pin the | |
| # version AND verify the archive's SHA-256 before it touches | |
| # the runner — a compromised/MITM'd release fails the job | |
| # instead of silently changing the solver. | |
| env: | |
| CVC5_VERSION: "1.3.0" | |
| CVC5_SHA256: "1e5a30c66f8fc3b65ddac69a3ac299bf03914cc58fc562e0ab6c730bf6bbfe6f" | |
| run: | | |
| curl -sSL "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-x86_64-static.zip" -o /tmp/cvc5.zip | |
| echo "${CVC5_SHA256} /tmp/cvc5.zip" | sha256sum -c - | |
| unzip -q /tmp/cvc5.zip -d /tmp/cvc5 | |
| sudo install -m 755 /tmp/cvc5/cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin/cvc5 | |
| cvc5 --version | |
| - name: Install Vampire (pinned + checksummed) | |
| # Phase-3 M3: Test/TacticMathlib.lean's | |
| # hol_function_composition_axiom_free reifies a higher-order | |
| # goal, dispatches to Vampire at lake-build time, and closes | |
| # the goal gated on the re-verified Tier-3 tstp cert. Vampire | |
| # is therefore part of the Lean-side trust footprint here, | |
| # same as cvc5 — pin + SHA-256-verify before use (audit M8; | |
| # same archive/hash as the `sdk` job, keep in sync on a bump). | |
| env: | |
| VAMPIRE_VERSION: "v5.0.1" | |
| VAMPIRE_SHA256: "6ff2f42ea7fb9753ee104efc3e623d5e39443190f7c82a63e1e1517bf9d2cde3" | |
| run: | | |
| curl -sSL "https://github.com/vprover/vampire/releases/download/${VAMPIRE_VERSION}/vampire-Linux-X64.zip" -o /tmp/vampire.zip | |
| echo "${VAMPIRE_SHA256} /tmp/vampire.zip" | sha256sum -c - | |
| unzip -q /tmp/vampire.zip -d /tmp/vampire | |
| sudo install -m 755 /tmp/vampire/vampire /usr/local/bin/vampire | |
| vampire --version | head -1 | |
| - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH) | |
| # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune | |
| # language; only `(using rocq 0.11)` parses there. But every | |
| # published rocq-runtime (<= 9.2.0) declares | |
| # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`), | |
| # so a dune-3.24 workspace cannot host the Rocq bridge at all. | |
| # dune-project therefore stays on `(using coq 0.8)` and pins | |
| # `(dune (< 3.24))` in every package. setup-ocaml installs the | |
| # newest dune; pin it here BEFORE the deps so `dune build` parses | |
| # dune-project. (The rocq-bridge job gets the same downgrade for | |
| # free from rocq-runtime's constraint and needs no pin step.) | |
| # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the | |
| # bound, migrate dune-project to `(lang dune 3.24)` + | |
| # `(using rocq 0.11)` and delete this step in all three jobs. | |
| run: opam install -y "dune<3.24" | |
| - name: Install SDK deps | |
| # See retry rationale in the `sdk` job's Install SDK deps step. | |
| run: | | |
| n=0 | |
| until opam install -y --deps-only --with-test ./proof_broker.opam; do | |
| n=$((n+1)) | |
| if [ "$n" -ge 3 ]; then echo "opam install failed after $n attempts" >&2; exit 1; fi | |
| echo "opam install attempt $n hit a transient fetch error; retrying in 15s..." >&2 | |
| sleep 15 | |
| done | |
| - name: Build SDK shared object | |
| run: opam exec -- dune build sdk | |
| - name: Install elan (Lean toolchain manager) | |
| # Audit M8: was `curl | run` of elan-init.sh from the moving | |
| # `master` ref (uncheckable, MITM-able). Pin to a release tag | |
| # — a tagged ref is immutable, so the installer can be | |
| # SHA-256-verified before execution. Bump ELAN_VERSION and | |
| # ELAN_INIT_SHA256 together. | |
| env: | |
| ELAN_VERSION: "v4.2.1" | |
| ELAN_INIT_SHA256: "4bacca9502cb89736fe63d2685abc2947cfbf34dc87673504f1bb4c43eda9264" | |
| run: | | |
| curl -sSf "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh" -o elan-init.sh | |
| echo "${ELAN_INIT_SHA256} elan-init.sh" | sha256sum -c - | |
| chmod +x elan-init.sh | |
| ./elan-init.sh -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Build Lean bridge (auto-installs toolchain via lean-toolchain) | |
| working-directory: lean-bridge | |
| # `set -o pipefail` is REQUIRED: GitHub Actions runs `run:` as | |
| # `bash -e` *without* pipefail, so `lake build | tee` would take | |
| # tee's exit code (always 0) and a failing build — including the | |
| # "solver missing → Lean error-recovery inserts `sorry`" mode the | |
| # very next trust-footprint gate exists to catch — would pass CI | |
| # silently. The tee is still needed so check_axioms.py can read | |
| # the captured #print axioms output. Mirrors the rocq-bridge | |
| # job's explicit failure propagation. | |
| run: | | |
| set -o pipefail | |
| lake build 2>&1 | tee ../lake_build.log | |
| - name: Trust-footprint gate (axiom allowlist, Lean side) | |
| run: python tools/check_axioms.py --build-output lake_build.log --bridge lean | |
| - name: Run Lean ↔ C ↔ OCaml round-trip | |
| working-directory: lean-bridge | |
| run: lake exe roundtripTest | |
| rocq-bridge: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| needs: sdk | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1 | |
| with: | |
| ocaml-compiler: "5.4" | |
| dune-cache: true | |
| - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 | |
| with: | |
| python-version: "3.12" | |
| - name: Install z3 (apt) | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y z3 cvc4 | |
| cvc4 --version | head -1 | |
| z3 --version | |
| - name: Install cvc5 (GitHub static release) | |
| # Pinned static-build release from the cvc5/cvc5 repo. The | |
| # SDK's manifest-cvc5.json declares adapter_version 1.3.3; | |
| # the cert.backend.version field records whatever the | |
| # binary reports at dispatch time — the verifier doesn't | |
| # compare those, so a CI-pinned 1.3.0 satisfies the gate | |
| # against a manifest pinned to 1.3.3. | |
| # Audit M8: SHA-256-verified before use (same archive/hash as | |
| # the lean-bridge job — keep both in sync on a version bump). | |
| env: | |
| CVC5_VERSION: "1.3.0" | |
| CVC5_SHA256: "1e5a30c66f8fc3b65ddac69a3ac299bf03914cc58fc562e0ab6c730bf6bbfe6f" | |
| run: | | |
| curl -sSL "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-x86_64-static.zip" -o /tmp/cvc5.zip | |
| echo "${CVC5_SHA256} /tmp/cvc5.zip" | sha256sum -c - | |
| unzip -q /tmp/cvc5.zip -d /tmp/cvc5 | |
| sudo install -m 755 /tmp/cvc5/cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin/cvc5 | |
| cvc5 --version | |
| - name: Install Vampire (pinned + checksummed) | |
| # Phase-3 #1 Rocq parity (rocq-bridge/hammer/Test.v's | |
| # pb_hol_function_composition_axiom_free): the HOL test | |
| # reifies a higher-order goal, dispatches to Vampire at | |
| # build time (THF), and closes via coq-hammer's hauto. | |
| # Pinned + SHA-256-verified, same archive/hash as the | |
| # sdk + lean-bridge jobs — keep in sync on a version bump. | |
| env: | |
| VAMPIRE_VERSION: "v5.0.1" | |
| VAMPIRE_SHA256: "6ff2f42ea7fb9753ee104efc3e623d5e39443190f7c82a63e1e1517bf9d2cde3" | |
| run: | | |
| curl -sSL "https://github.com/vprover/vampire/releases/download/${VAMPIRE_VERSION}/vampire-Linux-X64.zip" -o /tmp/vampire.zip | |
| echo "${VAMPIRE_SHA256} /tmp/vampire.zip" | sha256sum -c - | |
| unzip -q /tmp/vampire.zip -d /tmp/vampire | |
| sudo install -m 755 /tmp/vampire/vampire /usr/local/bin/vampire | |
| vampire --version | head -1 | |
| - name: Add coq-released opam repository | |
| # [coq-hammer-tactics] (the opt-in HOL closer's dep) lives | |
| # in the coq-released repo (https://coq.inria.fr/opam/released), | |
| # not the default opam-repository at opam.ocaml.org. | |
| # rocq-runtime / coq-core / coq-stdlib are in the default | |
| # repo so the original rocq-bridge job worked without this, | |
| # but coq-hammer-* has not been migrated. Adding it here | |
| # (rocq-bridge job only) keeps the dep surface localized — | |
| # the SDK and Lean-bridge jobs don't need it. | |
| run: | | |
| opam repository add coq-released https://coq.inria.fr/opam/released | |
| opam update | |
| - name: Install SDK + rocq-bridge deps | |
| # No explicit `dune<3.24` pin here: rocq-runtime's own | |
| # `dune {>= "3.8" & < "3.24"}` constraint makes the solver | |
| # downgrade dune (WATCH(rocq-dune-3.24), see the pin step in | |
| # the sdk / sdk-cross-platform / lean-bridge jobs). | |
| # proof_broker_rocq pulls in rocq-runtime (>= 9.0); proof_broker | |
| # pulls the OCaml SDK deps; proof_broker_rocq_hammer | |
| # (Phase-3 #1 Rocq parity, opt-in HOL closer via hauto) | |
| # pulls coq-hammer-tactics (the lighter reconstruction-only | |
| # half of coq-hammer — we don't need the ATP-prediction | |
| # layer here; the broker has already chosen the cert). | |
| # All opam files at repo root. | |
| # See retry rationale in the `sdk` job's Install SDK deps step. | |
| run: | | |
| n=0 | |
| until opam install -y --deps-only --with-test ./proof_broker.opam ./proof_broker_rocq.opam ./proof_broker_rocq_hammer.opam; do | |
| n=$((n+1)) | |
| if [ "$n" -ge 3 ]; then echo "opam install failed after $n attempts" >&2; exit 1; fi | |
| echo "opam install attempt $n hit a transient fetch error; retrying in 15s..." >&2 | |
| sleep 15 | |
| done | |
| - name: Build SDK + rocq-bridge | |
| # dune build with no path scope builds everything reachable | |
| # from the workspace root; for this job that's the SDK, the | |
| # core rocq-bridge plugin + theories, and the opt-in | |
| # rocq-bridge/hammer theory (which the Phase-3 HOL test | |
| # in rocq-bridge/hammer/Test.v depends on). Capture | |
| # stdout+stderr so the trust-footprint gate can parse the | |
| # Print Assumptions output of every .v file. Each .v file is | |
| # a separate dune action whose output dune truncates if it | |
| # grows too large (head+tail kept, middle dropped) — so a | |
| # single test that prints a very large proof term must live | |
| # in its own file to avoid truncating sibling tests' Print | |
| # Assumptions out of the log (see theories/TestSnapshot.v). | |
| run: opam exec -- dune build > rocq_build.log 2>&1 || (cat rocq_build.log; exit 1) | |
| - name: Trust-footprint gate (axiom allowlist, Rocq side) | |
| run: python tools/check_axioms.py --build-output rocq_build.log --bridge rocq | |
| # Live-drift check (the "Both"-model live half): re-run the corpus | |
| # generator against THIS job's cvc5 and compare to the committed | |
| # fixtures. BLOCKING: the CI-pinned static cvc5 1.3.0 release has been | |
| # confirmed to format proofs byte-identically to the committed traces | |
| # (which were minted locally), so any diff here is a real drift — a | |
| # cvc5 bump, a corpus_gen change, or a stale fixture — and must fail. | |
| # If you intentionally change cvc5 output or the corpus, re-run | |
| # `dune exec sdk/bin/corpus_gen.exe -- corpus` and commit the result. | |
| # The deterministic gates above (static coverage, CorpusReplay.v | |
| # compilation in `dune build`) do not depend on this step. | |
| - name: Walker corpus live-drift | |
| run: | | |
| opam exec -- dune exec sdk/bin/corpus_gen.exe -- corpus | |
| git diff --exit-code -- corpus/ \ | |
| || { echo "::error::cvc5 trace output drifted from committed corpus fixtures; re-run 'dune exec sdk/bin/corpus_gen.exe -- corpus' and commit the regenerated traces (or pin the cvc5 version that produced them)."; exit 1; } | |
| # Audit H5: single aggregate status. Before this, every job was an | |
| # independent check and `sdk-cross-platform` had no downstream, so | |
| # branch protection had to enumerate each job by name and a new or | |
| # cross-platform job was unprotected by default. `ci-status` depends | |
| # on every job and fails unless all concluded `success`, so branch | |
| # protection only needs to require this one check; nothing can slip | |
| # through by being added without updating protection rules. | |
| ci-status: | |
| name: ci-status | |
| if: ${{ always() }} | |
| needs: [schemas, sdk, sdk-cross-platform, lean-bridge, rocq-bridge] | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Require every required job to have succeeded | |
| run: | | |
| # GitHub expression string literals MUST be single-quoted | |
| # (double quotes are a workflow-parse error → 0-job failure). | |
| # Single-quote the separator inside the expression, and use | |
| # bash double-quotes for the assignment so the two don't clash. | |
| results="${{ join(needs.*.result, ' ') }}" | |
| echo "dependency results: ${results}" | |
| ok=1 | |
| for r in ${results}; do | |
| if [ "${r}" != "success" ]; then | |
| echo "::error::a required job concluded '${r}'" | |
| ok=0 | |
| fi | |
| done | |
| if [ "${ok}" -ne 1 ]; then | |
| echo "ci-status: one or more required jobs did not succeed" >&2 | |
| exit 1 | |
| fi | |
| echo "ci-status: all required jobs succeeded" |