feat(lint): escape-hatch + tab-mix rules#3
Merged
Conversation
Rounds out the v0.1 rule pack with the two cheap, high-value rules from
the spec/plan that need no external tooling.
- `escape-hatch` (warn): surfaces soundness escape hatches — the
termination-checker overrides (`TERMINATING`, `NON_TERMINATING`,
`NO_TERMINATION_CHECK`) and the trust primitives
(`believe_me`/`primTrustMe`). Warn, not hard-block: these are
sometimes legitimately budgeted (echo-types' quarantine discipline),
so the rule makes them visible without blocking promotion. Precise:
it ignores the words in `--` comments and only matches whole tokens
(so `believe_me_helper` does not trip it).
- `tab-mix` (warn): a tab in leading whitespace (Agda style is spaces).
Verification
- cargo fmt/clippy(-D warnings)/test clean; 28 tests (+7 unit).
- Re-dogfooded on echo-types: 0 escape-hatch/tab-mix hits, confirmed a
TRUE negative by ground-truth grep — the only two `.agda` files
containing the word "TERMINATING" carry it in `-- TERMINATING
CONDITION` comments, not pragmas, which the rule correctly skips. A
synthetic file with a real `{-# TERMINATING #-}` + `believe_me`
produces exactly two warns.
`missing-without-k` is intentionally not added: `missing-safe-pragma`
already reports a missing `--without-K`. Still deferred:
`unpinned-headline` (needs Smoke.agda parsing + configurable regex),
`unused-import` (shells out to agda-unused), content-hash invalidation,
the Groove manifest, and the `.machine_readable/` RSR retrofit.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
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.
Phase 1 (cont.) — round out the v0.1 lint pack
Follows the merged engine (#2). Adds the two cheap, high-value rules from the spec/plan that need no external tooling, on top of multi-root reachability.
New rules
escape-hatch(warn) — surfaces soundness escape hatches: termination-checker overrides (TERMINATING,NON_TERMINATING,NO_TERMINATION_CHECK) and trust primitives (believe_me/primTrustMe). Warn, not hard-block — these are sometimes legitimately budgeted (echo-types' quarantine discipline), so the rule makes them visible without blocking promotion. Precise: ignores the words inside--comments and only matches whole tokens (sobelieve_me_helperdoesn't trip it).tab-mix(warn) — a tab in leading whitespace (Agda style is spaces).missing-without-kis intentionally not added —missing-safe-pragmaalready reports a missing--without-K.Verification (real toolchain, dogfooded)
cargo fmt --check/clippy -D warnings/testclean — 28 tests (+7 unit: 2tab-mix, 5escape-hatch)..agdafiles containing the word "TERMINATING" carry it in-- TERMINATING CONDITIONcomments, which the rule correctly skips). A synthetic file with a real{-# TERMINATING #-}+believe_meproduces exactly two warns. So the rule is both precise (no comment false-positives) and correct (fires on real escapes).Still deferred
unpinned-headline(needsSmoke.agdaparsing + a configurable regex),unused-import(shells out toagda-unused), content-hash invalidation ofproven, the Groove service manifest, and the.machine_readable/RSR retrofit (its own PR next).Draft for review.
🤖 Generated with Claude Code
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
Generated by Claude Code