feat(tg-7): == on braids decides braid-group equivalence (#50 ruling)
#2
Workflow file for this run
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
| # SPDX-License-Identifier: MPL-2.0 | |
| # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | |
| # | |
| # OCaml compiler build + test gate. | |
| # | |
| # ── Why this exists ──────────────────────────────────────────────────────── | |
| # Until 2026-07-29 the OCaml compiler — the lexer, parser, typechecker and | |
| # interpreter, plus a test suite of well over 4,000 assertions (TG-3 1008, | |
| # TG-5 189, TG-7 2220, TG-8 2311, and the parser/typecheck/eval/e2e/property/ | |
| # round-trip suites) — was **not built or run by CI at all**. Only the Lean | |
| # proofs were gated. A semantics change to `eval.ml` could therefore land | |
| # fully green with nothing having compiled it. | |
| # | |
| # That gap was found while implementing the TG-7 ruling (#50), which changes | |
| # what `==` MEANS on braids. A change of that weight must be gated, so this | |
| # workflow makes `dune build` + `dune test` the oracle: any PR that breaks the | |
| # compiler or a single assertion fails here rather than landing silently. | |
| # | |
| # ── Toolchain choice ─────────────────────────────────────────────────────── | |
| # Debian/Ubuntu packages (`ocaml-dune`, `menhir`) rather than an OCaml setup | |
| # ACTION, deliberately: it adds no new third-party action pin to the estate's | |
| # allowlist, and no pin that can later become unresolvable — the failure mode | |
| # that produces a workflow with NO check run at all. | |
| name: OCaml CI | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'compiler/**' | |
| - '.github/workflows/ocaml-ci.yml' | |
| pull_request: | |
| paths: | |
| - 'compiler/**' | |
| - '.github/workflows/ocaml-ci.yml' | |
| workflow_dispatch: {} | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| build-and-test: | |
| name: Build + test the OCaml compiler | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Install OCaml toolchain | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update -qq | |
| sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir | |
| ocaml -version | |
| dune --version | |
| menhir --version | |
| - name: Build | |
| working-directory: compiler | |
| run: dune build | |
| - name: Test | |
| working-directory: compiler | |
| run: | | |
| set -euo pipefail | |
| # `dune test` exits non-zero if any suite fails. Also fail on any | |
| # "FAIL" line: several suites print their own tally and would | |
| # otherwise report failures while still exiting 0. | |
| dune test --force 2>&1 | tee /tmp/dune-test.log | |
| # Match a FAIL *marker* only: "FAIL" followed by ':' or whitespace. | |
| # NOT case-insensitive, and NOT bare "FAIL" — several suites print a | |
| # "Failed: 0" tally, which a looser pattern flags as a failure. (It | |
| # did: this gate's first run went red on a suite reporting zero | |
| # failures. A gate that cries wolf is worse than no gate.) | |
| if grep -qE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log; then | |
| echo "::error::A test reported FAIL — see the log above." | |
| grep -nE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log | head -20 | |
| exit 1 | |
| fi | |
| # Nonzero tallies, in either shape the suites use. | |
| if grep -qE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log; then | |
| echo "::error::A suite reported a nonzero failure count." | |
| grep -nE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log | |
| exit 1 | |
| fi | |
| echo "OCaml compiler: build + all suites GREEN." | |
| - name: TG-7 semantics guard | |
| working-directory: compiler | |
| run: | | |
| set -euo pipefail | |
| # The TG-7 ruling (#50) is only real if `==` actually decides | |
| # braid-group equality. These cases are FALSE under list equality, | |
| # so their presence and passing is what distinguishes the two | |
| # semantics — guard against a silent revert. | |
| missing=0 | |
| for t in "braid relation s1.s2.s1 == s2.s1.s2" \ | |
| "far commutation s1.s3 == s3.s1" \ | |
| "non-equivalent braids still compare false"; do | |
| grep -qF "$t" test/test_eval.ml || { echo "::error::TG-7 test missing: $t"; missing=1; } | |
| done | |
| [ "$missing" -eq 0 ] || exit 1 | |
| echo "TG-7 semantics tests present." |