diff --git a/.github/workflows/ocaml-ci.yml b/.github/workflows/ocaml-ci.yml index 9d9a87c..c90234b 100644 --- a/.github/workflows/ocaml-ci.yml +++ b/.github/workflows/ocaml-ci.yml @@ -29,10 +29,16 @@ on: branches: [main] paths: - 'compiler/**' + - 'examples/**' + - 'conformance/**' + - 'scripts/check-corpus.sh' - '.github/workflows/ocaml-ci.yml' pull_request: paths: - 'compiler/**' + - 'examples/**' + - 'conformance/**' + - 'scripts/check-corpus.sh' - '.github/workflows/ocaml-ci.yml' workflow_dispatch: {} @@ -93,6 +99,15 @@ jobs: fi echo "OCaml compiler: build + all suites GREEN." + - name: Corpus gate (examples + conformance) + run: | + set -euo pipefail + # Runs the language's OWN programs. Neither examples/ nor conformance/ + # was executed by anything before this, which is how + # examples/isotopy.tangle — the demonstration of the central claim — + # sat failing its own assertions until TG-7 (#87) fixed `~`. + bash scripts/check-corpus.sh + - name: TG-7 semantics guard working-directory: compiler run: | diff --git a/Justfile b/Justfile index d59bd23..f4a648b 100644 --- a/Justfile +++ b/Justfile @@ -74,3 +74,13 @@ crg-badge: secret-scan-trufflehog: @command -v trufflehog >/dev/null && trufflehog filesystem . --only-verified || true + +# Run the language's own programs (examples/ + conformance/) — same gate as CI +corpus: + @cd compiler && dune build + @bash scripts/check-corpus.sh + +# Compiler build + full test suite (4,000+ assertions) + the corpus gate. +check-all: + @cd compiler && dune build && dune test --force + @bash scripts/check-corpus.sh diff --git a/conformance/run_conformance.sh b/conformance/run_conformance.sh index 6773809..c326014 100755 --- a/conformance/run_conformance.sh +++ b/conformance/run_conformance.sh @@ -17,9 +17,25 @@ if [[ -n "${1:-}" ]]; then # shellcheck disable=SC2206 # deliberate word-splitting of caller's string PARSER_CMD=(${1}) else - PARSER_CMD=(dune exec --root "${SCRIPT_DIR}/../compiler" -- tangle --parse-only) + # The default used to be `dune exec -- tangle --parse-only`. BOTH halves were + # wrong: the executable is named `main` (compiler/bin/dune), not `tangle`, and + # there has never been a `--parse-only` flag — bare `` is parse + + # pretty-print. So every invocation failed, which made this suite REPORT + # 3/19 while proving nothing: the three "passes" were invalid/ cases, and an + # invalid case "passes" precisely when the command fails. It failed for the + # wrong reason and scored a point for it. + # + # Prefer a pre-built binary (CI builds once); fall back to `dune exec`. + BIN="${SCRIPT_DIR}/../compiler/_build/default/bin/main.exe" + if [[ -x "${BIN}" ]]; then + PARSER_CMD=("${BIN}") + else + PARSER_CMD=(dune exec --root "${SCRIPT_DIR}/../compiler" -- ./bin/main.exe) + fi fi +echo "parser: ${PARSER_CMD[*]}" + PASS=0 FAIL=0 TOTAL=0 diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh new file mode 100755 index 0000000..0627332 --- /dev/null +++ b/scripts/check-corpus.sh @@ -0,0 +1,169 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# check-corpus.sh — gate the RUNNABLE corpus: examples/ and conformance/. +# +# ── Why this exists ──────────────────────────────────────────────────────── +# Neither examples/ nor conformance/ was executed by anything — not CI, not the +# Justfile. The cost of that was concrete: `examples/isotopy.tangle`, the file +# whose entire purpose is to demonstrate the language's central claim ("two +# braids can be structurally different but topologically equivalent"), FAILED +# with "Assertion failed" and had done for as long as `~` used free reduction. +# It only began passing when TG-7 (#50/#87) made `~` decide real braid-group +# equivalence. A showcase example can sit broken indefinitely if nothing runs it. +# +# ── Why a RATCHET rather than a pass/fail ────────────────────────────────── +# Five example programs do not typecheck and five conformance `valid/` programs +# do not parse. Those are real gaps (see below), not things to paper over — but +# they also cannot be fixed in the change that introduces the gate. So each +# known failure is recorded EXPLICITLY here with its cause. The gate then +# enforces, in both directions: +# +# * nothing currently working may break (regression) +# * nothing may join the known-bad lists (new debt) +# * anything that starts working MUST be removed from the list (the ratchet +# tightens — a stale entry is itself a failure) +# +# That last rule is what stops an "expected failures" list decaying into a +# permanent excuse. +# +# USAGE: scripts/check-corpus.sh [path-to-tangle-binary] +# EXIT: 0 = corpus matches the manifest exactly; 1 = drift in either direction + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +BIN="${1:-${ROOT}/compiler/_build/default/bin/main.exe}" + +if [[ ! -x "${BIN}" ]]; then + echo "::error::tangle binary not found or not executable: ${BIN}" + echo "Build it first: (cd compiler && dune build)" + exit 1 +fi + +# ── MANIFEST ─────────────────────────────────────────────────────────────── +# Examples that must fully TYPECHECK and EVALUATE (all their asserts hold). +EXAMPLES_MUST_RUN=( + echo_pd.tangle + isotopy.tangle # the TG-7 witness — see header +) + +# Examples that PARSE but do not yet TYPECHECK. Cause is recorded per entry so +# the list cannot quietly become a dumping ground. Tracked in #88. +# braids_as_data / trefoil : recursive fn returning Num — `1 + length(rest)` +# infers the recursive call as Word[0], not Num +# compositional_pd / tensor_product : `identity == braid[...]` is a width +# mismatch (Word[0] vs Word[n]) under T-Eq-Word +# turing_complete : match arms disagree in width (Word[0] vs Word[2]) +EXAMPLES_KNOWN_UNTYPED=( + braids_as_data.tangle + compositional_pd.tangle + tensor_product.tangle + trefoil.tangle + turing_complete.tangle +) + +# conformance/valid programs the parser does not yet accept. These specify +# language surface that exists in the spec but not in parser.mly. Tracked in #88. +# v02/v08/v09/v12 : `weave strands a:Q, b:Q into (...) yield strands ...` +# v11 : `add{ ... }` blocks (JTV data injection) +CONFORMANCE_KNOWN_UNPARSED=( + v02_weave.tangle + v08_crossing.tangle + v09_twist.tangle + v11_add_block.tangle + v12_weave_expr.tangle +) + +fail=0 +note() { printf ' %-34s %s\n' "$1" "$2"; } + +in_list() { local n="$1"; shift; local x; for x in "$@"; do [[ "$x" == "$n" ]] && return 0; done; return 1; } + +# ── 1. Every example must PARSE. No exceptions: a file that cannot even parse +# is not documentation, it is a syntax error with a licence header. +echo "== examples: parse ==" +for f in "${ROOT}"/examples/*.tangle; do + n="$(basename "$f")" + if "${BIN}" "$f" >/dev/null 2>&1; then note "$n" "parse ok"; else + note "$n" "PARSE FAILED"; echo "::error::${n} does not parse"; fail=1; fi +done + +# ── 2. The working examples must keep typechecking AND evaluating. +echo "== examples: typecheck + evaluate (must-run set) ==" +for n in "${EXAMPLES_MUST_RUN[@]}"; do + f="${ROOT}/examples/${n}" + if [[ ! -f "$f" ]]; then + echo "::error::manifest lists ${n} but the file is gone"; fail=1; continue; fi + if "${BIN}" --eval "$f" >/dev/null 2>&1; then note "$n" "eval ok"; else + note "$n" "EVAL FAILED" + echo "::error::${n} must evaluate cleanly (all asserts holding) and does not:" + "${BIN}" --eval "$f" 2>&1 | head -5 + fail=1 + fi +done + +# ── 3. The known-untyped examples: still parse, still fail to typecheck. +# If one starts typechecking, the manifest is STALE and must be updated. +echo "== examples: known-untyped (ratchet) ==" +for n in "${EXAMPLES_KNOWN_UNTYPED[@]}"; do + f="${ROOT}/examples/${n}" + if [[ ! -f "$f" ]]; then + echo "::error::manifest lists ${n} but the file is gone"; fail=1; continue; fi + if "${BIN}" --eval "$f" >/dev/null 2>&1; then + note "$n" "NOW WORKS" + echo "::error::${n} now evaluates — good! Move it to EXAMPLES_MUST_RUN and drop it from EXAMPLES_KNOWN_UNTYPED." + fail=1 + else + note "$n" "still untyped (expected)" + fi +done + +# ── 4. Any example NOT in either list is unaccounted for. +echo "== examples: manifest covers every file ==" +for f in "${ROOT}"/examples/*.tangle; do + n="$(basename "$f")" + if ! in_list "$n" "${EXAMPLES_MUST_RUN[@]}" && ! in_list "$n" "${EXAMPLES_KNOWN_UNTYPED[@]}"; then + note "$n" "UNLISTED" + 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." + fail=1 + fi +done + +# ── 5. Conformance: valid must parse (except the recorded set); invalid must NOT. +echo "== conformance ==" +for f in "${ROOT}"/conformance/valid/*.tangle; do + n="$(basename "$f")" + if "${BIN}" "$f" >/dev/null 2>&1; then + if in_list "$n" "${CONFORMANCE_KNOWN_UNPARSED[@]}"; then + note "valid/$n" "NOW PARSES" + echo "::error::conformance/valid/${n} now parses — drop it from CONFORMANCE_KNOWN_UNPARSED." + fail=1 + else + note "valid/$n" "parse ok" + fi + else + if in_list "$n" "${CONFORMANCE_KNOWN_UNPARSED[@]}"; then + note "valid/$n" "still unparsed (expected)" + else + note "valid/$n" "PARSE FAILED" + echo "::error::conformance/valid/${n} must parse and does not"; fail=1 + fi + fi +done +for f in "${ROOT}"/conformance/invalid/*.tangle; do + n="$(basename "$f")" + if "${BIN}" "$f" >/dev/null 2>&1; then + note "invalid/$n" "PARSED (should not)" + echo "::error::conformance/invalid/${n} parsed successfully but is meant to be rejected"; fail=1 + else + note "invalid/$n" "rejected ok" + fi +done + +echo +if [[ "$fail" -ne 0 ]]; then + echo "::error::corpus drifted from the manifest — see the errors above." + exit 1 +fi +echo "Corpus matches the manifest: examples parse, the must-run set evaluates," +echo "known gaps are unchanged, and invalid programs are still rejected."