|
| 1 | +# SPDX-License-Identifier: MPL-2.0 |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# OCaml compiler build + test gate. |
| 5 | +# |
| 6 | +# ── Why this exists ──────────────────────────────────────────────────────── |
| 7 | +# Until 2026-07-29 the OCaml compiler — the lexer, parser, typechecker and |
| 8 | +# interpreter, plus a test suite of well over 4,000 assertions (TG-3 1008, |
| 9 | +# TG-5 189, TG-7 2220, TG-8 2311, and the parser/typecheck/eval/e2e/property/ |
| 10 | +# round-trip suites) — was **not built or run by CI at all**. Only the Lean |
| 11 | +# proofs were gated. A semantics change to `eval.ml` could therefore land |
| 12 | +# fully green with nothing having compiled it. |
| 13 | +# |
| 14 | +# That gap was found while implementing the TG-7 ruling (#50), which changes |
| 15 | +# what `==` MEANS on braids. A change of that weight must be gated, so this |
| 16 | +# workflow makes `dune build` + `dune test` the oracle: any PR that breaks the |
| 17 | +# compiler or a single assertion fails here rather than landing silently. |
| 18 | +# |
| 19 | +# ── Toolchain choice ─────────────────────────────────────────────────────── |
| 20 | +# Debian/Ubuntu packages (`ocaml-dune`, `menhir`) rather than an OCaml setup |
| 21 | +# ACTION, deliberately: it adds no new third-party action pin to the estate's |
| 22 | +# allowlist, and no pin that can later become unresolvable — the failure mode |
| 23 | +# that produces a workflow with NO check run at all. |
| 24 | + |
| 25 | +name: OCaml CI |
| 26 | + |
| 27 | +on: |
| 28 | + push: |
| 29 | + branches: [main] |
| 30 | + paths: |
| 31 | + - 'compiler/**' |
| 32 | + - '.github/workflows/ocaml-ci.yml' |
| 33 | + pull_request: |
| 34 | + paths: |
| 35 | + - 'compiler/**' |
| 36 | + - '.github/workflows/ocaml-ci.yml' |
| 37 | + workflow_dispatch: {} |
| 38 | + |
| 39 | +permissions: |
| 40 | + contents: read |
| 41 | + |
| 42 | +concurrency: |
| 43 | + group: ${{ github.workflow }}-${{ github.ref }} |
| 44 | + cancel-in-progress: true |
| 45 | + |
| 46 | +jobs: |
| 47 | + build-and-test: |
| 48 | + name: Build + test the OCaml compiler |
| 49 | + runs-on: ubuntu-latest |
| 50 | + timeout-minutes: 20 |
| 51 | + steps: |
| 52 | + - name: Checkout |
| 53 | + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
| 54 | + with: |
| 55 | + persist-credentials: false |
| 56 | + |
| 57 | + - name: Install OCaml toolchain |
| 58 | + run: | |
| 59 | + set -euo pipefail |
| 60 | + sudo apt-get update -qq |
| 61 | + sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir |
| 62 | + ocaml -version |
| 63 | + dune --version |
| 64 | + menhir --version |
| 65 | +
|
| 66 | + - name: Build |
| 67 | + working-directory: compiler |
| 68 | + run: dune build |
| 69 | + |
| 70 | + - name: Test |
| 71 | + working-directory: compiler |
| 72 | + run: | |
| 73 | + set -euo pipefail |
| 74 | + # `dune test` exits non-zero if any suite fails. Also fail on any |
| 75 | + # "FAIL" line: several suites print their own tally and would |
| 76 | + # otherwise report failures while still exiting 0. |
| 77 | + dune test --force 2>&1 | tee /tmp/dune-test.log |
| 78 | + # Match a FAIL *marker* only: "FAIL" followed by ':' or whitespace. |
| 79 | + # NOT case-insensitive, and NOT bare "FAIL" — several suites print a |
| 80 | + # "Failed: 0" tally, which a looser pattern flags as a failure. (It |
| 81 | + # did: this gate's first run went red on a suite reporting zero |
| 82 | + # failures. A gate that cries wolf is worse than no gate.) |
| 83 | + if grep -qE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log; then |
| 84 | + echo "::error::A test reported FAIL — see the log above." |
| 85 | + grep -nE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log | head -20 |
| 86 | + exit 1 |
| 87 | + fi |
| 88 | + # Nonzero tallies, in either shape the suites use. |
| 89 | + if grep -qE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log; then |
| 90 | + echo "::error::A suite reported a nonzero failure count." |
| 91 | + grep -nE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log |
| 92 | + exit 1 |
| 93 | + fi |
| 94 | + echo "OCaml compiler: build + all suites GREEN." |
| 95 | +
|
| 96 | + - name: TG-7 semantics guard |
| 97 | + working-directory: compiler |
| 98 | + run: | |
| 99 | + set -euo pipefail |
| 100 | + # The TG-7 ruling (#50) is only real if `==` actually decides |
| 101 | + # braid-group equality. These cases are FALSE under list equality, |
| 102 | + # so their presence and passing is what distinguishes the two |
| 103 | + # semantics — guard against a silent revert. |
| 104 | + missing=0 |
| 105 | + for t in "braid relation s1.s2.s1 == s2.s1.s2" \ |
| 106 | + "far commutation s1.s3 == s3.s1" \ |
| 107 | + "non-equivalent braids still compare false"; do |
| 108 | + grep -qF "$t" test/test_eval.ml || { echo "::error::TG-7 test missing: $t"; missing=1; } |
| 109 | + done |
| 110 | + [ "$missing" -eq 0 ] || exit 1 |
| 111 | + echo "TG-7 semantics tests present." |
0 commit comments