Skip to content

Commit 2c52cf6

Browse files
claudehyperpolymath
authored andcommitted
fix(proof-suite): make the runner's awk POSIX-portable
`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
1 parent d3757b8 commit 2c52cf6

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

scripts/canonical-proof-suite-runner.sh

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ BANNED=(
8888
parse_manifest() {
8989
awk '
9090
BEGIN { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=0 }
91-
/^\s*\(entry$/ { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=1; next }
91+
/^[[:space:]]*\(entry$/ { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=1; next }
9292
in_entry && /\(id "/ { match($0, /"[^"]*"/); id = substr($0, RSTART+1, RLENGTH-2) }
9393
in_entry && /\(domain "/ { match($0, /"[^"]*"/); domain = substr($0, RSTART+1, RLENGTH-2) }
9494
in_entry && /\(theorem "/ { match($0, /"[^"]*"/); thm = substr($0, RSTART+1, RLENGTH-2) }
@@ -312,7 +312,7 @@ prior_status() {
312312
local id="$1"
313313
local sc="${SIDECAR_DIR}/${id}.sidecar.a2ml"
314314
if [ -f "${sc}" ]; then
315-
grep -E '^\s*\(status "' "${sc}" 2>/dev/null \
315+
grep -E '^[[:space:]]*\(status "' "${sc}" 2>/dev/null \
316316
| head -1 \
317317
| sed -E 's/.*"([^"]+)".*/\1/'
318318
else
@@ -480,7 +480,7 @@ TOTAL=$(wc -l < "${TMP_RESULTS}")
480480
echo "| ID | Theorem | Prover | Status | Semantic | Elapsed (ms)"
481481
while IFS=$'\t' read -r id status elapsed prover kernel proof sem; do
482482
thm=$(awk -v want="${id}" '
483-
/^\s*\(entry$/ { in_e=1; next }
483+
/^[[:space:]]*\(entry$/ { in_e=1; next }
484484
in_e && /\(id "/ { match($0, /"[^"]*"/); cur=substr($0,RSTART+1,RLENGTH-2) }
485485
in_e && /\(theorem "/ {
486486
match($0, /"[^"]*"/); t=substr($0,RSTART+1,RLENGTH-2)

0 commit comments

Comments
 (0)