You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This issue is fixed on main. The stale .hypatia-ignore entries were removed in b7c780f (#174, 2026-09-26). .hypatia-ignore now contains only its SPDX header and a note saying the ReScript entries and the removed examples/go|java|kotlin|swift paths were pruned for this issue.
How I verified it: I ran a local scan of main at b7c780f with the hypatia escript from hyperpolymath/hypatia#883 (no Actions minutes used). No banned-language finding came back after the prune, so no entry was still doing any work.
The residue from that scan is 75 findings: 2 critical, 3 high, 52 medium, 18 warn.
Severity
Rule
Location
Note
critical
believe_me
src/abi/AbsoluteZero/ABI/Proofs/DivMod.idr:92
Real proof debt
critical
believe_me
src/abi/AbsoluteZero/ABI/Layout.idr:270
Real proof debt
high
isabelle_oops
proofs/isabelle/OND.thy:16
Real proof debt
high
unwrap_without_check
src/whitespace/src/lib.rs:169
Library code
high
ada_pragma_suppress
examples/ada/balanced_ops.adb:126
These are genuine findings, and they should be fixed in the code rather than ignored.
The scan also turned up two false positives. Both were fixed in the scanner itself (hyperpolymath/hypatia#883), not by adding ignore entries here:
WH002, wiki-sync.yml: it said "safe to narrow contents: write", but scripts/wiki-sync.sh does the push that needs that permission. The rule now follows repo-local scripts. It now warns that narrowing would break the sync.
"No SECURITY.md": it fired even though SECURITY.adoc is present. Both policy checks now accept .md, .markdown, .adoc and .rst, in the repo root, .github/ or docs/.
Activity
fix: resolve repository issues, port Lean FilesystemCNO, and unify Co…
hyperpolymath commentedon Sep 30, 2026
This issue is fixed on
main. The stale.hypatia-ignoreentries were removed in b7c780f (#174, 2026-09-26)..hypatia-ignorenow contains only its SPDX header and a note saying the ReScript entries and the removedexamples/go|java|kotlin|swiftpaths were pruned for this issue.How I verified it: I ran a local scan of
mainat b7c780f with the hypatia escript from hyperpolymath/hypatia#883 (no Actions minutes used). No banned-language finding came back after the prune, so no entry was still doing any work.The residue from that scan is 75 findings: 2 critical, 3 high, 52 medium, 18 warn.
believe_mesrc/abi/AbsoluteZero/ABI/Proofs/DivMod.idr:92believe_mesrc/abi/AbsoluteZero/ABI/Layout.idr:270isabelle_oopsproofs/isabelle/OND.thy:16unwrap_without_checksrc/whitespace/src/lib.rs:169ada_pragma_suppressexamples/ada/balanced_ops.adb:126These are genuine findings, and they should be fixed in the code rather than ignored.
The scan also turned up two false positives. Both were fixed in the scanner itself (hyperpolymath/hypatia#883), not by adding ignore entries here:
wiki-sync.yml: it said "safe to narrowcontents: write", butscripts/wiki-sync.shdoes the push that needs that permission. The rule now follows repo-local scripts. It now warns that narrowing would break the sync.SECURITY.adocis present. Both policy checks now accept.md,.markdown,.adocand.rst, in the repo root,.github/ordocs/.Closing as completed.
🤖 Generated with Claude Code
https://claude.ai/code/session_01QFphKkDVB9pUDSCD4bkz65