chore(ci): clear the two in-repo governance false-positives (LICENSE SPDX + trusted-base)#329
Merged
Merged
Conversation
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
hyperpolymath
marked this pull request as ready for review
June 27, 2026 18:35
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.
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@d135b05check-script regexes (fetched via raw HTTPS and verified locally, not guessed).1.
governance / Licence consistencyRoot
LICENSEis the verbatim MPL-2.0 text with no SPDX header.check-licence-consistency.shdoes:then normalises the identifier and checks it matches the manifest. Fix: prepend
SPDX-License-Identifier: MPL-2.0(normalises tompl-2.0, matchesCargo.tomllicense = "MPL-2.0"). Verified the grep now matches.2.
governance / Trusted-base reduction policycheck-trusted-base.shflags^[[:space:]]*(Axiom|Admitted|admit\.).formal/RegionEnvL1.v:17is 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-ignoreentry deliberately: the file stays fully scanned, so a genuine future axiom there is still caught — and aTRUSTED:/AXIOM:inline annotation would be false (the file really is axiom-free; that's the whole point ofRegionEnvL1.v).Not fixable here
scan / Hypatia Neurosymbolic Analysisfails on an ElixirCompileError(real_subdirs) inside thestandards/Hypatia repo — out of ephapax's reach. Flagging, not fixing.Verification
standards@d135b05).formal/RegionEnvL1.vstill compiles undercoqc 8.18.0(comment-only change).🤖 Generated with Claude Code
https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
Generated by Claude Code