From 2978882f1375cae19e412746840a2d7411184bc5 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 17:09:47 +0000 Subject: [PATCH] fix(proof-suite): make the runner's awk POSIX-portable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- scripts/canonical-proof-suite-runner.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/canonical-proof-suite-runner.sh b/scripts/canonical-proof-suite-runner.sh index 14d839b..2e5bf31 100755 --- a/scripts/canonical-proof-suite-runner.sh +++ b/scripts/canonical-proof-suite-runner.sh @@ -88,7 +88,7 @@ BANNED=( parse_manifest() { awk ' BEGIN { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=0 } - /^\s*\(entry$/ { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=1; next } + /^[[:space:]]*\(entry$/ { id=""; domain=""; thm=""; prover=""; proof=""; sym=""; in_entry=1; next } in_entry && /\(id "/ { match($0, /"[^"]*"/); id = substr($0, RSTART+1, RLENGTH-2) } in_entry && /\(domain "/ { match($0, /"[^"]*"/); domain = substr($0, RSTART+1, RLENGTH-2) } in_entry && /\(theorem "/ { match($0, /"[^"]*"/); thm = substr($0, RSTART+1, RLENGTH-2) } @@ -312,7 +312,7 @@ prior_status() { local id="$1" local sc="${SIDECAR_DIR}/${id}.sidecar.a2ml" if [ -f "${sc}" ]; then - grep -E '^\s*\(status "' "${sc}" 2>/dev/null \ + grep -E '^[[:space:]]*\(status "' "${sc}" 2>/dev/null \ | head -1 \ | sed -E 's/.*"([^"]+)".*/\1/' else @@ -480,7 +480,7 @@ TOTAL=$(wc -l < "${TMP_RESULTS}") echo "| ID | Theorem | Prover | Status | Semantic | Elapsed (ms)" while IFS=$'\t' read -r id status elapsed prover kernel proof sem; do thm=$(awk -v want="${id}" ' - /^\s*\(entry$/ { in_e=1; next } + /^[[:space:]]*\(entry$/ { in_e=1; next } in_e && /\(id "/ { match($0, /"[^"]*"/); cur=substr($0,RSTART+1,RLENGTH-2) } in_e && /\(theorem "/ { match($0, /"[^"]*"/); t=substr($0,RSTART+1,RLENGTH-2)