chore(licence): reconcile SPDX headers to the AGPL ruling — three-part split - #354
Merged
Merged
Conversation
This comment has been minimized.
This comment has been minimized.
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
hyperpolymath
dismissed
gitar-bot[bot]’s stale review
August 7, 2026 13:42
The base branch was changed.
…t split
Owner ruling: ECHIDNA is AGPL-3.0-or-later. Until now LICENSE and
Cargo.toml said so while every source file granted MPL-2.0, NOTICE
described the project as MPL, and .reuse/dep5 claimed PMPL-1.0 AND
Palimpsest-0.6. Since per-file SPDX headers are themselves a licence
grant, a recipient could have taken the tree under MPL — which has no
network clause. This reconciles the tree to the ruling.
Three parts, deliberately:
code -> AGPL-3.0-or-later (594 files + 6 duals)
documentation -> CC-BY-SA-4.0 (92 files + 1 dual)
echidna-playground/ -> MPL-2.0, UNCHANGED
The playground is not relicensed: it carries contributions attributed
to 'Coq-Jr Contributors', and relicensing another party's contribution
needs their consent. It does not need relicensing — MPL-2.0 s3.3 names
the GNU licences (incl. AGPL-3.0+) as Secondary Licenses, so MPL files
combine into an AGPL work and distribute under the AGPL while remaining
individually available under MPL. Verified no file carries the Exhibit B
'Incompatible With Secondary Licenses' notice that would prevent this;
the only match in the tree is inside LICENSES/MPL-2.0.txt, which is the
licence's own boilerplate.
Method — identifiers were REPLACED IN PLACE on SPDX-License-Identifier
lines only, never inserted. A previous estate sweep mis-licensed files
by imposing a header where a different one already sat further down.
Consequences of that choice:
- prose mentioning MPL is untouched
- the 7 files offering Palimpsest-0.6 keep that grant
('AGPL-3.0-or-later OR/AND Palimpsest-0.6') — dropping half of a
dual would withdraw a licence the owner granted
- 3 workflows carrying PMPL-1.0-or-later folded into AGPL
- SPDX stays on line 1 of all 30 workflows (linter greps head -1)
Excluded deliberately: LICENSES/ and docs/legal/ — licence texts and
their exhibits are reference documents, and restating the licensing of
a licence text is confusing.
Also:
- NOTICE rewritten: it previously said 'licensed under MPL-2.0' while
citing LICENSE (AGPL) as its full text. Now sets out the three-part
split, the MPL s3.3 compatibility argument, and the licence history.
- .reuse/dep5 rewritten to match reality.
- LICENSE: dropped the two prepended SPDX lines, making it byte-identical
to LICENSES/AGPL-3.0-or-later.txt. GitHub reported the licence as
'Other' because the prepend stopped its detector matching the body.
Known gap, unchanged by this commit: Palimpsest-0.6 has no licence text
in this repository or the estate, so those 7 dual grants reference an
unresolvable identifier. Recorded in docs/DEBT.md rather than resolved
by dropping the grant.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… DEBT Follows the header reconciliation in the previous commit. Surfaces that warned readers the licence was unresolved now state the three-part split and the MPL s3.3 compatibility argument instead. DEBT.md P0 rewritten from 'four licences at once' to RESOLVED, with the four verification commands that now come back clean — all re-run before committing: - MPL outside playground/LICENSES/docs-legal: 0 - code identifiers: AGPL-3.0-or-later (+1 preserved Palimpsest dual) - playground: 35 files still MPL-2.0 - Palimpsest text present anywhere: 0 A residual entry replaces it: Palimpsest-0.6 is granted by 7 files but has no licence text in this repo or the estate, so REUSE cannot resolve it. The grants were kept, not dropped — withdrawing half of a dual licence is the owner's call, not a documentation one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…p cannot see
Owner ruling: Palimpsest is not a licence grant in this repository.
CONTRIBUTING.adoc already said so — the Palimpsest licence proper is the
legal licence only on palimpsest-license, palimpsest-plasma and
(prospectively) consent-aware-http, and in ECHIDNA it is an ETHICAL
FRAMEWORK reference, orthogonal to the SPDX choice. Version 0.6 is also
superseded by the hyperpolymath/palimpsest-license repository. The dual
SPDX identifiers were therefore drift, not a deliberate grant.
Removed from all 29 files. The framework reference is preserved and
CONTRIBUTING.adoc + NOTICE now state explicitly that it is not a grant,
so it cannot drift back silently. Deliberately untouched:
training_data/proof_states_v2.jsonl (SPDX strings there are scraped
CORPUS CONTENT — proof goals harvested from files; editing them would
corrupt the training data) and docs/legal/ (licence reference texts).
Removing the Palimpsest half exposed three further classes that the
SPDX-header sweep could not have caught, all now fixed:
1. STALE MIT. src/rescript/{.gitignore,styles/main.css,tailwind.config.js}
declared 'MIT OR Palimpsest-0.6', predating even the MPL migration.
Dropping only the Palimpsest half would have left them MIT.
2. MACHINE-READABLE LICENCE FIELDS — what packaging and tooling actually
read, and carrying no SPDX line to match. Ten declared MPL-2.0:
docs-site/.well-known/aibdp.json (served on the site), stapeln.toml,
container/manifest.toml, three Ada alire.toml manifests, two Idris2
.ipkg manifests, descriptiles/META.a2ml, 0-AI-MANIFEST.a2ml — plus a
NESTED src/rescript/.reuse/dep5 declaring MIT OR Palimpsest-0.6 for
the UI sub-tree.
3. OCI IMAGE LABELS — 16 LABEL org.opencontainers.image.licenses=MPL-2.0
across Containerfile, container/Containerfile and .containerization/
(11 in Containerfile.wave3, one per per-prover stage). These are baked
into every image published to ghcr.io and read by registries, SBOM
generators and supply-chain scanners, so the wrong value propagated
downstream of the repository entirely.
Also: src/rescript/src/Main.res RENDERED 'MIT OR Palimpsest-0.6 License'
in the UI — a false licence statement shown to users.
docs/DEBT.md records all of it with a detector that greps by licence
VALUE rather than by file type, which is what caught the last three
classes.
Verified: exhaustive sweep for MPL/MIT/Palimpsest as a licence value
returns nothing outside echidna-playground/; SPDX still line 1 on all
30 workflows.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ReScript is a banned language under the estate language policy, with
AffineScript-TEA as the replacement. This removes echidna's own ReScript:
src/rescript/ 24 files (the UI)
src/provers/ 13 files (.res prover clients — orphaned; nothing
outside reports/ and the hypatia baseline referenced
them)
echidna-playground/ retains its 8 .res files: that sub-project carries
contributions attributed to Coq-Jr Contributors, so removing their code
is a separate decision, not a language-policy cleanup.
Build and CI references updated rather than left dangling:
- Justfile: build-ui/watch-ui/dev-ui replaced. build-ui now FAILS with
a clear message instead of silently doing nothing — the
AffineScript-TEA pipeline is not wired yet (issues #117, #266,
missing Http::fetch / Async / Json primitives). serve-ui and the gui
recipe serve the static shell at src/ui/public/ instead.
- deno.json: dev:ui/build:ui -> serve:ui; dropped node_modules excludes
- codecov.yml: dropped the rescript flag and rescript_ui component
- .gitlab-ci.yml: dropped the build-rescript job
- .echidnabot.toml: secondary_languages rescript -> affinescript
Not fixed here: .gitlab-ci.yml does not parse as YAML, at a line
untouched by this change (a bare % inside an unquoted shell command).
Verified pre-existing — HEAD fails identically at the same line before
the removal shifted it. Recorded in docs/DEBT.md.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ds work
Owner ruling. Palimpsest is MPL-2.0 with ethical provisions layered on
top, so MPL-2.0 is the faithful reduction wherever the Palimpsest layer
is not being asserted — and MPL is what a standards body can work with,
where AGPL's strong copyleft would obstruct adoption and re-publication.
Split is now four parts (was three):
application code AGPL-3.0-or-later 756 files
SPECIFICATION SURFACE MPL-2.0 .machine_readable/ (A2ML
descriptiles, contractiles, K9 configs,
anchors, policies), 0-AI-MANIFEST.a2ml,
package + container manifests, and the OCI
image labels emitted by stapeln / svalinn
documentation CC-BY-SA-4.0 101 files
echidna-playground/ MPL-2.0 unchanged
MPL-2.0 total: 131 files.
Files that previously offered Palimpsest-0.6 now carry MPL-2.0 rather
than AGPL, per the same reasoning.
The AGPL umbrella still governs the combined work — MPL s3.3 (Secondary
Licenses) is what lets the MPL parts sit inside it — but each MPL part
remains individually available under MPL, which is the property the
standards path needs.
NOTICE, .reuse/dep5, CONTRIBUTING.adoc, README, CLAUDE.md, humans.txt,
docs/DEBT.md and both wiki pages restated for four parts, each spelling
out WHY the specification surface is weak-copyleft rather than leaving a
future reader to guess and 'fix' it back to AGPL.
Verified: SPDX still line 1 on all 30 workflows.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
force-pushed
the
chore/licence-reconciliation-agpl
branch
from
August 7, 2026 13:43
f634828 to
d1da40d
Compare
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
There was a problem hiding this comment.
Hypatia found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Applies your ruling — AGPL for echidna — and implements the two boundary decisions: the playground stays MPL-2.0, and the documentation surface normalises to CC-BY-SA-4.0.
Stacked on #352 (base is
docs/full-documentation-refresh, notmain) because it retires that PR's P0 debt entry and rewrites the licence warnings it added. Merge #352 first; this then targetsmainautomatically.Answer to the compatibility question
Yes — and in exactly the direction needed. MPL-2.0 §3.3 designates the GNU licences, including AGPL-3.0+, as "Secondary Licenses": MPL files can be combined into an AGPL work and the combined work distributed under AGPL, while those files individually remain available under MPL. I verified no file carries the Exhibit B
Incompatible With Secondary Licensesnotice that would break this — the only match in the tree is insideLICENSES/MPL-2.0.txt, which is the licence's own boilerplate.What I found looking for the components you expected
You anticipated borrowed code from gossamer, snifs and similar. In this repo there is essentially none:
crates/shared with other estate reposproven,burble,gossamer")The only externally-attributed code is
echidna-playground/src/*.res("Coq-Jr Contributors"). So the MPL headers everywhere else were historical residue from the MIT/Palimpsest → MPL migration, not a marker of borrowed code — which is what makes relicensing them straightforward: you hold the copyright.The split
src/,crates/,ffi/,proofs/,spark/,verification/, build system, CI, machine-readable metadatadocs/, top-level.md/.adocechidna-playground/Method — why this isn't the sweep that went wrong before
Identifiers were replaced in place on
SPDX-License-Identifier:lines only, never inserted. A previous estate sweep mis-licensed files by imposing a header where a different one already sat further down the file. Consequences:Palimpsest-0.6keep that grant (AGPL-3.0-or-later OR/AND Palimpsest-0.6) — dropping half of a dual withdraws a permission you granted, which isn't a documentation decisionPMPL-1.0-or-laterfolded into AGPLhead -1)Excluded deliberately:
LICENSES/anddocs/legal/— restating the licensing of a licence text is confusing.Supporting files
NOTICErewritten. It previously said "licensed under the Mozilla Public License" while citingLICENSE— which is AGPL — as its full text. Now states the split, the §3.3 argument, and the licence history..reuse/dep5rewritten; it claimedPMPL-1.0 AND Palimpsest-0.6for everything.LICENSE: dropped two prepended SPDX lines, making it byte-identical toLICENSES/AGPL-3.0-or-later.txt. That prepend is why GitHub reported the licence as "Other"; expect it to detect AGPL-3.0 after merge.Verification (all re-run before commit)
One thing left for you
Palimpsest-0.6has no licence text — not in this repo, not instandards/LICENSES/. Seven files grant it, so REUSE cannot resolve the identifier. I kept the grants and recorded it as the residual P0 entry. Either supplyLICENSES/Palimpsest-0.6.txt, or decide the grant is retired and remove it deliberately. (NotePMPL-1.0-or-laterdoes have a text — different identifier.)🤖 Generated with Claude Code