proofs(lean4): promote ET-2 to main — L1 conversion is decidable #9
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
| # SPDX-License-Identifier: MPL-2.0 | |
| # Proof gate: the same scripts/check-proofs.sh a developer runs locally. | |
| # Hermetic by construction — elan comes from a version-pinned release tarball | |
| # with a checksum, the Lean toolchain from the committed lean-toolchain file, | |
| # and no floating setup action is involved. A missing prover FAILS (the gate | |
| # never skips), so this workflow existing is what makes green mean "proved". | |
| name: proofs | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - "verification/proofs/**" | |
| - "scripts/check-proofs.sh" | |
| - "scripts/check-proof-status.sh" | |
| - "scripts/scan-dangerous.sh" | |
| - "docs/status/PROOF-STATUS.adoc" | |
| - ".github/workflows/proofs.yml" | |
| pull_request: | |
| paths: | |
| - "verification/proofs/**" | |
| - "scripts/check-proofs.sh" | |
| - "scripts/check-proof-status.sh" | |
| - "scripts/scan-dangerous.sh" | |
| - "docs/status/PROOF-STATUS.adoc" | |
| - ".github/workflows/proofs.yml" | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| jobs: | |
| lean4: | |
| name: lean4 proof gate | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Cache elan + toolchain (keyed on lean-toolchain pin) | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: ~/.elan | |
| key: elan-4.2.3-${{ runner.os }}-${{ hashFiles('verification/proofs/lean4/lean-toolchain') }} | |
| - name: Install elan (pinned tarball, checksum-verified) | |
| run: | | |
| set -euo pipefail | |
| if [ ! -x "$HOME/.elan/bin/elan" ]; then | |
| ELAN_VERSION=4.2.3 | |
| ELAN_SHA256=df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2 | |
| curl -sSfL --proto '=https' --tlsv1.2 -o /tmp/elan.tar.gz \ | |
| "https://github.com/leanprover/elan/releases/download/v${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz" | |
| echo "${ELAN_SHA256} /tmp/elan.tar.gz" | sha256sum -c - | |
| tar -xzf /tmp/elan.tar.gz -C /tmp | |
| /tmp/elan-init -y --default-toolchain none | |
| fi | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Install pinned Lean toolchain | |
| run: | | |
| set -euo pipefail | |
| tc="$(cat verification/proofs/lean4/lean-toolchain)" | |
| # `elan toolchain install` exits 1 with "is already installed" when the | |
| # runner image already ships the pinned toolchain, which fails the gate | |
| # for a reason that has nothing to do with the proofs. Install only when | |
| # absent, so a genuine install failure still fails the gate. | |
| # match on the first field so an annotated listing (e.g. "... (default)") still matches | |
| if elan toolchain list | awk '{print $1}' | grep -qx "$tc"; then | |
| echo "toolchain $tc already present" | |
| else | |
| elan toolchain install "$tc" | |
| fi | |
| elan toolchain list | |
| - name: Proof gate (compile + coverage + axiom audit) | |
| run: ./scripts/check-proofs.sh lean4 | |
| - name: Dangerous-construct scan | |
| run: ./scripts/scan-dangerous.sh | |
| - name: Status drift gate (PROOF-STATUS must match MANIFEST) | |
| run: ./scripts/check-proof-status.sh |