Skip to content

Commit bb83b7e

Browse files
chore(ci): clear the two in-repo governance false-positives (LICENSE SPDX + trusted-base) (#329)
## Summary Two governance checks have been red on **every** PR (#322#324) for reasons unrelated to any diff — both are repo-level. This clears the two that are in ephapax's control. Fixes were derived from the **exact `standards@d135b05` check-script regexes** (fetched via raw HTTPS and verified locally, not guessed). ### 1. `governance / Licence consistency` Root `LICENSE` is the verbatim MPL-2.0 text with **no SPDX header**. `check-licence-consistency.sh` does: ```sh grep -m1 -E '^[[:space:]]*SPDX-License-Identifier:' "$lic_file" ``` then normalises the identifier and checks it matches the manifest. **Fix:** prepend `SPDX-License-Identifier: MPL-2.0` (normalises to `mpl-2.0`, matches `Cargo.toml` `license = "MPL-2.0"`). Verified the grep now matches. ### 2. `governance / 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 happens to start with "Axiom". A false positive. **Fix:** reword to *"On the axiom budget: …"* so the line no longer matches (verified). Chosen over a `.trusted-base-ignore` entry deliberately: the file stays **fully scanned**, so a genuine future axiom there is still caught — and a `TRUSTED:`/`AXIOM:` inline annotation would be *false* (the file really is axiom-free; that's the whole point of `RegionEnvL1.v`). ## Not fixable here `scan / Hypatia Neurosymbolic Analysis` fails on an Elixir `CompileError` (`real_subdirs`) **inside the `standards`/Hypatia repo** — out of ephapax's reach. Flagging, not fixing. ## Verification - Both fixes checked against the actual fetched regexes (`standards@d135b05`). - `formal/RegionEnvL1.v` still compiles under `coqc 8.18.0` (comment-only change). - 2 files, +3/−1. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL --- _Generated by [Claude Code](https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent e81c9f8 commit bb83b7e

2 files changed

Lines changed: 3 additions & 1 deletion

File tree

LICENSE

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
SPDX-License-Identifier: MPL-2.0
2+
13
Mozilla Public License Version 2.0
24
==================================
35

formal/RegionEnvL1.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
[region_name -> nat] (re-entry depth per region; 0 = dead), reasoned
1515
up to a **pointwise-equality setoid** [renv_eq].
1616
17-
Axiom budget: this file is axiom-free. We use a setoid relation
17+
On the axiom budget: this file is axiom-free. We use a setoid relation
1818
([renv_eq]) rather than [functional_extensionality], so [Print
1919
Assumptions] stays clean — order-insensitivity is *definitional*
2020
(the carrier is a function; permutation collapses to [renv_eq]),

0 commit comments

Comments
 (0)