fix(unused): align to live agda-unused (per-file local mode, UTF-8 locale)

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

Author: claude

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

@@ -22,5 +22,4 @@ pub use diagnostic::{Diagnostic, LintReport, Severity};
 pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
-pub use unused::{find_unused, UnusedOutcome};
 pub use workspace::{StaleEntry, State, Workspace};

src/main.rs

@@ -1,11 +1,10 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, check_file, default_rules, event, find_unused, graph, rules_with_config, run_lints,
-    watcher, Diagnostic, LintReport, 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::collections::HashMap;
 use std::path::{Path, PathBuf};
 use std::time::Duration;
 use walkdir::WalkDir;
@@ -173,18 +172,29 @@ fn scan(
     }
     let files_scanned = reports.len();
 
-    // Optional project-level unused-code pass via the external `agda-unused`.
+    // 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 outcome = find_unused(include_root, &roots)?;
-        if !outcome.available {
-            eprintln!("note: `agda-unused` not found on PATH; skipping unused-import findings");
-        } else {
-            if outcome.kind.as_deref() == Some("error") {
-                eprintln!(
-                    "note: agda-unused reported an analysis error; unused-import findings may be incomplete"
-                );
+        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);
             }
-            merge_unused(&mut reports, outcome.diagnostics);
+        }
+        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"
+            );
         }
     }
 
@@ -222,32 +232,6 @@ fn scan(
     Ok(())
 }
 
-/// Attribute `agda-unused` findings to the scanned per-file reports by
-/// canonical path. A finding for a file that was not scanned (rare) gets its
-/// own report so nothing is silently dropped.
-fn merge_unused(reports: &mut Vec<LintReport>, diags: Vec<Diagnostic>) {
-    let mut by_canon: HashMap<PathBuf, usize> = HashMap::new();
-    for (idx, r) in reports.iter().enumerate() {
-        if let Ok(c) = std::fs::canonicalize(&r.file) {
-            by_canon.insert(c, idx);
-        }
-    }
-    for d in diags {
-        let canon = std::fs::canonicalize(&d.file).ok();
-        if let Some(idx) = canon.as_ref().and_then(|c| by_canon.get(c).copied()) {
-            reports[idx].push(d);
-        } else {
-            let idx = reports.len();
-            if let Some(c) = canon {
-                by_canon.insert(c, idx);
-            }
-            let mut r = LintReport::new(d.file.clone());
-            r.push(d);
-            reports.push(r);
-        }
-    }
-}
-
 fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> {
     if !file.is_file() {
         anyhow::bail!("file not found: {}", file.display());