Repository navigation
[feat] Modularize proof reconstruction interface and support CPC format from cvc5 #86
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: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| # A push that supersedes an in-flight run cancels it; the suite spawns real | |
| # solver processes, so overlapping runs are worth avoiding. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| # The suite runs a solver per `crush` call under a wall-clock timeout, so it is | |
| # slower than a pure compile. This is a ceiling, not an expectation. | |
| timeout-minutes: 45 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # Pinned rather than floating: the suite's `#guard_msgs` expectations include | |
| # solver-dependent text, so an unannounced solver upgrade can turn a green | |
| # build red for reasons unrelated to a code change. Bump deliberately. | |
| - name: Install z3 | |
| run: | | |
| set -euo pipefail | |
| # 4.15 is the floor: the translator emits the standard SMT-LIB BV→Int | |
| # conversions `sbv_to_int` / `bv2nat` (for `BitVec.toInt`/`toNat`), and | |
| # older z3 (≤4.13) rejects `sbv_to_int` as an unknown constant, failing | |
| # the BitVec tests. The glibc-2.39 asset matches ubuntu-latest (24.04). | |
| Z3_VERSION=5.1.0 | |
| Z3_DIR="z3-${Z3_VERSION}-x64-glibc-2.39" | |
| curl -sSfL -o z3.zip \ | |
| "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/${Z3_DIR}.zip" | |
| unzip -q z3.zip | |
| sudo install -m755 "${Z3_DIR}/bin/z3" /usr/local/bin/z3 | |
| z3 --version | |
| # cvc5 is needed for the `native` higher-order mode, which gates on it (z3 | |
| # ignores the `HO_` logic prefix and then fails on the function sorts), and for | |
| # Alethe proof replay. The version floor is 1.3.x: 1.2.0 rejects | |
| # `--proof-format-mode=alethe` as experimental, and forcing it through with | |
| # `--proof-alethe-experimental` emits malformed Alethe (clauses printed as bare | |
| # integers), so replay must decline. See `Crush/Solver/Process.lean`. | |
| - name: Install cvc5 | |
| run: | | |
| set -euo pipefail | |
| CVC5_VERSION=1.3.4 | |
| curl -sSfL -o cvc5.zip \ | |
| "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-x86_64-static.zip" | |
| unzip -q cvc5.zip | |
| sudo install -m755 cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin/cvc5 | |
| cvc5 --version | head -1 | |
| - name: Install Lean toolchain | |
| run: | | |
| set -euo pipefail | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | |
| -o elan-init.sh | |
| sh elan-init.sh -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| # Keyed on both package manifests: a toolchain bump or dependency change must | |
| # not silently reuse stale artifacts. Mathlib's own oleans (~6.6 GB) are | |
| # deliberately excluded; the optional suite downloads them from Mathlib's CDN. | |
| - name: Cache build artifacts | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build | |
| MathlibTest/.lake/build | |
| .lake/packages/batteries | |
| .lake/packages/aesop | |
| .lake/packages/Qq | |
| .lake/packages/importGraph | |
| .lake/packages/proofwidgets | |
| .lake/packages/LeanSearchClient | |
| .lake/packages/plausible | |
| .lake/packages/Cli | |
| key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ hashFiles('MathlibTest/lake-manifest.json') }} | |
| restore-keys: lake-${{ runner.os }}- | |
| - name: Build library | |
| run: lake build | |
| # The core suite runs before Mathlib is fetched, pinning that the root package | |
| # and all ordinary tests are independent of it. | |
| - name: Build core test suite | |
| run: lake build Test | |
| - name: Download optional Mathlib cache | |
| working-directory: MathlibTest | |
| run: lake exe cache get | |
| - name: Build optional Mathlib test suite | |
| working-directory: MathlibTest | |
| run: lake build | |
| # `lake build` reports a `sorry` as a warning, not an error, so a proof that | |
| # regressed to `sorry` would otherwise pass CI. The suite's contract is that | |
| # every theorem is fully proved. | |
| - name: Assert no sorry | |
| run: | | |
| set -euo pipefail | |
| # Lean reports this as a *warning*, so `lake build` exits 0 even when a | |
| # proof regressed to `sorry`. Match the literal message; note it is | |
| # backtick-quoted (declaration uses `sorry`), so the pattern is quote- | |
| # agnostic rather than assuming a particular quote character. | |
| if lake build Test 2>&1 | grep -nE "declaration uses .sorry."; then | |
| echo "::error::a declaration uses sorry; the suite must be sorry-free" | |
| exit 1 | |
| fi | |
| echo "no sorry found" | |
| - name: Assert no sorry in Mathlib integration tests | |
| working-directory: MathlibTest | |
| run: | | |
| set -euo pipefail | |
| if lake build 2>&1 | grep -nE "declaration uses .sorry."; then | |
| echo "::error::a declaration uses sorry; the suite must be sorry-free" | |
| exit 1 | |
| fi | |
| echo "no sorry found" |