Repository navigation
feat(assail): line-anchor Lean/Isabelle sorry findings so inline markers apply #160
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 | |
| # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | |
| # | |
| # proven-tests.yml — the estate's evidence-graded test framework, wired. | |
| # | |
| # THE TWO JOBS DO DIFFERENT THINGS AND NEITHER PRETENDS TO BE THE OTHER | |
| # --------------------------------------------------------------------- | |
| # `ledger` (every PR, blocking, minutes): derives a proven-tests run report from | |
| # THIS repo's suite — from a test inventory the runner emitted in the same | |
| # commit — and then feeds that report to `panic-attack aggregate | |
| # --proven-tests --fail-on-defect`, which applies the tier->verdict mapping and | |
| # refuses claims the report's own contents do not support (an Actually-Proven | |
| # entry with no ladder, a ladder step citing a file that is not there, a | |
| # summary that disagrees with the entries). A cell with no executed test is a | |
| # gate failure, not a rounding error. | |
| # | |
| # `framework` (schedule and dispatch only, tens of minutes): builds the | |
| # `proven-tests-and-benches` framework itself from a pinned commit with its | |
| # own Idris2 toolchain and runs its suite, so the *grader* is exercised rather | |
| # than trusted. This is deliberately off the PR path: bootstrapping Idris2 for | |
| # every pull request buys nothing that the ledger job does not already prove, | |
| # and it would make every contributor wait on a compiler that cannot change | |
| # for them. | |
| # | |
| # `idris-abi` (every PR, blocking): type-checks this repo's own Idris2 ABI | |
| # proofs in src/abi/. This is a departure from the rule above, made because | |
| # these proofs are claims in PROOF-NEEDS.adoc and a claim needs a receipt on | |
| # every change. Idris2 is built from source once and cached by version and | |
| # commit, so after the first run a PR waits only for the check itself. | |
| # | |
| # WHY THE REPORT IS A FILE, NOT A PARAGRAPH: docs/INTEROP-PANIC-ATTACK.adoc in | |
| # proven-tests-and-benches fixes the mapping in prose; a report plus a verifier | |
| # is the same mapping with something at stake. | |
| name: Proven Tests | |
| on: | |
| pull_request: | |
| branches: ['**'] | |
| push: | |
| branches: [main, master] | |
| schedule: | |
| - cron: '41 4 * * 1' # Mondays, off the hour | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: proven-tests-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| # Pinned: the framework commit this repo's ledger was written against. | |
| PROVEN_TESTS_PIN: eca682bcd419554f6779e72969902e6faef4fd9d | |
| IDRIS2_VERSION: '0.7.0' | |
| jobs: | |
| ledger: | |
| name: Ledger — coverage derived from executed tests | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 | |
| with: | |
| toolchain: stable | |
| - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 | |
| with: | |
| key: proven-ledger | |
| # The suite must PASS before a report may claim anything about it: a | |
| # `result: passed` field written by a job that never ran the tests is | |
| # exactly the dishonesty this framework exists to remove. | |
| - name: Run the suite | |
| run: bash scripts/ci/annotate.sh "proven:suite" -- cargo test --locked --no-fail-fast | |
| - name: Inventory the tests that exist | |
| run: bash scripts/proven/inventory.sh /tmp/inventory.json | |
| - name: Derive the run report (cells must select real tests) | |
| run: | | |
| bash scripts/ci/annotate.sh "proven:ledger" -- \ | |
| bash scripts/proven/verify-ledger.sh \ | |
| --inventory /tmp/inventory.json \ | |
| --ledger proven/ledger.json \ | |
| --root . \ | |
| --out /tmp/proven-report.json | |
| - name: Build panic-attack | |
| run: cargo build --locked --release | |
| # The interop, actually executed: our own tool reads the framework's | |
| # report, applies the mapping in code, and fails on an unsupported claim. | |
| - name: Fold the report through aggregate --fail-on-defect | |
| run: | | |
| set -euo pipefail | |
| bash scripts/ci/annotate.sh "proven:aggregate" -- \ | |
| ./target/release/panic-attack aggregate \ | |
| --proven-tests /tmp/proven-report.json \ | |
| --proven-tests-root . \ | |
| --fail-on-defect \ | |
| --output /tmp/proven-aggregate.json | |
| jq -e '.proven_tests | type == "array" and length == 1 and (.[0].defects == []) and (.[0].summary.total | type == "number" and . > 0)' /tmp/proven-aggregate.json > /dev/null | |
| jq -r '.proven_tests[0].summary | "proven-tests: \(.passed)/\(.total) passed, \(.covered_cells)/\(.cat_aspect_cells) cells, \(.actually_proven) actually-proven"' /tmp/proven-aggregate.json | |
| - name: Publish to the job summary | |
| if: always() | |
| run: | | |
| { | |
| echo "## Proven-tests ledger" | |
| echo "" | |
| if [ -f /tmp/proven-report.json ]; then | |
| python3 - <<'PY' >> "$GITHUB_STEP_SUMMARY" | |
| import json | |
| r = json.load(open('/tmp/proven-report.json')) | |
| s = r['summary'] | |
| print(f"**{s['passed']}/{s['total']}** executed tests, " | |
| f"**{s['covered_cells']}/{s['cat_aspect_cells']}** category×aspect cells") | |
| print("") | |
| print(f"| tier | tests |\n|---|---|") | |
| print(f"| Actually-Proven | {s['actually_proven']} |") | |
| print(f"| Provisionally-Proven | {s['provisionally_proven']} |") | |
| print(f"| Unproven | {s['unproven']} |") | |
| print("") | |
| print("Cells declared absent, with the command that would test them, are in") | |
| print("`proven/ledger.json` — a to-do list, not a silencer.") | |
| PY | |
| else | |
| echo "_the report was not produced; see the failed step above_" | |
| fi | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| - name: Upload the run report | |
| if: always() | |
| uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 | |
| with: | |
| name: proven-report | |
| path: | | |
| /tmp/proven-report.json | |
| /tmp/proven-aggregate.json | |
| retention-days: 30 | |
| if-no-files-found: warn | |
| framework: | |
| name: Framework — the grader is exercised (scheduled) | |
| if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - name: Checkout this repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Checkout proven-tests-and-benches at the pinned commit | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| repository: hyperpolymath/proven-tests-and-benches | |
| ref: ${{ env.PROVEN_TESTS_PIN }} | |
| path: .proven-tests | |
| persist-credentials: false | |
| - name: Cache the Idris2 toolchain | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: ~/.idris2 | |
| key: idris2-v${{ env.IDRIS2_VERSION }}-${{ runner.os }} | |
| - name: Install Idris2 (chez backend) | |
| working-directory: .proven-tests | |
| env: | |
| # The pinned older installer passes this verbatim to git --branch. | |
| # Idris2's release ref is v0.7.0, not 0.7.0. | |
| IDRIS2_VERSION: v${{ env.IDRIS2_VERSION }} | |
| run: bash scripts/install-idris2.sh | |
| - name: Build and run the framework's suite | |
| working-directory: .proven-tests | |
| run: | | |
| set -euo pipefail | |
| export PATH="$HOME/.idris2/bin:$PATH" | |
| idris2 --version | |
| bash scripts/ci-build.sh | |
| - name: Upload the framework's own run report | |
| if: always() | |
| uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 | |
| with: | |
| name: proven-framework-report | |
| path: .proven-tests/build/report/*.json | |
| retention-days: 30 | |
| if-no-files-found: warn | |
| # The Idris2 ABI proofs in src/abi/ (PA1, PA2, Layer 1.0 stripping, | |
| # attestation unforgeability, ABI types). Until this job, none was ever | |
| # type-checked. scripts/ci/check-idris-abi.sh fails on any type error, | |
| # a missing `%default total`, or an escape hatch. | |
| # | |
| # Deviation (PROOF-POLICY §6), state: open. Leg: Idris2 ABI proofs. Tool: | |
| # Idris2 0.7.0 built from the v0.7.0 tag (commit checked below) with the | |
| # runner's Chez Scheme. Why not Guix or the container: panic-attack's Guix | |
| # manifest and container do not provide Idris2 yet. | |
| idris-abi: | |
| name: Idris2 ABI proofs type-check | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 45 | |
| env: | |
| IDRIS2_COMMIT: 27780073c8631826d846499840b3857d9b9a4fd5 | |
| steps: | |
| - name: Checkout this repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Cache the Idris2 toolchain built from source | |
| id: idris2-cache | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: ~/.idris2-src-build | |
| key: idris2-src-${{ env.IDRIS2_VERSION }}-${{ env.IDRIS2_COMMIT }}-${{ runner.os }} | |
| - name: Build Idris2 from the pinned tag (cache miss only) | |
| if: steps.idris2-cache.outputs.cache-hit != 'true' | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update -qq | |
| sudo apt-get install -y -qq chezscheme | |
| src=$(mktemp -d) | |
| git clone --quiet --depth 1 --branch "v${IDRIS2_VERSION}" \ | |
| https://github.com/idris-lang/Idris2.git "$src" | |
| test "$(git -C "$src" rev-parse HEAD)" = "$IDRIS2_COMMIT" | |
| make -C "$src" bootstrap SCHEME=scheme PREFIX="$HOME/.idris2-src-build" | |
| make -C "$src" install PREFIX="$HOME/.idris2-src-build" | |
| - name: Type-check every module in src/abi | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| # The cached build still needs Chez Scheme at run time. | |
| command -v scheme >/dev/null || { sudo apt-get update -qq && sudo apt-get install -y -qq chezscheme; } | |
| export PATH="$HOME/.idris2-src-build/bin:$PATH" | |
| bash scripts/ci/check-idris-abi.sh |