fix(proof-suite): make the runner's awk POSIX-portable (mawk reported 0/0)#47
Merged
Merged
Conversation
`canonical-proof-suite-runner.sh` parsed the manifest with `\s` in its awk patterns (`/^\s*\(entry$/`) — `\s` is a GNU-awk extension. Under `mawk` (the default `awk` on Debian/Ubuntu and many CI/dev boxes) `\s` matches nothing, so `parse_manifest` returns zero entries and the runner reports a silent `Summary: 0/0 passing` while exiting 0 — i.e. it looks like it ran but checked nothing. Replace the three `\s` occurrences (two awk `(entry` matchers + one `grep -E` status matcher) with POSIX `[[:space:]]`, which behaves identically under mawk, gawk, and grep. Verified with a locally-installed Rocq 9 + idris2 + agda: the runner now parses all entries and reports `Summary: 35/37 passing` (the 2 not-passing are the Coquelicot/mathcomp-dependent proofs whose sources are unreachable from this host) — previously `0/0`. https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
hyperpolymath
marked this pull request as ready for review
June 18, 2026 17:35
This was referenced Jun 19, 2026
hyperpolymath
pushed a commit
that referenced
this pull request
Jun 20, 2026
… (35/37) Roadmap item 3 (full proof suite green). A full local runner pass — idris2 0.8 + agda 2.6.3 + Rocq 9.0, now awk-portable since #47 — reports **35/37 passing, 2 regressed**. The key finding: the suite was far greener than its labels. `M5-yoneda.agda` is not a stub — it is a complete 386-line self-contained Yoneda formalization that compiles (my earlier "agda 0/1" was the same path/module-name trap as the idris files: run from repo root vs. `cd` into the dir + basename). Likewise the ~20 `not-started`-labelled rocq entries (M6–M14, S6–S10, E6–E11) all compile and define their headline symbol. So this flips 21 stale `not-started` + 1 stale `in-progress` (M1) labels to `passing`, verified by that runner pass. The 2 not locally verifiable — `M2` (mathcomp) and `E1` (Coquelicot, ndim port) — keep their prior CI-canonical `passing` status: their dependency sources live on `gitlab.inria.fr` / `erratique.ch` (403 in this github-only environment) but pass in CI. `REPORT.a2ml` and the per-entry sidecars are intentionally NOT regenerated from this local run (they would show those 2 as locally-regressed); the nightly CI run with the full toolchain regenerates the canonical evidence. Manifest stays well-formed (parens 500/500; 37 entries parse; all `passing`); revision-log entry added; `last-manifest-update` bumped. https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
canonical-proof-suite-runner.shparsed the manifest with\sin its awk patterns (/^\s*\(entry$/).\sis a GNU-awk extension — undermawk(the defaultawkon Debian/Ubuntu and many CI/dev boxes) it matches nothing, soparse_manifestreturns zero entries and the runner prints a silentSummary: 0/0 passingwhile exiting 0. It looks like it ran, but checked nothing.Fix
Replace the three
\soccurrences — two awk(entrymatchers + onegrep -Estatus matcher — with POSIX[[:space:]], which behaves identically under mawk, gawk, and grep.Verified
Installed Rocq 9 + idris2 + agda locally and ran the runner:
Summary: 0/0 passing(mawk parsed nothing)Summary: 35/37 passing— matches a directcoqcsweep of the.vfiles(The 2 not-passing are the Coquelicot/mathcomp-dependent proofs, whose sources live on hosts unreachable from this box's network policy — unrelated to this fix.)
One-line-per-site portability fix; no behavior change in CI (gawk already accepted
\s), but now the suite is runnable locally too.https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We
Generated by Claude Code