Repository navigation
ci(antipattern): fix top-level dir + benchmark/lsp filename matching - #50
Merged
Merged
Conversation
…lename allowlists
4 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 14, 2026
## Summary
Adds three quality gate scripts for the BoJ stack:
- **`scripts/typecheck-proofs.sh`**: runs `idris2 --find-ipkg --check`
on every `.idr` file under `src/abi/` and `cartridges/*/abi/`; reports
PASS/FAIL per file; exits 1 if any FAIL
- **`scripts/check-trusted-base.sh`**: counts non-comment `believe_me`
calls in `SafetyLemmas.idr`; exits 1 if count != 5 (the declared axiom
budget); currently **PASS 5/5**
- **`tests/truthfulness_check.sh`**: finds all cartridges with
`available:true` across boj-server and sibling boj-server-cartridges,
invokes `boj-invoke` on each first tool, fails if result is
`{"status":"stub"}`; currently **PASS=1 (textkit-mcp encode_base64),
SKIP=264**
Also fixes the pre-commit hook's `boj-*` AGPL classification heuristic —
`boj-server` is `hyperpolymath/boj-server` (MPL-2.0), not a son-shared
AGPL repo. Updated to only require AGPL when the `boj-*` repo actually
has an AGPL LICENSE file.
## Gate results
```
check-trusted-base.sh:
Axiom count: 5 (expected 5)
PASS: trusted-base axiom count correct (5/5)
truthfulness_check.sh:
PASS textkit-mcp (encode_base64): {"base64":""}
Results: PASS=1 FAIL=0 SKIP=264
PASS: all available cartridges are truthful
```
Note: `typecheck-proofs.sh` surfaces 3 pre-existing failures in core ABI
modules (CartridgeDispatch parser error, SafeCORS unsolved constraint,
SafePromptInjection unsolved constraint). These predate this PR;
textkit-mcp's new ABI proof passes cleanly.
## Test plan
- [ ] `bash scripts/check-trusted-base.sh` → PASS 5/5
- [ ] `bash tests/truthfulness_check.sh` → PASS=1 FAIL=0 (textkit-mcp)
- [ ] `bash scripts/typecheck-proofs.sh` → shows pre-existing failures
in core ABI (separate debt); textkit-mcp PASS
- [ ] Sibling: boj-server-cartridges PR #50
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Mistral Vibe <vibe@mistral.ai>
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
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
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.
Fix-up for v3 (which used fnmatch globs that don't match top-level directories like
tests/foo.ts).Replaces fnmatch-based glob matching with explicit string predicates:
lsp-server.tsetc.) and benchmarks (*_bench.ts,*.bench.ts)*and**both treated as 'any chars including /' (loose user-friendly interpretation).Verified against the affinescript exemption table + ubicity tests/+benchmarks/ + various edge cases.