From 6e8b775ab5045c601752dfdea8774a79f6e1e312 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:33:31 +0000 Subject: [PATCH] chore(ci): clear the two in-repo governance false-positives MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two governance checks have been red on every PR for reasons unrelated to any diff; both are repo-level. Fixed against the exact standards@d135b05 check regexes (fetched + verified, not guessed): - Licence consistency: root LICENSE (verbatim MPL-2.0 text) had no SPDX header. check-licence-consistency.sh greps `^SPDX-License-Identifier:` and normalises it against the manifest. Prepend `SPDX-License-Identifier: MPL-2.0` (matches Cargo.toml `license = "MPL-2.0"`). - Trusted-base reduction policy: check-trusted-base.sh flags `^[[:space:]]*(Axiom|Admitted|admit\.)`; formal/RegionEnvL1.v:17 is a PROSE comment ("Axiom budget: this file is axiom-free") that starts with "Axiom" — a false positive. Reworded to "On the axiom budget: …" so the line no longer matches. Chosen over a .trusted-base-ignore entry on purpose: the file stays fully scanned, so a genuine future axiom there is still caught (and a TRUSTED:/AXIOM: annotation would be false — the file really is axiom-free). Hypatia's own Elixir CompileError lives in the standards repo and is out of ephapax's reach. RegionEnvL1.v still compiles (comment-only change). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL --- LICENSE | 2 ++ formal/RegionEnvL1.v | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/LICENSE b/LICENSE index 14e2f777..2a8b9601 100644 --- a/LICENSE +++ b/LICENSE @@ -1,3 +1,5 @@ +SPDX-License-Identifier: MPL-2.0 + Mozilla Public License Version 2.0 ================================== diff --git a/formal/RegionEnvL1.v b/formal/RegionEnvL1.v index d7fcc6fa..7ba0d421 100644 --- a/formal/RegionEnvL1.v +++ b/formal/RegionEnvL1.v @@ -14,7 +14,7 @@ [region_name -> nat] (re-entry depth per region; 0 = dead), reasoned up to a **pointwise-equality setoid** [renv_eq]. - Axiom budget: this file is axiom-free. We use a setoid relation + On the axiom budget: this file is axiom-free. We use a setoid relation ([renv_eq]) rather than [functional_extensionality], so [Print Assumptions] stays clean — order-insensitivity is *definitional* (the carrier is a function; permutation collapses to [renv_eq]),