feat: finish the v0.1 engine — dag, check, state machine, event stream#2
Merged
Conversation
Implements the spec's first-sprint items 4/5/6 (arghda-spec.adoc) plus a soundness lint, all verified with the real Agda toolchain (2.6.3) and dogfooded against the echo-types corpus. New capabilities - `graph` module: the Agda import graph is now first-class (nodes + typed `imports` edges, deterministic/sorted output). Lifted out of the `orphan-module` rule, which had computed the edges and thrown them away; the rule now reuses it. - `dag` command: emits the dependency-DAG JSON contract a visual layer consumes — nodes with lint-derived status (clean/warn/blocked), import edges, and a `blocked` list (self-blocked by rule + prerequisite-blocked by an unclean import). - Workspace state machine: `transition`/`state_of` move files between the four triage states, validated against the spec's transition table, each move appended to `.arghda/events.jsonl`. CLI: `claim`, `promote`, `reject`, `requeue`, `invalidate`, `events`. - `check` command: runs Agda on a file and combines the typecheck verdict with the lint report (`proven-eligible` / `rejected` / `agda-unavailable`). Degrades gracefully when `agda` is not on PATH. - `event` module: typed append-only JSONL event log + reader. - `agda` module: typecheck invocation with graceful NotFound handling. - `timestamp` module: dependency-free RFC 3339 UTC (keeps the build hermetic against the committed lockfile). - New lint rule `unjustified-postulate` (hard-block): a `postulate` opener with no adjacent `-- JUSTIFY:` comment. Verification - cargo fmt/clippy(-D warnings)/build/test all clean; 20 tests (11 unit + 9 integration: dag, transitions, smoke). - `check` exercised against real Agda: clean file -> proven-eligible; typechecking file missing --safe -> rejected by lint; type error -> rejected by agda (exit 42); JSON output verified. - `dag`/`scan` dogfooded on echo-types (193 modules): 903 import edges; `scan` independently rediscovers the orphan the 2026-06-16 trust audit found by hand (VarianceGate.agda) and the files outside the --safe --without-K kernel cone (Fidelity.agda, the cubical island, the postulated shadow). Deferred (next slice): remaining lint rules, content-hash invalidation of `proven`, the Groove service 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
The orphan rule previously computed reachability from a single entry module, so on a corpus with several CI roots it over-reported: every module reachable only from a non-`All.agda` root looked orphaned. The echo-types dogfood made this concrete — 38 orphan hits, most of them false. Changes - `graph::discover_roots` auto-discovers CI roots (`All.agda`/`Smoke.agda` at any depth); `graph::reachable_from_roots` unions reachability across them. - `LintContext.entry_module: &Path` -> `entry_modules: &[PathBuf]`; the orphan rule flags a module only if it is unreachable from *every* root and is not itself a root. - `scan` and `dag` share `resolve_roots_and_rules`: explicit `--entry` (now repeatable) wins, else auto-discover; if no roots are found the orphan rule is dropped (with a note) rather than flagging everything. - `dag` document now carries `entry_modules` (the roots it used). Verification - cargo fmt/clippy(-D warnings)/test clean; 21 tests (added a graph unit test proving union reachability: Used via All + Other via Smoke are reachable, Orphan via neither is not). - Re-dogfooded on echo-types (193 modules, 5 discovered roots): orphan reports drop 38 -> 17 genuine orphans (the experimental/echo-additive tree incl. VarianceGate.agda, plus standalone scratch files); the `dag` clean count rises 155 -> 176. postulate/pragma hits unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
hyperpolymath
added a commit
that referenced
this pull request
Jun 18, 2026
## 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 (so `believe_me_helper` doesn't trip it). - **`tab-mix`** (warn) — a tab in leading whitespace (Agda style is spaces). `missing-without-k` is intentionally **not** added — `missing-safe-pragma` already reports a missing `--without-K`. ### Verification (real toolchain, dogfooded) - `cargo fmt --check` / `clippy -D warnings` / `test` clean — **28 tests** (+7 unit: 2 `tab-mix`, 5 `escape-hatch`). - Re-dogfooded on echo-types (193 modules): **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**, which the rule correctly skips). A synthetic file with a real `{-# TERMINATING #-}` + `believe_me` produces exactly two warns. So the rule is both precise (no comment false-positives) and correct (fires on real escapes). ### Still deferred `unpinned-headline` (needs `Smoke.agda` parsing + a configurable regex), `unused-import` (shells out to `agda-unused`), content-hash invalidation of `proven`, the Groove service manifest, and the `.machine_readable/` RSR retrofit (its own PR next). Draft for review. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- _Generated by [Claude Code](https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs)_
14 tasks
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 — finish the v0.1 engine
Implements the spec's first-sprint items 4/5/6 (
docs/arghda-spec.adoc) plus a soundness lint. The engine now produces the JSON contract the planned AffineScript visual layer (arghda-studio, seedocs/arghda-vision.adoc) will consume. Verified with the real Agda toolchain (2.6.3) and dogfooded against the echo-types corpus, not eyeballed.New capabilities
graphmodule — the Agda import graph is now first-class (nodes + typedimportsedges, deterministic output). Lifted out of theorphan-modulerule, which had computed the edges and thrown them away; the rule now reuses it.dagcommand — emits the dependency-DAG JSON: nodes with lint-derived status (clean/warn/blocked), import edges, and ablockedlist (self-blocked by rule + prerequisite-blocked by an unclean import).transition/state_ofmove files between the four triage states, validated against the spec's transition table, each move appended to.arghda/events.jsonl. CLI:claim,promote,reject,requeue,invalidate,events.checkcommand — runs Agda on a file and combines the typecheck verdict with the lint report (proven-eligible/rejected/agda-unavailable); degrades gracefully whenagdais absent.event(append-only JSONL log + reader),agda(typecheck invocation, gracefulNotFound),timestamp(dependency-free RFC 3339 — keeps the build hermetic against the lockfile).unjustified-postulate(hard-block) — apostulateopener with no adjacent-- JUSTIFY:comment.Verification (the "do it right, not looks-fine" part)
cargo fmt --check/clippy -D warnings/build/testall clean — 20 tests (11 unit + 9 integration:dag,transitions,smoke).checkagainst real Agda 2.6.3: clean file →proven-eligible; a file that typechecks but lacks--safe→rejectedby lint (the silent-failure class the spec targets); a type error →rejected(agda exit 42). JSON output verified.dag/scandogfooded on echo-types (193 modules): 903 import edges;scanindependently rediscovers the orphan the 2026-06-16 trust audit found by hand (experimental/echo-additive/VarianceGate.agda) and the three files deliberately outside the--safe --without-Kkernel cone (Fidelity.agda, the cubical island, the postulated shadow).Deferred to the next slice
Remaining lint rules (
missing-without-k,unpinned-headline,unused-import,tab-mix), content-hash invalidation ofproven, multi-root reachability (echo-types is reachable from a union of CI roots, so single-entry orphan detection over-reports), the Groove service manifest, and the.machine_readable/RSR retrofit.Draft for review.
🤖 Generated with Claude Code
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
Generated by Claude Code