Specify and verify: spqr::encoding::polynomial::PolyDecoder::get_pts_needed in polynomial.rs
#718
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: Lean Verification | |
| # This workflow builds and checks the Lean verification project. | |
| # It ensures that all proofs compile and that the formal verification remains valid. | |
| on: | |
| push: | |
| branches: [ 'main' ] | |
| paths: | |
| - 'Spqr/**' | |
| - 'lakefile.toml' | |
| - 'lean-toolchain' | |
| - '.github/workflows/lean.yml' | |
| # Since the check is required for merging, it must run on every PR even | |
| # when no Lean-related files changed (GitHub treats a skipped required | |
| # check as "not passed"). Restricting `push` to main avoids duplicate | |
| # runs on PR branches while keeping the sorry-manifest cache working. | |
| # See https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/collaborating-on-repositories-with-code-quality-features/troubleshooting-required-status-checks#handling-skipped-but-required-checks | |
| pull_request: | |
| branches: [ '**' ] | |
| workflow_dispatch: | |
| env: | |
| LEAN_ABORT_ON_PANIC: 1 | |
| jobs: | |
| build: | |
| name: Build Lean Project | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| actions: write | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Setup Lean | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build: false | |
| test: false | |
| lint: false | |
| use-mathlib-cache: true | |
| - name: Build and check for non-sorry warnings | |
| run: | | |
| lake build --no-ansi 2>&1 | tee /tmp/lake-build.log | |
| if grep 'warning:' /tmp/lake-build.log | grep -qv 'declaration uses .sorry'; then | |
| echo "::error::Build produced warnings (other than sorry). Please fix them." | |
| grep 'warning:' /tmp/lake-build.log | grep -v 'declaration uses .sorry' | |
| exit 1 | |
| fi | |
| - name: Lint hand-written code | |
| run: | | |
| # Lint ONLY the hand-written `Spqr` library. | |
| lake exe runLinter Spqr 2>&1 | tee /tmp/lake-lint.log || true | |
| if grep -q 'error:' /tmp/lake-lint.log; then | |
| echo "::error::Lint errors in hand-written code. Please fix them." | |
| grep 'error:' /tmp/lake-lint.log | |
| exit 1 | |
| fi | |
| - name: Restore base sorry manifest | |
| if: github.event_name == 'pull_request' | |
| uses: actions/cache/restore@v4 | |
| with: | |
| key: sorry-manifest-${{ github.event.pull_request.base.ref }}-${{ github.event.pull_request.base.sha }} | |
| path: sorry-manifest.txt | |
| - name: Prepare base manifest | |
| if: github.event_name == 'pull_request' | |
| run: | | |
| [ -f sorry-manifest.txt ] && mv sorry-manifest.txt sorry-manifest-base.txt || true | |
| - name: Axiom audit and sorry manifest | |
| run: lake env lean scripts/Audit.lean | |
| - name: Save sorry manifest to cache | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| uses: actions/cache/save@v4 | |
| with: | |
| key: sorry-manifest-main-${{ github.sha }} | |
| path: sorry-manifest.txt | |
| - name: Save PR number | |
| if: github.event_name == 'pull_request' | |
| run: echo "${{ github.event.pull_request.number }}" > pr-number.txt | |
| - name: Upload sorry manifests | |
| if: github.event_name == 'pull_request' | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: sorry-manifests | |
| path: | | |
| sorry-manifest.txt | |
| sorry-manifest-base.txt | |
| pr-number.txt | |
| if-no-files-found: ignore | |
| retention-days: 1 |