aver proof --minimize: collapse each proof portfolio to its proven branch #401
Workflow file for this run
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: Proof | |
| # Nightly proof-export gate. `tests/proof_spec.rs` emits Lean | |
| # (`aver proof <example> --target lean` → `lake build`) and Dafny | |
| # (`aver proof --backend dafny` → `dafny verify`) on the real | |
| # `examples/formal/` corpus. The job installs both toolchains and | |
| # runs the same `cargo test --test proof_spec` invocation — the | |
| # Dafny arm is conditional on `dafny --version` succeeding, so | |
| # whether we install it here is the only thing standing between | |
| # "tested" and "silently skipped". | |
| # | |
| # Runs per-PR AND nightly. A proof-codegen / proof-metric drift — | |
| # e.g. the platform-sensitive quicksort Dafny error count (#342) — | |
| # is caught at PR time, not only on the next morning's nightly. The | |
| # per-PR run pays the Lean + Dafny toolchain install up front (the | |
| # reason this was nightly-only before); the nightly stays to verify | |
| # the tip of main against toolchain / Z3-image bumps no PR touches. | |
| on: | |
| # Per-PR + main-push so a proof-codegen / proof-metric drift is | |
| # caught at PR time, same convention as `ci.yml`. | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| schedule: | |
| # 03:00 UTC daily — still runs against the tip of main (catches | |
| # toolchain / Z3-image bumps that no PR touches), same as fuzz | |
| # nightly. | |
| - cron: '0 3 * * *' | |
| workflow_dispatch: | |
| env: | |
| CARGO_TERM_COLOR: always | |
| jobs: | |
| proof-export: | |
| name: Proof Export (Lean + Dafny) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - uses: Swatinem/rust-cache@v2 | |
| - name: Install Lean (via elan) | |
| # Elan with a real default toolchain — `--default-toolchain none` | |
| # leaves `lake` as a wrapper that errors on every call because | |
| # it has no toolchain to delegate to (works for a project dir | |
| # with its own `lean-toolchain` file, broken for the upfront | |
| # `lake --version` sanity check). Pinning `stable` makes the | |
| # bare-PATH lake binary executable; emitted proof projects with | |
| # a different `lean-toolchain` still trigger elan to fetch the | |
| # matching version on first `lake build`. | |
| run: | | |
| curl -sSfL --retry 6 --retry-all-errors --retry-delay 15 --connect-timeout 30 \ | |
| https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | |
| | sh -s -- -y --default-toolchain stable | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Verify `lake` reachable | |
| # The first lake/lean invocation lazily fetches the pinned toolchain | |
| # from releases.lean-lang.org; that download has no built-in retry and | |
| # times out on transient network blips (the same failure mode the | |
| # Dafny arm already hardens against with `curl --retry`). Retry the | |
| # toolchain materialization a few times before failing the job. | |
| run: | | |
| for attempt in 1 2 3 4 5 6; do | |
| if lake --version; then exit 0; fi | |
| echo "::warning::lake/toolchain fetch failed (attempt ${attempt}/6); retrying in 15s" | |
| sleep 15 | |
| done | |
| echo "::error::lake unreachable after 6 attempts (toolchain download)" | |
| exit 1 | |
| - name: Install Dafny | |
| # Manual download of the self-contained (62 MB — bundles its own | |
| # .NET runtime and Z3) Dafny release zip, replacing | |
| # dafny-lang/setup-dafny-action. Two reasons: | |
| # 1. Robustness. The action's internal 3x retry gave up after | |
| # ~40s on a transient GitHub-releases CDN 504 and failed the | |
| # nightly; `curl --retry 6 --retry-all-errors` rides a | |
| # multi-minute CDN blip instead. | |
| # 2. Node-20 EOL. The action is pinned at v1.9.1 (no newer | |
| # release) and its internal setup-node@v4 / setup-dotnet@v4 | |
| # are Node-20 only — GitHub force-migrates those to Node-24 | |
| # on 2026-06-16 and removes Node-20 on 2026-09-16. A self- | |
| # contained zip needs no dotnet, so a plain download + PATH | |
| # sidesteps the whole chain. | |
| # The next step double-checks the install via `dafny --version` | |
| # (which `tests/proof_spec.rs` also gates the Dafny arms on). Keep | |
| # the version in lockstep with the macOS Homebrew Dafny local | |
| # contributors use so `cargo test --test proof_spec` behaves | |
| # identically dev + CI (4.11.0 closes quicksort + rle within the | |
| # 5-budget where 4.9.0 left 2 undischarged). | |
| env: | |
| DAFNY_VERSION: '4.11.0' | |
| run: | | |
| set -euo pipefail | |
| url="https://github.com/dafny-lang/dafny/releases/download/v${DAFNY_VERSION}/dafny-${DAFNY_VERSION}-x64-ubuntu-22.04.zip" | |
| curl -fSL --retry 6 --retry-all-errors --retry-delay 15 --connect-timeout 30 -o /tmp/dafny.zip "$url" | |
| unzip -q /tmp/dafny.zip -d "$HOME/dafny-install" | |
| dafny_dir="$(dirname "$(find "$HOME/dafny-install" -name dafny -type f | head -1)")" | |
| chmod +x "$dafny_dir/dafny" || true | |
| echo "$dafny_dir" >> "$GITHUB_PATH" | |
| - name: Verify `dafny` reachable | |
| run: dafny --version | |
| - name: Run proof-export tests | |
| # Restricting to the proof_spec target keeps this job short | |
| # (no overlap with the lib / wasm / bench jobs). Lean and | |
| # Dafny arms are interleaved inside individual #[test] fns; | |
| # the test harness picks whichever toolchains are on PATH. | |
| run: cargo test -p aver-lang --test proof_spec |