chore: settle the licence contradiction, drop dead code (closes #265, #266) (#359)

## Licence — a three-way contradiction, now settled

This repo declared **three different licences at once**. Its own
`docs/testing-and-bench-strategy.adoc` already diagnosed it and said the
fix needed an
owner decision:

> "Licence single-source: `guix/pixi/stapeln` say PMPL-1.0-or-later, 255
headers say
> MPL-2.0, only `LICENSES/MPL-2.0.txt` exists — a 3-way contradiction
... any FIX is
> owner-manual, file-by-file"

**Owner ruling applied: MPL-2.0 for code, CC-BY-SA-4.0 for
documentation.**

The most visible symptom: `README.adoc` declared `PMPL-1.0-or-later` as
the primary
licence and linked `LICENSES/PMPL-1.0-or-later.txt` — **a file that does
not exist**. A
broken licence link on a public README, contradicting both `LICENSE` and
GitHub's own
MPL-2.0 classification.

| Where | Was | Now |
|---|---|---|
| `README.adoc` | PMPL primary, MPL "fallback", broken link | MPL-2.0
(code) / CC-BY-SA-4.0 (docs) |
| `pixi.toml`, `stapeln.toml` | `PMPL-1.0-or-later` | `MPL-2.0` |
| 5 crate manifests | `PMPL-1.0-or-later` | `MPL-2.0` |
| `guix.scm` | custom PMPL constructor | `mpl2.0` |
| `LICENSES/AGPL-3.0-or-later.txt` | present, referenced by nothing |
removed |

PMPL is **not a registered SPDX identifier**, so those manifest fields
were invalid to
any tool that read them, not merely inconsistent.

Historical/diagnostic mentions of PMPL (CHANGELOG, tech-debt notes, the
strategy doc
quoted above) are deliberately left alone — they *describe* the problem
rather than
declare a licence.

GitHub already classified this repo MPL-2.0, so no change was needed
there; this makes
the tree agree with it.

## `guix.scm` — a real parse hazard

Line 2 was `// Owner: ...` — a **C-style comment in a Scheme file**.
`//` is not a
comment in Guile, so `guix shell -f guix.scm` could not have worked. Now
`;;`.

## Dead code and a fake gate

**closes #265** — deletes the orphaned OCaml "Choreographic Sessions"
prototype:
`src/lexer.mll`, `src/parser.mli`, `src/parser.mly`,
`test/test_typecheck.ml`, and the
stray `test_minimal.ml` in the repo root. Verified fully orphaned: no
dune file, no opam
file, no CI step, nothing in the tree imports them.

**closes #266** — deletes `.github/workflows/boj-build.yml`. To answer
the question in
the issue directly: it is **not** an implementation of the cartridge, it
is a *trigger*
that POSTs to boj-server asking it to build this repo. It could never
have worked, and
was reporting green anyway:

- `http://` — plaintext, violating estate policy
- `boj-server.local` — an **mDNS hostname**, unresolvable from
GitHub-hosted runners
- **malformed JSON** payload (stray escaping plus an extra closing
brace)
- `continue-on-error: true` — which masked all three as a passing check

That combination is a textbook fake gate: it has been showing "BoJ
Server Build Trigger
success" on the board while doing nothing.

## Follow-up, not done here

With the OCaml prototype gone, the `ocaml 5.4.1` pin in `.tool-versions`
is vestigial.
Left in place deliberately — that file is the single source of truth for
the prover
toolchain and isn't worth churning in this PR.

## Verification

- `git grep PMPL -- '*.toml' '*.scm' '*.a2ml'` returns nothing.
- `LICENSES/` now contains exactly `MPL-2.0.txt` and `CC-BY-SA-4.0.txt`,
matching what
the tree actually declares — `reuse lint` was previously guaranteed to
fail on the
  missing PMPL file.
- Governance's "Licence consistency" job should stay green; the
workflow-security linter
  loses one file to check.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

.github/workflows/boj-build.yml

@@ -69,4 +69,4 @@ After reading this file, demonstrate understanding by stating:
 - **Format Version:** 1.0.0
 - **Last Updated:** 2026-04-23
 - **Maintained By:** Jonathan D.A. Jewell (hyperpolymath)
-- **License:** PMPL-1.0-or-later
+- **License:** MPL-2.0 (code), CC-BY-SA-4.0 (documentation)

0-AI-MANIFEST.a2ml

@@ -800,9 +800,12 @@ See `formal/PRESERVATION-DESIGN.md §12` and `PROOF-NEEDS.md §3`.
 
 == Licence
 
-PMPL-1.0-or-later — see link:LICENSES/PMPL-1.0-or-later.txt[PMPL-1.0-or-later.txt].
+Code is `MPL-2.0` — see link:LICENSES/MPL-2.0.txt[MPL-2.0.txt].
 
-MPL-2.0 fallback available — see link:LICENSES/MPL-2.0.txt[MPL-2.0.txt].
+Documentation is `CC-BY-SA-4.0` — see link:LICENSES/CC-BY-SA-4.0.txt[CC-BY-SA-4.0.txt].
+
+Every file carries its own `SPDX-License-Identifier:` header, so the applicable
+licence is always the one named in the file itself.
 
 == Author
 

LICENSES/AGPL-3.0-or-later.txt

@@ -7,7 +7,7 @@ name = "ephapax-linear"
 version = "0.1.0"
 edition = "2021"
 rust-version = "1.83"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 repository = "https://github.com/hyperpolymath/ephapax"
 description = "Standalone linear/affine discipline checker for ephapax — dual grammars with full substructural focusing"

README.adoc

@@ -1,5 +1,5 @@
 ; SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+;; Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ;; guix.scm — GNU Guix package definition for ephapax
 ;; Usage: guix shell -f guix.scm
 
@@ -15,5 +15,4 @@
   (synopsis "ephapax")
   (description "ephapax — part of the hyperpolymath ecosystem.")
   (home-page "https://github.com/hyperpolymath/ephapax")
-  (license ((@@ (guix licenses) license) "PMPL-1.0-or-later"
-             "https://github.com/hyperpolymath/palimpsest-license")))
+  (license mpl2.0))

ephapax-linear/Cargo.toml

@@ -11,6 +11,6 @@ See README.adoc for overview.
 - `just heal` — attempt auto-repair
 
 ## Quick Context
-- License: PMPL-1.0-or-later
+- License: MPL-2.0 (code), CC-BY-SA-4.0 (documentation)
 - Part of hyperpolymath ecosystem
 - See EXPLAINME.adoc for architecture

guix.scm

@@ -11,6 +11,6 @@ See README.adoc for overview.
 - `just heal` — attempt auto-repair
 
 ## Quick Context
-- License: PMPL-1.0-or-later
+- License: MPL-2.0 (code), CC-BY-SA-4.0 (documentation)
 - Part of hyperpolymath ecosystem
 - See EXPLAINME.adoc for architecture

llm-warmup-dev.md

@@ -8,7 +8,7 @@ name = "ephapax"
 version = "0.1.0"
 description = "A dyadic linear/affine type system language targeting WebAssembly"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 channels = ["conda-forge"]
 platforms = ["linux-64", "osx-arm64", "osx-64"]
 

llm-warmup-user.md

@@ -6,7 +6,7 @@
 name = "ephapax-ir"
 version = "0.1.0"
 edition = "2021"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 
 [dependencies]
 smol_str = { workspace = true }