From bfaef6a79657e56039e3acb34f875e4d122249a6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 04:37:51 +0000 Subject: [PATCH] fix(license): correct 3 stale PMPL-1.0-or-later declarations -> MPL-2.0 absolute-zero is a sole-owner repo -> MPL-2.0 (its SPDX *headers* are already correct). Three *body* declarations still named the banned PMPL-1.0-or-later, contradicting the headers and the repo's own CLAUDE.md policy ("MPL-2.0 only -- never PMPL-1.0 / PMPL-1.0-or-later"): - .well-known/ai.txt License: ... - .well-known/humans.txt Standards: ... - absolute-zero-abi.ipkg license = ... Also updated PROOF-STATUS.adoc's flag note to reflect the .ipkg fix. NOT touched (legitimate references / history -- a blind sweep would have corrupted these): the CLAUDE.md banned-licence policy table, Glossary.md ("PMPL is the FORMER licence; current is MPL-2.0"), CHANGELOG/AUDIT history, ROADMAP items, and docs/archive/* (one of which contains the old sed-sweep command itself). Per-file, owner-approved. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn --- .well-known/ai.txt | 2 +- .well-known/humans.txt | 2 +- PROOF-STATUS.adoc | 4 ++-- absolute-zero-abi.ipkg | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.well-known/ai.txt b/.well-known/ai.txt index 900c311..557c42a 100644 --- a/.well-known/ai.txt +++ b/.well-known/ai.txt @@ -10,5 +10,5 @@ Roadmap: /ROADMAP.adoc Allow: training-with-attribution Allow: documentation-summarisation Disallow: closed-source-redistribution -License: PMPL-1.0-or-later +License: MPL-2.0 Contact: developer@joshuajewell.dev diff --git a/.well-known/humans.txt b/.well-known/humans.txt index 49d241c..4a5cdc0 100644 --- a/.well-known/humans.txt +++ b/.well-known/humans.txt @@ -11,5 +11,5 @@ Contributors: see git log + docs/MAINTAINERS.adoc /* SITE */ Last update: 2026-05-25 -Standards: PMPL-1.0-or-later, RSR (Rhodium Standard Repository) compliant +Standards: MPL-2.0, RSR (Rhodium Standard Repository) compliant Components: Coq, Lean 4, Z3, Agda, Isabelle, Mizar, Idris2, ReScript, Rust diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 18a07f3..9688639 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -49,8 +49,8 @@ repo build) covers `common` + `malbolge`; the full set builds with the per-area `Layout.idr`/`Foreign.idr` `--check` individually but `Types.idr`/`Proofs/DivMod.idr` report module-name/file-path mismatches. This is the same template-scaffold issue as `typell`; fixing it is a package-restructuring task (align module names ↔ paths ↔ -`sourcedir`), deferred. *Also flagged: the `.ipkg` SPDX is `PMPL-1.0-or-later`, -which is a licence-policy item for the owner (sole-owner repos use MPL-2.0).* +`sourcedir`), deferred. *(The `.ipkg` `license` field — previously +`PMPL-1.0-or-later` — has been corrected to `MPL-2.0` per the sole-owner policy.)* == Lean — NOT verified here (requires Mathlib) diff --git a/absolute-zero-abi.ipkg b/absolute-zero-abi.ipkg index 99f0ab9..93cf631 100644 --- a/absolute-zero-abi.ipkg +++ b/absolute-zero-abi.ipkg @@ -3,7 +3,7 @@ package absolute-zero-abi version = 0.1.0 authors = "Jonathan D. A. Jewell" -license = "PMPL-1.0-or-later" +license = "MPL-2.0" opts = "--ignore-missing-ipkg"