Skip to content

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

Merged
hyperpolymath merged 1 commit into
mainfrom
chore/licence-and-deadwood
Jul 27, 2026
Merged

chore: settle the licence contradiction, drop dead code (closes #265, #266)#359
hyperpolymath merged 1 commit into
mainfrom
chore/licence-and-deadwood

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

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.txta 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

…266)

## Licence — resolves a three-way contradiction, per owner ruling

This repo declared three different licences at once. `docs/testing-and-bench-strategy.adoc`
already diagnosed it: "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".

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

- `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 link on a
  public README, contradicting both `LICENSE` and GitHub's own MPL-2.0 classification.
  Now states MPL-2.0 (code) / CC-BY-SA-4.0 (docs).
- `license = "PMPL-1.0-or-later"` -> `"MPL-2.0"` in `pixi.toml`, `stapeln.toml` and the
  five crate manifests (`ephapax-linear`, `src/ephapax-ir`, `src/ephapax-lsp`,
  `tools/ephapax-dap`, `tools/ephapax-lsp`). PMPL is not a registered SPDX identifier,
  so these were also invalid to any tool reading the manifests.
- `guix.scm`: licence -> `mpl2.0`.
- Removed `LICENSES/AGPL-3.0-or-later.txt` — added by an agent sweep, referenced by
  nothing in the tree, and inconsistent with the ruling above.

Historical and diagnostic mentions of PMPL (CHANGELOG, tech-debt notes,
testing-and-bench-strategy) are deliberately left alone: they describe the problem
rather than declare a licence.

## guix.scm — fix a genuine parse hazard

Line 2 used `// Owner: ...`, a C-style comment in a Scheme file. `//` is not a comment
in Guile, so `guix shell -f guix.scm` could not work. Now `;;`.

## Dead code and a fake gate

- **closes #265** — delete 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). No dune file, no opam file, no CI
  step, and nothing in the tree imports them.
- **closes #266** — delete `.github/workflows/boj-build.yml`. It is not an
  implementation of the cartridge; it is a trigger that POSTs to boj-server. It could
  never have worked and was reporting green regardless:
    * `http://` — plaintext, violating estate policy;
    * `boj-server.local` — an mDNS hostname, unresolvable from GitHub-hosted runners;
    * malformed JSON payload (stray escaping and an extra closing brace);
    * `continue-on-error: true`, which masked all of the above as a passing check.

Note for follow-up: with the OCaml prototype gone, the `ocaml 5.4.1` pin in
`.tool-versions` is now vestigial. Left in place deliberately — that file is the single
source of truth for the prover toolchain and is not worth churning here.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@hyperpolymath
hyperpolymath marked this pull request as ready for review July 27, 2026 18:19
@hyperpolymath
hyperpolymath merged commit bcaa977 into main Jul 27, 2026
24 of 25 checks passed
@hyperpolymath
hyperpolymath deleted the chore/licence-and-deadwood branch July 27, 2026 18:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

1 participant