feat(lint): unused-import via agda-unused shell-out#7
Merged
Conversation
… validation pending)
Adds `src/unused.rs`, an `agda.rs`-style project-level shell-out to the
external `agda-unused` analyser, re-emitting its findings as `unused-import`
warn diagnostics (spec §Linter rules). Opt-in behind `scan --unused`;
degrades gracefully (with a note) when the binary is absent.
- Parses agda-unused's `--json` wrapper `{type,message}` and the findings
text in `message` (`/path/File.agda:line,col-col` + `<category> 'name'`).
- `merge_unused` attributes findings to per-file reports by canonical path.
- `lib.rs` re-exports `find_unused` / `UnusedOutcome`.
- `dist-newstyle/` gitignored (local agda-unused build output).
- Fixture `tests/fixtures/unused/{Main,Helper}.agda` (a genuine unused import).
Compiles; 6 parser unit tests pass against agda-unused's documented format.
The message-format parser is still to be validated against live agda-unused
output (binary building locally) before this PR leaves draft.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
…cale)
Validated against a freshly-built agda-unused binary and adjusted the design
to match real behaviour:
- Local per-file mode, not `--global`. `--global` treats the given root's
imports as project roots and reports nothing for them; local mode
(`agda-unused <file> --json -i <root>`) flags imports unused within a file
— the rule's namesake. Invoked once per scanned file; findings attach to
that file's report (no canonical-path merge needed).
- `LC_ALL=C.UTF-8` on the invocation. agda-unused reads source in the process
locale and aborts on the first multi-byte char otherwise; Agda is all UTF-8.
- Parser pinned to the real `{type,message}` JSON and the real findings text
(`/path/File.agda:line,col-col` + ` unused import ‘Name’`, Unicode quotes).
A run that yields no JSON (tool crash) is surfaced as an `error` kind rather
than aborting the scan.
- Drops `merge_unused` and the roots-based `find_unused`; `lib.rs` no longer
flat-re-exports (avoids clashing with `agda::check_file`).
- Fixtures carry the `--safe --without-K` pragma so the dogfood shows only the
unused-import finding.
Live dogfood: `scan --unused` on the fixture emits exactly
`unused-import: unused import ‘Helper’`; with agda-unused off PATH it degrades
with a note (0 warns). README + CHANGELOG updated; unused-import removed from
"Not yet". fmt/clippy/test green (lib 41 tests).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
hyperpolymath
changed the title
hyperpolymath
added a commit
that referenced
this pull request
Jun 20, 2026
## Summary Persists the operator-configurable headline pattern (and any future lint knobs) in `.arghda/config.toml` — the per-workspace surface the spec's open question calls for (`docs/arghda-spec.adoc` lines 200–202). Until now the pattern was only a CLI flag. ## Design - **`src/config.rs`** — a serde/`toml` schema deserialised from `.arghda/config.toml`, overlaid on `RuleConfig::default()`: ```toml [lint] headline_pattern = "^[a-z][A-Za-z0-9-]*$" ``` `deny_unknown_fields` so a typo (`headline_patten`) **errors** rather than being silently ignored; a missing file yields defaults. - **`scan` / `dag`** gain `--config <file>`; discovery defaults to `<PATH>/.arghda/config.toml`. - **Precedence (low → high):** built-in default < `config.toml` < CLI `--headline-pattern`. An explicit `--config` pointing at a missing file is an error; the default-location lookup is silently optional. - Reuses the existing `RuleConfig` / `rules_with_config` (from #6) — **no change to the rule itself**, just where its pattern comes from. ## Verification - `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo build`, `cargo test` all green (lib suite 41 → 47; 6 new config unit tests: parse / precedence / unknown-key-rejection / malformed-TOML / discovery). - **Live end-to-end:** empty config → default pattern flags all headlines; `[lint] headline_pattern = "^thm-.*$"` narrows to just `thm-key`; `--headline-pattern '^foo-.*$'` overrides the config file; `--config <missing>` errors cleanly. Adds the `toml` dependency. Second of three sequenced engine-polish PRs (3 → 2 → 1): `unused-import` (#7, merged), **`.arghda/config.toml`** (this), then the DAG `headlines` field. 🤖 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)_
hyperpolymath
added a commit
that referenced
this pull request
Jun 20, 2026
## Summary Completes the v0 DAG schema: each `dag` node now carries the per-node **`headlines`** array the spec defines (`docs/arghda-spec.adoc` lines 128–135) but the builder previously omitted — the sorted, deduped list of top-level headline theorem names the module declares. ## Design - **Reuses the `unpinned-headline` extractor** — no duplicate parsing. `headline_decls` becomes `pub`, and `dag::build` runs it per node with the configured headline `Regex`. - **`build_dag` gains a `headline_pattern: &str` parameter.** `dag` threads the *resolved* pattern through (built-in default < `.arghda/config.toml` < CLI `--headline-pattern`, via the #8 config plumbing), so the DAG honours the same operator configuration as the lint. - Column-0-only extraction means indented `private` helpers are not surfaced (same export-only filter as the rule). ## Verification - `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo build`, `cargo test` all green (7 groups). - New `tests/fixtures/headlines/` + `dag_populates_node_headlines`: asserts `Thm → ["thm-one","thm-two"]`, that the indented `private helper` is excluded, and the import-only `All` entry surfaces `[]`. - **Live:** `arghda dag tests/fixtures/headlines` emits `"headlines": ["thm-one","thm-two"]` on the `Thm` node and `[]` on `All`. Last of three sequenced engine-polish PRs (3 → 2 → 1): `unused-import` (#7), `.arghda/config.toml` (#8), **DAG `headlines`** (this). With these, the v0 Agda lint set and DAG schema in `arghda-spec.adoc` are complete. 🤖 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)_
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.
Summary
Implements the last spec'd v0 Agda lint (
docs/arghda-spec.adoc§Linter rules, line 106): shell out toagda-unusedand re-emit findings asunused-importwarn diagnostics. Validated end-to-end against a liveagda-unusedbinary (built locally for this work).Design (matches real
agda-unusedbehaviour)src/unused.rs— anagda.rs-style shell-out. Runsagda-unused <file> --json -i <root>per file, in local mode.--global: live testing showed--globaltreats the given root's imports as project roots and reports nothing for them; local mode flags imports unused within a file — the rule's namesake.LC_ALL=C.UTF-8:agda-unusedreads source in the process locale and aborts on the first multi-byte character otherwise — and real Agda is all UTF-8. (Same fix echo-types' docs use foragdaitself.){ "type": "none"|"unused"|"error", "message": … }wrapper and the findings text (/path/File.agda:line,col-col+unused import ‘Name’). A run that yields no JSON (tool crash) is surfaced as anerrorkind, so one bad file never aborts the scan.scan --unused(it needs the external tool and re-checks each file). Graceful degradation with anote:when the binary is absent — mirroring howchecktolerates a missingagda.lib.rskeepsunusedmodule-qualified (no flat re-export, to avoid clashing withagda::check_file).dist-newstyle/gitignored; fixturetests/fixtures/unused/{Main,Helper}.agda(a genuine unused import, pragma-clean).Verification
cargo fmt --check,cargo clippy --all-targets -- -D warnings,cargo build,cargo testall green (lib suite 35 → 41).scan --unusedon the fixture emits exactlyunused-import: unused import ‘Helper’; withagda-unusedoffPATHit degrades with a note and 0 warns.Note: CI runners don't have
agda-unused, so the shell-out path isn't exercised in CI (the parser is unit-tested; the binary glue degrades gracefully) — exactly the patternagda.rsuses foragda.First of three sequenced engine-polish PRs (3 → 2 → 1):
unused-import(this), then.arghda/config.tomlpersistence, then the DAGheadlinesfield.🤖 Generated with Claude Code
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs