feat(lint): unused-import via agda-unused shell-out (#7)

## Summary

Implements the last spec'd v0 Agda lint (`docs/arghda-spec.adoc` §Linter
rules, line 106): shell out to `agda-unused` and re-emit findings as
`unused-import` **warn** diagnostics. **Validated end-to-end against a
live `agda-unused` binary** (built locally for this work).

## Design (matches real `agda-unused` behaviour)

- **`src/unused.rs`** — an `agda.rs`-style shell-out. Runs `agda-unused
<file> --json -i <root>` **per file, in local mode**.
- *Why local, not `--global`:* live testing showed `--global` treats 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-unused` reads 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 for `agda` itself.)
- Parses the real `{ "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
an `error` kind, so one bad file never aborts the scan.
- **Opt-in** behind `scan --unused` (it needs the external tool and
re-checks each file). **Graceful degradation** with a `note:` when the
binary is absent — mirroring how `check` tolerates a missing `agda`.
- `lib.rs` keeps `unused` module-qualified (no flat re-export, to avoid
clashing with `agda::check_file`).
- `dist-newstyle/` gitignored; fixture
`tests/fixtures/unused/{Main,Helper}.agda` (a genuine unused import,
pragma-clean).

## Verification

- `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`,
`cargo build`, `cargo test` all green (lib suite 35 → 41).
- **Live dogfood:** `scan --unused` on the fixture emits exactly
`unused-import: unused import ‘Helper’`; with `agda-unused` off `PATH`
it degrades with a note and 0 warns.
- Parser unit tests pinned to the **real** captured JSON + findings
format.

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 pattern `agda.rs` uses for `agda`.

First of three sequenced engine-polish PRs (3 → 2 → 1):
**`unused-import`** (this), then `.arghda/config.toml` persistence, then
the DAG `headlines` field.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs

Author: hyperpolymath

.gitignore

@@ -1,6 +1,9 @@
 # Rust build artefacts
 target/
 
+# Haskell / cabal build artefacts (from building agda-unused locally)
+dist-newstyle/
+
 # Editor / tooling backups
 *.bak
 *~

CHANGELOG.md

@@ -31,6 +31,12 @@ All notable changes to arghda-core are documented here. The format follows
   `^[a-z][A-Za-z0-9-]*$`, per the spec). Detects top-level (column-0)
   signatures only, which gives the export-only filter for free; tolerant of
   multi-line `using` lists; self-skips when no `Smoke.agda` is in scope.
+- `unused-import` (warn): re-emits the findings of the external `agda-unused`
+  tool (spec §Linter rules). Opt-in behind `scan --unused`; runs `agda-unused`
+  per file in local mode with `LC_ALL=C.UTF-8`, parses its `--json` output,
+  and re-emits each finding as an `unused-import` warning attributed to the
+  file. Degrades gracefully (with a note) when `agda-unused` is not on `PATH`,
+  mirroring how `check` tolerates a missing `agda`.
 - RSR scaffolding: `.machine_readable/6a2/` artefacts, `0-AI-MANIFEST.a2ml`,
   `Justfile`, `.well-known/`, and community-health files.
 - Content-hash invalidation of `proven`: promotion records a SHA-256 of the

README.md

@@ -30,6 +30,11 @@ record.
     its default `^[a-z][A-Za-z0-9-]*$` is deliberately broad, so operators
     narrow it to their own headline-naming convention. Self-skips when no
     `Smoke.agda` is in scope (e.g. a single-file `check`)
+  - `unused-import` (warn) — re-emits the findings of the external
+    [`agda-unused`](https://github.com/msuperdock/agda-unused) tool. Opt-in
+    behind `scan --unused` (it runs `agda-unused` per file in local mode and
+    re-checks each file); skipped with a note if the binary is not on `PATH`.
+    Invoked with `LC_ALL=C.UTF-8` so it can read UTF-8 Agda sources
 - Workspace state machine — transitions are file moves, each logged to
   `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`,
   `invalidate`)
@@ -51,12 +56,12 @@ plus standalone scratch files. `scan` also flags the files deliberately
 outside the `--safe --without-K` kernel cone (`Fidelity.agda`, the cubical
 island, the postulated shadow).
 
-Not yet: `unused-import` (shells out to `agda-unused`); the DAG `headlines`
-field (the extractor now exists for `unpinned-headline`, but the per-node
-`headlines` array in the DAG schema is still unpopulated); persisting the
-headline pattern in `.arghda/config.toml` (currently a CLI flag); the Groove
-service manifest. (`missing-without-k` is subsumed by `missing-safe-pragma`,
-which already reports a missing `--without-K`.)
+Not yet: the DAG `headlines` field (the extractor now exists for
+`unpinned-headline`, but the per-node `headlines` array in the DAG schema is
+still unpopulated); persisting the headline pattern in `.arghda/config.toml`
+(currently a CLI flag); the Groove service manifest. (`missing-without-k` is
+subsumed by `missing-safe-pragma`, which already reports a missing
+`--without-K`.)
 
 ## Build
 

src/lib.rs

@@ -12,6 +12,7 @@ pub mod hash;
 pub mod lint;
 pub mod proven;
 pub mod timestamp;
+pub mod unused;
 pub mod watcher;
 pub mod workspace;
 

src/main.rs

@@ -1,8 +1,8 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, check_file, default_rules, event, graph, rules_with_config, run_lints, watcher,
-    LintRule, RuleConfig, State, Workspace,
+    build_dag, check_file, default_rules, event, graph, rules_with_config, run_lints, unused,
+    watcher, LintRule, RuleConfig, State, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -39,6 +39,11 @@ enum Cmd {
         /// (`unpinned-headline` rule). Defaults to the spec pattern.
         #[arg(long)]
         headline_pattern: Option<String>,
+        /// Also run the external `agda-unused` analyser and re-emit its
+        /// findings as `unused-import` warnings (requires `agda-unused` on
+        /// PATH; skipped with a note if absent).
+        #[arg(long)]
+        unused: bool,
         /// Emit the report as JSON instead of human-readable text.
         #[arg(long)]
         json: bool,
@@ -101,8 +106,9 @@ fn main() -> Result<()> {
             path,
             entry,
             headline_pattern,
+            unused,
             json,
-        } => scan(&path, &entry, headline_pattern.as_deref(), json)?,
+        } => scan(&path, &entry, headline_pattern.as_deref(), unused, json)?,
         Cmd::Check {
             file,
             include_root,
@@ -142,6 +148,7 @@ fn scan(
     include_root: &Path,
     entry: &[PathBuf],
     headline_pattern: Option<&str>,
+    unused: bool,
     json: bool,
 ) -> Result<()> {
     let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern)?;
@@ -151,9 +158,6 @@ fn scan(
     };
 
     let mut reports = Vec::new();
-    let mut hard_blocks = 0usize;
-    let mut warns = 0usize;
-
     for entry in WalkDir::new(include_root)
         .into_iter()
         .filter_map(|e| e.ok())
@@ -164,17 +168,45 @@ fn scan(
         }
         let report =
             run_lints(path, &ctx, &rules).with_context(|| format!("linting {}", path.display()))?;
-        hard_blocks += report.hard_blocks().count();
-        warns += report.warns().count();
         reports.push(report);
     }
+    let files_scanned = reports.len();
+
+    // Optional unused-code pass via the external `agda-unused` (per file,
+    // local mode). Opt-in because it needs the external tool and re-checks
+    // each file. Findings attach to that file's report.
+    if unused {
+        let mut available = true;
+        let mut saw_error = false;
+        for report in &mut reports {
+            let check = unused::check_file(&report.file, include_root)?;
+            if !check.available {
+                available = false;
+                break;
+            }
+            saw_error |= check.kind.as_deref() == Some("error");
+            for d in check.diagnostics {
+                report.push(d);
+            }
+        }
+        if !available {
+            eprintln!("note: `agda-unused` not found on PATH; skipping unused-import findings");
+        } else if saw_error {
+            eprintln!(
+                "note: agda-unused could not analyse some files; unused-import findings may be incomplete"
+            );
+        }
+    }
+
+    let hard_blocks: usize = reports.iter().map(|r| r.hard_blocks().count()).sum();
+    let warns: usize = reports.iter().map(|r| r.warns().count()).sum();
 
     if json {
         let payload = serde_json::json!({
             "version": "0.1",
             "include_root": include_root,
             "entry_modules": roots,
-            "files_scanned": reports.len(),
+            "files_scanned": files_scanned,
             "hard_blocks": hard_blocks,
             "warns": warns,
             "reports": reports,