|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# check-corpus.sh — gate the RUNNABLE corpus: examples/ and conformance/. |
| 4 | +# |
| 5 | +# ── Why this exists ──────────────────────────────────────────────────────── |
| 6 | +# Neither examples/ nor conformance/ was executed by anything — not CI, not the |
| 7 | +# Justfile. The cost of that was concrete: `examples/isotopy.tangle`, the file |
| 8 | +# whose entire purpose is to demonstrate the language's central claim ("two |
| 9 | +# braids can be structurally different but topologically equivalent"), FAILED |
| 10 | +# with "Assertion failed" and had done for as long as `~` used free reduction. |
| 11 | +# It only began passing when TG-7 (#50/#87) made `~` decide real braid-group |
| 12 | +# equivalence. A showcase example can sit broken indefinitely if nothing runs it. |
| 13 | +# |
| 14 | +# ── Why a RATCHET rather than a pass/fail ────────────────────────────────── |
| 15 | +# Five example programs do not typecheck and five conformance `valid/` programs |
| 16 | +# do not parse. Those are real gaps (see below), not things to paper over — but |
| 17 | +# they also cannot be fixed in the change that introduces the gate. So each |
| 18 | +# known failure is recorded EXPLICITLY here with its cause. The gate then |
| 19 | +# enforces, in both directions: |
| 20 | +# |
| 21 | +# * nothing currently working may break (regression) |
| 22 | +# * nothing may join the known-bad lists (new debt) |
| 23 | +# * anything that starts working MUST be removed from the list (the ratchet |
| 24 | +# tightens — a stale entry is itself a failure) |
| 25 | +# |
| 26 | +# That last rule is what stops an "expected failures" list decaying into a |
| 27 | +# permanent excuse. |
| 28 | +# |
| 29 | +# USAGE: scripts/check-corpus.sh [path-to-tangle-binary] |
| 30 | +# EXIT: 0 = corpus matches the manifest exactly; 1 = drift in either direction |
| 31 | + |
| 32 | +set -uo pipefail |
| 33 | + |
| 34 | +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" |
| 35 | +BIN="${1:-${ROOT}/compiler/_build/default/bin/main.exe}" |
| 36 | + |
| 37 | +if [[ ! -x "${BIN}" ]]; then |
| 38 | + echo "::error::tangle binary not found or not executable: ${BIN}" |
| 39 | + echo "Build it first: (cd compiler && dune build)" |
| 40 | + exit 1 |
| 41 | +fi |
| 42 | + |
| 43 | +# ── MANIFEST ─────────────────────────────────────────────────────────────── |
| 44 | +# Examples that must fully TYPECHECK and EVALUATE (all their asserts hold). |
| 45 | +EXAMPLES_MUST_RUN=( |
| 46 | + echo_pd.tangle |
| 47 | + isotopy.tangle # the TG-7 witness — see header |
| 48 | +) |
| 49 | + |
| 50 | +# Examples that PARSE but do not yet TYPECHECK. Cause is recorded per entry so |
| 51 | +# the list cannot quietly become a dumping ground. Tracked in #88. |
| 52 | +# braids_as_data / trefoil : recursive fn returning Num — `1 + length(rest)` |
| 53 | +# infers the recursive call as Word[0], not Num |
| 54 | +# compositional_pd / tensor_product : `identity == braid[...]` is a width |
| 55 | +# mismatch (Word[0] vs Word[n]) under T-Eq-Word |
| 56 | +# turing_complete : match arms disagree in width (Word[0] vs Word[2]) |
| 57 | +EXAMPLES_KNOWN_UNTYPED=( |
| 58 | + braids_as_data.tangle |
| 59 | + compositional_pd.tangle |
| 60 | + tensor_product.tangle |
| 61 | + trefoil.tangle |
| 62 | + turing_complete.tangle |
| 63 | +) |
| 64 | + |
| 65 | +# conformance/valid programs the parser does not yet accept. These specify |
| 66 | +# language surface that exists in the spec but not in parser.mly. Tracked in #88. |
| 67 | +# v02/v08/v09/v12 : `weave strands a:Q, b:Q into (...) yield strands ...` |
| 68 | +# v11 : `add{ ... }` blocks (JTV data injection) |
| 69 | +CONFORMANCE_KNOWN_UNPARSED=( |
| 70 | + v02_weave.tangle |
| 71 | + v08_crossing.tangle |
| 72 | + v09_twist.tangle |
| 73 | + v11_add_block.tangle |
| 74 | + v12_weave_expr.tangle |
| 75 | +) |
| 76 | + |
| 77 | +fail=0 |
| 78 | +note() { printf ' %-34s %s\n' "$1" "$2"; } |
| 79 | + |
| 80 | +in_list() { local n="$1"; shift; local x; for x in "$@"; do [[ "$x" == "$n" ]] && return 0; done; return 1; } |
| 81 | + |
| 82 | +# ── 1. Every example must PARSE. No exceptions: a file that cannot even parse |
| 83 | +# is not documentation, it is a syntax error with a licence header. |
| 84 | +echo "== examples: parse ==" |
| 85 | +for f in "${ROOT}"/examples/*.tangle; do |
| 86 | + n="$(basename "$f")" |
| 87 | + if "${BIN}" "$f" >/dev/null 2>&1; then note "$n" "parse ok"; else |
| 88 | + note "$n" "PARSE FAILED"; echo "::error::${n} does not parse"; fail=1; fi |
| 89 | +done |
| 90 | + |
| 91 | +# ── 2. The working examples must keep typechecking AND evaluating. |
| 92 | +echo "== examples: typecheck + evaluate (must-run set) ==" |
| 93 | +for n in "${EXAMPLES_MUST_RUN[@]}"; do |
| 94 | + f="${ROOT}/examples/${n}" |
| 95 | + if [[ ! -f "$f" ]]; then |
| 96 | + echo "::error::manifest lists ${n} but the file is gone"; fail=1; continue; fi |
| 97 | + if "${BIN}" --eval "$f" >/dev/null 2>&1; then note "$n" "eval ok"; else |
| 98 | + note "$n" "EVAL FAILED" |
| 99 | + echo "::error::${n} must evaluate cleanly (all asserts holding) and does not:" |
| 100 | + "${BIN}" --eval "$f" 2>&1 | head -5 |
| 101 | + fail=1 |
| 102 | + fi |
| 103 | +done |
| 104 | + |
| 105 | +# ── 3. The known-untyped examples: still parse, still fail to typecheck. |
| 106 | +# If one starts typechecking, the manifest is STALE and must be updated. |
| 107 | +echo "== examples: known-untyped (ratchet) ==" |
| 108 | +for n in "${EXAMPLES_KNOWN_UNTYPED[@]}"; do |
| 109 | + f="${ROOT}/examples/${n}" |
| 110 | + if [[ ! -f "$f" ]]; then |
| 111 | + echo "::error::manifest lists ${n} but the file is gone"; fail=1; continue; fi |
| 112 | + if "${BIN}" --eval "$f" >/dev/null 2>&1; then |
| 113 | + note "$n" "NOW WORKS" |
| 114 | + echo "::error::${n} now evaluates — good! Move it to EXAMPLES_MUST_RUN and drop it from EXAMPLES_KNOWN_UNTYPED." |
| 115 | + fail=1 |
| 116 | + else |
| 117 | + note "$n" "still untyped (expected)" |
| 118 | + fi |
| 119 | +done |
| 120 | + |
| 121 | +# ── 4. Any example NOT in either list is unaccounted for. |
| 122 | +echo "== examples: manifest covers every file ==" |
| 123 | +for f in "${ROOT}"/examples/*.tangle; do |
| 124 | + n="$(basename "$f")" |
| 125 | + if ! in_list "$n" "${EXAMPLES_MUST_RUN[@]}" && ! in_list "$n" "${EXAMPLES_KNOWN_UNTYPED[@]}"; then |
| 126 | + note "$n" "UNLISTED" |
| 127 | + echo "::error::${n} is in examples/ but not in the manifest. Add it to EXAMPLES_MUST_RUN (preferred) or, with a recorded cause, EXAMPLES_KNOWN_UNTYPED." |
| 128 | + fail=1 |
| 129 | + fi |
| 130 | +done |
| 131 | + |
| 132 | +# ── 5. Conformance: valid must parse (except the recorded set); invalid must NOT. |
| 133 | +echo "== conformance ==" |
| 134 | +for f in "${ROOT}"/conformance/valid/*.tangle; do |
| 135 | + n="$(basename "$f")" |
| 136 | + if "${BIN}" "$f" >/dev/null 2>&1; then |
| 137 | + if in_list "$n" "${CONFORMANCE_KNOWN_UNPARSED[@]}"; then |
| 138 | + note "valid/$n" "NOW PARSES" |
| 139 | + echo "::error::conformance/valid/${n} now parses — drop it from CONFORMANCE_KNOWN_UNPARSED." |
| 140 | + fail=1 |
| 141 | + else |
| 142 | + note "valid/$n" "parse ok" |
| 143 | + fi |
| 144 | + else |
| 145 | + if in_list "$n" "${CONFORMANCE_KNOWN_UNPARSED[@]}"; then |
| 146 | + note "valid/$n" "still unparsed (expected)" |
| 147 | + else |
| 148 | + note "valid/$n" "PARSE FAILED" |
| 149 | + echo "::error::conformance/valid/${n} must parse and does not"; fail=1 |
| 150 | + fi |
| 151 | + fi |
| 152 | +done |
| 153 | +for f in "${ROOT}"/conformance/invalid/*.tangle; do |
| 154 | + n="$(basename "$f")" |
| 155 | + if "${BIN}" "$f" >/dev/null 2>&1; then |
| 156 | + note "invalid/$n" "PARSED (should not)" |
| 157 | + echo "::error::conformance/invalid/${n} parsed successfully but is meant to be rejected"; fail=1 |
| 158 | + else |
| 159 | + note "invalid/$n" "rejected ok" |
| 160 | + fi |
| 161 | +done |
| 162 | + |
| 163 | +echo |
| 164 | +if [[ "$fail" -ne 0 ]]; then |
| 165 | + echo "::error::corpus drifted from the manifest — see the errors above." |
| 166 | + exit 1 |
| 167 | +fi |
| 168 | +echo "Corpus matches the manifest: examples parse, the must-run set evaluates," |
| 169 | +echo "known gaps are unchanged, and invalid programs are still rejected." |
0 commit comments