census: Nurse and Triage take their seats in the fold — carved after … #1220
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: CI | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| lean: | |
| name: Lean (zero sorry, zero warning) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "" | |
| lake-package-directory: . | |
| - name: Build each Lean file individually (surfaces hidden type errors) | |
| run: | | |
| for f in $(find Foam -name '*.lean' | sort); do | |
| mod=$(echo "${f%.lean}" | tr '/' '.') | |
| echo "Building $mod..." | |
| lake build "$mod" || exit 1 | |
| done | |
| - name: Build counter (the axiom-free application layer) | |
| run: cd counter && lake build | |
| - name: Every discovered identity pinned (the rfl-Twins procession) | |
| # producer: bin/foam-rfl (scans for identical bodies). consumer: | |
| # counter/Counter/Twins.lean (pins each as rfl). procession: this | |
| # check (discovered => pinned) plus lake build itself (pinned => | |
| # still true — once pinned, divergence is a build break: a ratchet). | |
| run: bin/foam-rfl --check | |
| - name: Build seam (the identification layer — core-Lean axioms only) | |
| run: cd seam && lake build | |
| - name: No warnings (sorry included — zero tolerance) | |
| run: | | |
| warns=0 | |
| for f in $(find Foam -name '*.lean' | sort); do | |
| mod=$(echo "${f%.lean}" | tr '/' '.') | |
| touch "$f" | |
| # Every warning counts now — sorry no longer exempt. The mirror | |
| # commits to its own hygiene: a hole is a failure, not a known gap. | |
| found=$(lake build "$mod" 2>&1 | grep "warning:" || true) | |
| if [ -n "$found" ]; then | |
| echo "$found" | |
| warns=$((warns + 1)) | |
| fi | |
| done | |
| if [ $warns -gt 0 ]; then | |
| echo "" | |
| echo "Warnings found (sorry included). Fix before merging." | |
| exit 1 | |
| fi | |
| echo "Clean: zero warnings, sorry included" | |
| integrity: | |
| name: Reference integrity | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Every Lean file referenced in README.md | |
| run: | | |
| # the spirit of this law: the readme mentions everyone in here. | |
| # the letter below covers all four packages; if letter and spirit | |
| # ever diverge again, the spirit wins (see README expeditions: judiciary). | |
| # word-boundary match per foam-judge's first finding: substring | |
| # match let short names (Mu, Nu, Lu, Kin, ...) pass by coincidence. | |
| errors=0 | |
| for f in $(find Foam counter/Counter seam/Seam bridges/Bridges -name '*.lean' | sort); do | |
| base=$(basename "$f" .lean) | |
| if ! grep -qw "$base" README.md; then | |
| echo "UNREFERENCED: $base (not in README.md)" | |
| errors=$((errors + 1)) | |
| fi | |
| done | |
| if [ $errors -gt 0 ]; then | |
| echo "" | |
| echo "$errors lean file(s) not referenced in README.md" | |
| exit 1 | |
| fi | |
| echo "All lean files referenced" | |
| - name: Every module ranked on the spine (the SPINE-corpus procession) | |
| # the two tellings (README shape, gait SPINE) are each conserved | |
| # against the one quiver rather than against each other: census | |
| # closes README-corpus, --strict closes SPINE-corpus, and the | |
| # SPINE-README pair closes transitively through the shared object. | |
| run: bin/foam-gait --strict | |
| - name: Every schema audit has its rest-theorem (the audits-Silent procession) | |
| run: | | |
| # producer: schema.sql's runtime audits (finite shadows). consumer: | |
| # counter/Counter/Silent.lean (the laws: each audit's silence sealed | |
| # over the infinite domain). procession: every foam.*_audit names a | |
| # theorem carrying its name; lake build keeps the theorems true. | |
| errors=0 | |
| for a in $(grep -oE 'FUNCTION foam\.[a-z_]+_audit' schema.sql | sed 's/FUNCTION foam\.//' | sort -u); do | |
| if ! grep -q "$a" counter/Counter/Silent.lean; then | |
| echo "UNRESTED: foam.$a (no rest-theorem in Silent.lean)" | |
| errors=$((errors + 1)) | |
| fi | |
| done | |
| if [ $errors -gt 0 ]; then exit 1; fi | |
| echo "All audits rest on named theorems" | |
| - name: Every Lean citation in schema.sql and bin/ resolves | |
| run: | | |
| # The operational layer (schema.sql, bin/) cites its proofs by module path — | |
| # "the why is the Lean." A citation to a moved or retired module is a receipt | |
| # with no record. The reverse of the check above: there, every Lean file must | |
| # be named in README; here, every Lean file named in the operational layer must | |
| # exist. Self-certifying, the way foam.born_audit / foam.held_audit are for the | |
| # field's own laws. | |
| errors=0 | |
| for ref in $(grep -rhoE 'Foam/[A-Za-z0-9/]+\.lean' schema.sql bin/ | sort -u); do | |
| if [ ! -f "$ref" ]; then | |
| echo "DANGLING: $ref (cited in schema.sql/bin, no such file)" | |
| errors=$((errors + 1)) | |
| fi | |
| done | |
| if [ $errors -gt 0 ]; then | |
| echo "" | |
| echo "$errors dangling Lean citation(s) — repoint to the real module path" | |
| exit 1 | |
| fi | |
| echo "All Lean citations in schema.sql and bin/ resolve" | |
| comments: | |
| name: Comment-free Lean (only #print axioms receipts) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Audit Lean for reader-facing comments | |
| run: python3 .github/comment_audit.py |