paper 2.0.0: the relation to classical logic, stated without understa… #162
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 | |
| on: | |
| push: | |
| paths: | |
| - "lean/**" | |
| - "inventory/**" | |
| - ".github/workflows/lean.yml" | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: lean | |
| # The hand-placed `#print axioms` lines. The floor tracks the corpus | |
| # exactly (158 on 2026-07-21): a threshold set well below the real | |
| # count would stay green while dozens of prints were deleted. | |
| - name: zero-axiom ledger | |
| working-directory: lean | |
| run: | | |
| lake build > build.log 2>&1 | |
| clean=$(grep -c "does not depend on any axioms" build.log || true) | |
| dirty=$(grep -c "depends on axioms" build.log || true) | |
| echo "zero-axiom checks: $clean; dirty: $dirty" | |
| test "$dirty" -eq 0 | |
| test "$clean" -ge 558 | |
| # The hand-placed prints cover 558 names of 1112 theorems; the rest are | |
| # covered transitively, which is an ARGUMENT. This audits every | |
| # theorem individually, and fails on an orphan module that no | |
| # target builds. | |
| - name: per-theorem axiom audit | |
| run: python3 inventory/axiom_audit.py |