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
hyperpolymath
marked this pull request as ready for review
June 18, 2026 15:06
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
…(docs) (#49) ## What Records the outcome of investigating the **last** open roadmap item — the real Echidna orchestrator HTTP client. **Verdict: BLOCKED (not an effort gap) — the honest `Unavailable` stub stays.** Docs-only (STATE.a2ml); no code fabricated. ## Why (in-scope investigation) To build the client honestly you need a confirmed HTTP contract to dogfood against. There isn't one: - `src/dispatch.rs` itself states the orchestrator API is *"unconfirmed (it may not exist yet)"*. - `ECOSYSTEM.a2ml` describes echidna only at a high level (orchestrator, "Unified Zig API service #3, port 8090") — **no endpoints, no request/response schema**, i.e. no contract. - The `echidna` repo is **outside this session's GitHub access scope** (not among the scoped repos), so it can't be read to discover an API — and searching outside scope is disallowed. Writing a client would therefore mean **inventing an unverifiable contract**, which the honesty mandate and dispatch.rs's own honest-stub discipline forbid. **Unblock condition:** a published Echidna API (endpoints + schemas) *and* a reachable instance to dogfood against; then wire `Dispatch::run` behind a cargo feature — no backend/caller churn. ## Roadmap terminus All tractable items are done: - Engine spine **M0–M11** - Refinements **M3** (workspace verdicts), **M4** (.ipkg roots + totality/`partial` lint), **M6** (axiom audit + lake-env) - Heavy tail **M8 Coq / M9 Isabelle / M10 Mizar** **Nine backends** (agda, agda-cubical, idris2, lean4, coq, isabelle, mizar + z3, cvc5), every one dogfooded against its real tool. M7's client is the sole residual and is externally blocked. Gate unaffected (docs-only): `check-spdx.sh` OK, 173 tests still pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- _Generated by [Claude Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_ Co-authored-by: Claude <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
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