paper 2.0.0: the relation to classical logic, stated without understa… #619
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: regression | |
| # Every MEASURED claim of the preprint — the 12/14 price list, the | |
| # algebraic passport, interpolation, cut admissibility, the temporal | |
| # layer, the quantum stands — rests on these stands. Until 2026-07-20 | |
| # no workflow ran them: they were green on the author's machine only, | |
| # which is precisely the kind of assurance this project refuses to | |
| # grant itself. | |
| # | |
| # No `paths:` filter, deliberately. The Python core and the Lean corpus | |
| # mirror each other, and `bridge.py` is what proves they still agree | |
| # (141 kernel-computed answers, cell by cell). A filter on lean/** would | |
| # let a change to ztl.py drift away from ZTL.lean unnoticed — the one | |
| # divergence that would invalidate the machine-verification claim. | |
| on: | |
| push: | |
| # Branches only. A tag push re-runs the workflow against the commit the tag | |
| # points at — and release tags point at FROZEN history (a downstream input | |
| # tag pinned by a consumer). Old commits predate current fixes and fail | |
| # honestly; that is not a regression, it is archaeology, and it cannot be | |
| # repaired without breaking the pin. Test the branch, not the museum. | |
| branches: | |
| - '**' | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| stands: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # ПОЛНАЯ история и теги. Мелкий клон (глубина 1, без тегов) прячет | |
| # целый класс расхождений: стенд, опирающийся на пин, без истории | |
| # объявляет прогон недействительным и валит regression — а локально | |
| # всё зелено. Промерено 2026-08-31: «ALL GREEN 144» локально против | |
| # RED на удалённом расходились ИМЕННО здесь, и это был не сбой | |
| # инфраструктуры. Стенд, из-за которого правило появилось, изъят | |
| # 2026-09-03 (его опора исчезла вместе с переписанной историей), но | |
| # правило остаётся: оно про класс, а не про один прибор. | |
| with: | |
| fetch-depth: 0 | |
| fetch-tags: true | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: lean | |
| build: false | |
| # run_all.py ends with `lake build` itself and asserts the | |
| # zero-axiom line, so the Lean corpus is exercised here too. | |
| # poppler-utils must be present BEFORE run_all.py, not after it: | |
| # inventory/paper_claims.py is itself one of the stands, and it counts | |
| # PDF pages with `pdfinfo`. Installing poppler only for the later step | |
| # left the in-regression run without it, so the stand reported | |
| # "sheet: says 9, measured None" and the workflow was RED on every push | |
| # from 2026-07-22 onward. The corpus was never at fault. | |
| - name: page-count tool for the paper claims | |
| run: sudo apt-get install -y poppler-utils >/dev/null 2>&1 || true | |
| - name: all stands + Lean | |
| run: python3 run_all.py | |
| # The papers are claims too. Until 2026-07-20 nothing checked that | |
| # their numbers matched the corpus, and two of them did not. | |
| - name: paper claims | |
| run: | | |
| sudo apt-get install -y poppler-utils >/dev/null 2>&1 || true | |
| python3 inventory/paper_claims.py |