From 54106d9f75d3e1a5a4a486fad7ef09bf9e87960f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 10:05:00 +0000 Subject: [PATCH 1/2] feat(lint): unused-import via agda-unused shell-out (WIP: live parser validation pending) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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` + ` '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 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- .gitignore | 3 + src/lib.rs | 2 + src/main.rs | 66 +++++++-- src/unused.rs | 230 ++++++++++++++++++++++++++++++ tests/fixtures/unused/Helper.agda | 6 + tests/fixtures/unused/Main.agda | 5 + 6 files changed, 303 insertions(+), 9 deletions(-) create mode 100644 src/unused.rs create mode 100644 tests/fixtures/unused/Helper.agda create mode 100644 tests/fixtures/unused/Main.agda diff --git a/.gitignore b/.gitignore index fd5fec7..2dcc89f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ # Rust build artefacts target/ +# Haskell / cabal build artefacts (from building agda-unused locally) +dist-newstyle/ + # Editor / tooling backups *.bak *~ diff --git a/src/lib.rs b/src/lib.rs index f1b0fc2..b96e736 100644 --- a/src/lib.rs +++ b/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; @@ -21,4 +22,5 @@ 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}; diff --git a/src/main.rs b/src/main.rs index 91b63a7..6b80f38 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,10 +1,11 @@ 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, find_unused, graph, rules_with_config, run_lints, + watcher, Diagnostic, LintReport, LintRule, RuleConfig, State, Workspace, }; use clap::{Parser, Subcommand}; +use std::collections::HashMap; use std::path::{Path, PathBuf}; use std::time::Duration; use walkdir::WalkDir; @@ -39,6 +40,11 @@ enum Cmd { /// (`unpinned-headline` rule). Defaults to the spec pattern. #[arg(long)] headline_pattern: Option, + /// 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 +107,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 +149,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 +159,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 +169,34 @@ 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 project-level unused-code pass via the external `agda-unused`. + 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" + ); + } + merge_unused(&mut reports, outcome.diagnostics); + } + } + + 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, @@ -200,6 +222,32 @@ 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, diags: Vec) { + let mut by_canon: HashMap = 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()); diff --git a/src/unused.rs b/src/unused.rs new file mode 100644 index 0000000..a638aa9 --- /dev/null +++ b/src/unused.rs @@ -0,0 +1,230 @@ +//! Shelling out to `agda-unused` to find unused code in a project. +//! +//! Like [`crate::agda`], ArghDA does not analyse for unused code itself — it +//! asks the external `agda-unused` tool and re-emits its findings as ArghDA +//! diagnostics (the `unused-import` rule, `docs/arghda-spec.adoc`). If +//! `agda-unused` is not on `PATH` it degrades gracefully (`available: false`) +//! so the rest of the engine still works without it (the rule is opt-in +//! behind `scan --unused`). +//! +//! `agda-unused` is a *project-level* analyser — it resolves the whole import +//! graph from a root module — so this is a single pass over a source tree, +//! not a per-file [`crate::lint::LintRule`]. Its `--json` output is a wrapper +//! object `{ "type": "none" | "unused" | "error", "message": "…" }`; the +//! findings live in `message` in the human-readable form +//! +//! ```text +//! /abs/path/File.agda:line,col-col +//! '' +//! ``` +//! +//! which we parse into per-file [`Diagnostic`]s under the `unused-import` +//! rule (severity `warn`, per the spec's rule table). + +use crate::diagnostic::{Diagnostic, Severity}; +use anyhow::{Context, Result}; +use serde::Deserialize; +use std::collections::BTreeSet; +use std::path::{Path, PathBuf}; +use std::process::Command; + +/// The rule name re-emitted findings carry. +pub const RULE_NAME: &str = "unused-import"; + +/// Outcome of an `agda-unused` pass over a source tree. +#[derive(Clone, Debug, Default)] +pub struct UnusedOutcome { + /// Whether the `agda-unused` binary was found and executed. + pub available: bool, + /// Findings re-emitted as diagnostics (rule = `unused-import`, warn). + pub diagnostics: Vec, + /// The last `type` field seen ("none" / "unused" / "error"), for surfacing + /// the case where `agda-unused` itself errored (e.g. a type error). + pub kind: Option, +} + +/// The `--json` wrapper `agda-unused` emits. +#[derive(Debug, Deserialize)] +struct UnusedJson { + #[serde(rename = "type")] + kind: String, + #[serde(default)] + message: String, +} + +/// Run `agda-unused --global --json -i ` for each root and +/// union the findings (deduplicated by file + line + message). A missing +/// binary yields `available: false` with no diagnostics. +pub fn find_unused(include_root: &Path, roots: &[PathBuf]) -> Result { + let mut outcome = UnusedOutcome::default(); + let mut seen: BTreeSet<(PathBuf, Option, String)> = BTreeSet::new(); + + for root in roots { + let Some(parsed) = run_one(root, include_root)? else { + // Binary not found: report unavailable and stop. + return Ok(UnusedOutcome::default()); + }; + outcome.available = true; + outcome.kind = Some(parsed.kind.clone()); + if parsed.kind != "unused" { + // "none" → nothing unused; "error" → agda-unused could not analyse + // (surfaced via `kind`); neither yields findings. + continue; + } + for (file, line, desc) in parse_findings(&parsed.message) { + let message = if desc.is_empty() { + "unused code".to_string() + } else { + desc + }; + if seen.insert((file.clone(), line, message.clone())) { + outcome.diagnostics.push(Diagnostic { + rule: RULE_NAME.to_string(), + severity: Severity::Warn, + file, + message, + line, + }); + } + } + } + Ok(outcome) +} + +/// Invoke `agda-unused` once on `root`. `Ok(None)` iff the binary is absent. +fn run_one(root: &Path, include_root: &Path) -> Result> { + let output = Command::new("agda-unused") + .arg(root) + .arg("--global") + .arg("--json") + .arg("-i") + .arg(include_root) + .output(); + + match output { + Ok(out) => { + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); + combined.push_str(&String::from_utf8_lossy(&out.stderr)); + let json = extract_json(&combined).with_context(|| { + format!( + "no JSON object in agda-unused output for {}", + root.display() + ) + })?; + let parsed: UnusedJson = serde_json::from_str(json) + .with_context(|| format!("parsing agda-unused JSON for {}", root.display()))?; + Ok(Some(parsed)) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => Ok(None), + Err(e) => Err(e.into()), + } +} + +/// Extract the outermost `{ … }` JSON object from `s` (tolerant of any +/// non-JSON preamble the tool might print before the object). +fn extract_json(s: &str) -> Option<&str> { + let start = s.find('{')?; + let end = s.rfind('}')?; + if end >= start { + Some(&s[start..=end]) + } else { + None + } +} + +/// Parse the findings out of an `agda-unused` `message`. Each finding is a +/// location line (`…/File.agda:line,col-col`) followed by an indented +/// description line (` ''`). +fn parse_findings(message: &str) -> Vec<(PathBuf, Option, String)> { + let lines: Vec<&str> = message.lines().collect(); + let mut out = Vec::new(); + let mut i = 0; + while i < lines.len() { + if let Some((file, line)) = parse_location(lines[i]) { + // The description is the next non-empty line that is not itself a + // location (indented ` ''`). + let mut desc = String::new(); + if i + 1 < lines.len() { + let next = lines[i + 1].trim(); + if !next.is_empty() && parse_location(lines[i + 1]).is_none() { + desc = next.to_string(); + i += 1; + } + } + out.push((file, line, desc)); + } + i += 1; + } + out +} + +/// Parse a location line `…/File.agda:line,col-col` into the file path and the +/// 1-based line number. Tolerant: the trailing column/range part is optional. +fn parse_location(line: &str) -> Option<(PathBuf, Option)> { + let trimmed = line.trim(); + // Anchor on the `.agda:` boundary so paths containing `:` (unlikely) or + // colons elsewhere don't confuse the split. + let marker = ".agda:"; + let idx = trimmed.rfind(marker)?; + let file = PathBuf::from(&trimmed[..idx + ".agda".len()]); + let rest = &trimmed[idx + marker.len()..]; + // `rest` looks like `12,3-8` or `12,3-13,5`; take the leading integer. + let lineno = rest + .split(|c: char| !c.is_ascii_digit()) + .find(|s| !s.is_empty()) + .and_then(|s| s.parse::().ok()); + Some((file, lineno)) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn absent_binary_degrades_gracefully() { + // `run_one` against a guaranteed-absent binary name is exercised + // indirectly: find_unused with a bogus PATH can't be forced here, so + // we assert the parser/JSON layers instead. The not-found path is the + // `Ok(None)` arm of `run_one` (see also crate::agda). + let o = UnusedOutcome::default(); + assert!(!o.available); + assert!(o.diagnostics.is_empty()); + } + + #[test] + fn extract_json_finds_object_amid_noise() { + assert_eq!( + extract_json("preamble {\"type\":\"none\"} trailing"), + Some("{\"type\":\"none\"}") + ); + assert_eq!(extract_json("no object here"), None); + } + + #[test] + fn parse_location_reads_path_and_line() { + let (f, l) = parse_location("/home/u/proj/Foo/Bar.agda:12,3-8").unwrap(); + assert_eq!(f, PathBuf::from("/home/u/proj/Foo/Bar.agda")); + assert_eq!(l, Some(12)); + } + + #[test] + fn parse_location_tolerates_line_range() { + let (_f, l) = parse_location("X.agda:7,1-9,4").unwrap(); + assert_eq!(l, Some(7)); + } + + #[test] + fn parse_location_rejects_non_location() { + assert!(parse_location(" unused import 'Foo'").is_none()); + } + + #[test] + fn parse_findings_pairs_location_with_description() { + let msg = "/p/Main.agda:3,1-19\n unused import 'Unused'\n"; + let found = parse_findings(msg); + assert_eq!(found.len(), 1); + assert_eq!(found[0].0, PathBuf::from("/p/Main.agda")); + assert_eq!(found[0].1, Some(3)); + assert_eq!(found[0].2, "unused import 'Unused'"); + } +} diff --git a/tests/fixtures/unused/Helper.agda b/tests/fixtures/unused/Helper.agda new file mode 100644 index 0000000..a15ed48 --- /dev/null +++ b/tests/fixtures/unused/Helper.agda @@ -0,0 +1,6 @@ +module Helper where + +-- A trivial, dependency-free definition. Nothing references it, so a +-- whole-project (`--global`) agda-unused pass should also flag it. +helper : Set₁ +helper = Set diff --git a/tests/fixtures/unused/Main.agda b/tests/fixtures/unused/Main.agda new file mode 100644 index 0000000..1cf2724 --- /dev/null +++ b/tests/fixtures/unused/Main.agda @@ -0,0 +1,5 @@ +module Main where + +-- Imports Helper but uses nothing from it: a genuine unused import, which is +-- exactly what `agda-unused` should report (re-emitted as `unused-import`). +open import Helper From 7feae637ad73ca6f44d465518a6ef1a70ab5bebc Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 10:18:12 +0000 Subject: [PATCH 2/2] fix(unused): align to live agda-unused (per-file local mode, UTF-8 locale) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --json -i `) 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 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- CHANGELOG.md | 6 + README.md | 17 ++- src/lib.rs | 1 - src/main.rs | 62 ++++----- src/unused.rs | 201 ++++++++++++++++-------------- tests/fixtures/unused/Helper.agda | 4 +- tests/fixtures/unused/Main.agda | 3 +- 7 files changed, 150 insertions(+), 144 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index df7dab1..9421d1e 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/README.md b/README.md index 052275a..2524928 100644 --- a/README.md +++ b/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 diff --git a/src/lib.rs b/src/lib.rs index b96e736..1fea9d2 100644 --- a/src/lib.rs +++ b/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}; diff --git a/src/main.rs b/src/main.rs index 6b80f38..234f9c9 100644 --- a/src/main.rs +++ b/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, diags: Vec) { - let mut by_canon: HashMap = 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()); diff --git a/src/unused.rs b/src/unused.rs index a638aa9..a47f87b 100644 --- a/src/unused.rs +++ b/src/unused.rs @@ -1,46 +1,49 @@ -//! Shelling out to `agda-unused` to find unused code in a project. +//! Shelling out to `agda-unused` to find unused code (the `unused-import` rule). //! //! Like [`crate::agda`], ArghDA does not analyse for unused code itself — it //! asks the external `agda-unused` tool and re-emits its findings as ArghDA -//! diagnostics (the `unused-import` rule, `docs/arghda-spec.adoc`). If -//! `agda-unused` is not on `PATH` it degrades gracefully (`available: false`) -//! so the rest of the engine still works without it (the rule is opt-in -//! behind `scan --unused`). +//! diagnostics (`docs/arghda-spec.adoc` §Linter rules). If `agda-unused` is +//! not on `PATH` it degrades gracefully (`available: false`) so the rest of +//! the engine still works; the rule is opt-in behind `scan --unused`. //! -//! `agda-unused` is a *project-level* analyser — it resolves the whole import -//! graph from a root module — so this is a single pass over a source tree, -//! not a per-file [`crate::lint::LintRule`]. Its `--json` output is a wrapper -//! object `{ "type": "none" | "unused" | "error", "message": "…" }`; the -//! findings live in `message` in the human-readable form +//! We invoke it **per file in local mode** (`agda-unused --json -i +//! `). Local mode flags imports/code unused *within* that file (the +//! rule's namesake); `--global` instead treats the given root's imports as +//! project roots and would not flag them. `agda-unused` reads source in the +//! process locale, so we force `LC_ALL=C.UTF-8` — Agda sources are UTF-8 and +//! without it the tool aborts on the first multi-byte character. +//! +//! `--json` output is a wrapper object +//! `{ "type": "none" | "unused" | "error", "message": "…" }`; when `type` is +//! `"unused"` the findings live in `message` as location/description pairs: //! //! ```text //! /abs/path/File.agda:line,col-col -//! '' +//! unused import ‘Name’ //! ``` //! -//! which we parse into per-file [`Diagnostic`]s under the `unused-import` -//! rule (severity `warn`, per the spec's rule table). +//! re-emitted as `unused-import` `warn` diagnostics. use crate::diagnostic::{Diagnostic, Severity}; use anyhow::{Context, Result}; use serde::Deserialize; -use std::collections::BTreeSet; use std::path::{Path, PathBuf}; use std::process::Command; /// The rule name re-emitted findings carry. pub const RULE_NAME: &str = "unused-import"; -/// Outcome of an `agda-unused` pass over a source tree. +/// Result of an `agda-unused` pass over a single file. #[derive(Clone, Debug, Default)] -pub struct UnusedOutcome { +pub struct UnusedCheck { /// Whether the `agda-unused` binary was found and executed. pub available: bool, - /// Findings re-emitted as diagnostics (rule = `unused-import`, warn). - pub diagnostics: Vec, - /// The last `type` field seen ("none" / "unused" / "error"), for surfacing - /// the case where `agda-unused` itself errored (e.g. a type error). + /// The `type` field of the JSON wrapper ("none" / "unused" / "error"), + /// so the caller can surface the case where `agda-unused` could not + /// analyse a file. pub kind: Option, + /// Findings located in the checked file, as `unused-import` warnings. + pub diagnostics: Vec, } /// The `--json` wrapper `agda-unused` emits. @@ -52,68 +55,73 @@ struct UnusedJson { message: String, } -/// Run `agda-unused --global --json -i ` for each root and -/// union the findings (deduplicated by file + line + message). A missing -/// binary yields `available: false` with no diagnostics. -pub fn find_unused(include_root: &Path, roots: &[PathBuf]) -> Result { - let mut outcome = UnusedOutcome::default(); - let mut seen: BTreeSet<(PathBuf, Option, String)> = BTreeSet::new(); - - for root in roots { - let Some(parsed) = run_one(root, include_root)? else { - // Binary not found: report unavailable and stop. - return Ok(UnusedOutcome::default()); - }; - outcome.available = true; - outcome.kind = Some(parsed.kind.clone()); - if parsed.kind != "unused" { - // "none" → nothing unused; "error" → agda-unused could not analyse - // (surfaced via `kind`); neither yields findings. - continue; - } - for (file, line, desc) in parse_findings(&parsed.message) { - let message = if desc.is_empty() { - "unused code".to_string() - } else { - desc - }; - if seen.insert((file.clone(), line, message.clone())) { - outcome.diagnostics.push(Diagnostic { +/// Run `agda-unused --json -i ` (local mode, UTF-8) and +/// return the unused-code findings located in `file`. `available: false` iff +/// the binary is absent. +pub fn check_file(file: &Path, include_root: &Path) -> Result { + let Some(parsed) = run_one(file, include_root)? else { + return Ok(UnusedCheck::default()); + }; + let mut check = UnusedCheck { + available: true, + kind: Some(parsed.kind.clone()), + diagnostics: Vec::new(), + }; + if parsed.kind == "unused" { + // Local mode can also visit dependencies; keep only findings that + // belong to `file` so each is attributed exactly once (when we invoke + // agda-unused on its own file). agda-unused reports absolute paths, so + // compare canonicalised. + let target = std::fs::canonicalize(file).ok(); + for (path, line, desc) in parse_findings(&parsed.message) { + if target.is_some() && std::fs::canonicalize(&path).ok() == target { + check.diagnostics.push(Diagnostic { rule: RULE_NAME.to_string(), severity: Severity::Warn, - file, - message, + file: file.to_path_buf(), + message: if desc.is_empty() { + "unused code".to_string() + } else { + desc + }, line, }); } } } - Ok(outcome) + Ok(check) } -/// Invoke `agda-unused` once on `root`. `Ok(None)` iff the binary is absent. -fn run_one(root: &Path, include_root: &Path) -> Result> { +/// Invoke `agda-unused` once on `file`. `Ok(None)` iff the binary is absent. +/// A run that produces no JSON object (e.g. the tool itself errored) is +/// reported as an `"error"` wrapper rather than failing the whole scan. +fn run_one(file: &Path, include_root: &Path) -> Result> { let output = Command::new("agda-unused") - .arg(root) - .arg("--global") + .arg(file) .arg("--json") .arg("-i") .arg(include_root) + .env("LC_ALL", "C.UTF-8") .output(); match output { Ok(out) => { let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); combined.push_str(&String::from_utf8_lossy(&out.stderr)); - let json = extract_json(&combined).with_context(|| { - format!( - "no JSON object in agda-unused output for {}", - root.display() - ) - })?; - let parsed: UnusedJson = serde_json::from_str(json) - .with_context(|| format!("parsing agda-unused JSON for {}", root.display()))?; - Ok(Some(parsed)) + match extract_json(&combined) { + Some(json) => { + let parsed: UnusedJson = serde_json::from_str(json).with_context(|| { + format!("parsing agda-unused JSON for {}", file.display()) + })?; + Ok(Some(parsed)) + } + // No JSON: agda-unused crashed/errored on this file. Surface as + // an error wrapper so one bad file does not abort the scan. + None => Ok(Some(UnusedJson { + kind: "error".to_string(), + message: combined.trim().to_string(), + })), + } } Err(e) if e.kind() == std::io::ErrorKind::NotFound => Ok(None), Err(e) => Err(e.into()), @@ -121,20 +129,16 @@ fn run_one(root: &Path, include_root: &Path) -> Result> { } /// Extract the outermost `{ … }` JSON object from `s` (tolerant of any -/// non-JSON preamble the tool might print before the object). +/// non-JSON text printed around it). fn extract_json(s: &str) -> Option<&str> { let start = s.find('{')?; let end = s.rfind('}')?; - if end >= start { - Some(&s[start..=end]) - } else { - None - } + (end >= start).then(|| &s[start..=end]) } /// Parse the findings out of an `agda-unused` `message`. Each finding is a /// location line (`…/File.agda:line,col-col`) followed by an indented -/// description line (` ''`). +/// description line (`unused import ‘Name’`). fn parse_findings(message: &str) -> Vec<(PathBuf, Option, String)> { let lines: Vec<&str> = message.lines().collect(); let mut out = Vec::new(); @@ -142,7 +146,7 @@ fn parse_findings(message: &str) -> Vec<(PathBuf, Option, String)> { while i < lines.len() { if let Some((file, line)) = parse_location(lines[i]) { // The description is the next non-empty line that is not itself a - // location (indented ` ''`). + // location (the indented ` ‘’`). let mut desc = String::new(); if i + 1 < lines.len() { let next = lines[i + 1].trim(); @@ -162,13 +166,12 @@ fn parse_findings(message: &str) -> Vec<(PathBuf, Option, String)> { /// 1-based line number. Tolerant: the trailing column/range part is optional. fn parse_location(line: &str) -> Option<(PathBuf, Option)> { let trimmed = line.trim(); - // Anchor on the `.agda:` boundary so paths containing `:` (unlikely) or - // colons elsewhere don't confuse the split. + // Anchor on the `.agda:` boundary so colons elsewhere don't confuse it. let marker = ".agda:"; let idx = trimmed.rfind(marker)?; let file = PathBuf::from(&trimmed[..idx + ".agda".len()]); let rest = &trimmed[idx + marker.len()..]; - // `rest` looks like `12,3-8` or `12,3-13,5`; take the leading integer. + // `rest` looks like `5,1-19` or `5,1-9,4`; take the leading integer. let lineno = rest .split(|c: char| !c.is_ascii_digit()) .find(|s| !s.is_empty()) @@ -180,26 +183,38 @@ fn parse_location(line: &str) -> Option<(PathBuf, Option)> { mod tests { use super::*; + // The wrapper agda-unused actually emits (captured live, local mode, on a + // fixture with an unused import). Note the Unicode quotes ‘ ’. + const REAL_UNUSED: &str = + r#"{"message":"/p/Main.agda:5,1-19\n unused import ‘Helper’","type":"unused"}"#; + const REAL_NONE: &str = r#"{"message":"No unused code.","type":"none"}"#; + #[test] - fn absent_binary_degrades_gracefully() { - // `run_one` against a guaranteed-absent binary name is exercised - // indirectly: find_unused with a bogus PATH can't be forced here, so - // we assert the parser/JSON layers instead. The not-found path is the - // `Ok(None)` arm of `run_one` (see also crate::agda). - let o = UnusedOutcome::default(); - assert!(!o.available); - assert!(o.diagnostics.is_empty()); + fn default_outcome_is_unavailable_and_empty() { + let c = UnusedCheck::default(); + assert!(!c.available); + assert!(c.kind.is_none()); + assert!(c.diagnostics.is_empty()); } #[test] fn extract_json_finds_object_amid_noise() { assert_eq!( - extract_json("preamble {\"type\":\"none\"} trailing"), + extract_json("warn: blah {\"type\":\"none\"} trailing"), Some("{\"type\":\"none\"}") ); assert_eq!(extract_json("no object here"), None); } + #[test] + fn deserialises_real_wrappers() { + let unused: UnusedJson = serde_json::from_str(extract_json(REAL_UNUSED).unwrap()).unwrap(); + assert_eq!(unused.kind, "unused"); + assert!(unused.message.contains("unused import")); + let none: UnusedJson = serde_json::from_str(extract_json(REAL_NONE).unwrap()).unwrap(); + assert_eq!(none.kind, "none"); + } + #[test] fn parse_location_reads_path_and_line() { let (f, l) = parse_location("/home/u/proj/Foo/Bar.agda:12,3-8").unwrap(); @@ -208,23 +223,19 @@ mod tests { } #[test] - fn parse_location_tolerates_line_range() { - let (_f, l) = parse_location("X.agda:7,1-9,4").unwrap(); - assert_eq!(l, Some(7)); - } - - #[test] - fn parse_location_rejects_non_location() { - assert!(parse_location(" unused import 'Foo'").is_none()); + fn parse_location_tolerates_line_range_and_rejects_non_location() { + assert_eq!(parse_location("X.agda:7,1-9,4").unwrap().1, Some(7)); + assert!(parse_location(" unused import ‘Foo’").is_none()); } #[test] - fn parse_findings_pairs_location_with_description() { - let msg = "/p/Main.agda:3,1-19\n unused import 'Unused'\n"; + fn parse_findings_pairs_real_location_with_description() { + // The `message` payload of REAL_UNUSED, with the \n unescaped. + let msg = "/p/Main.agda:5,1-19\n unused import ‘Helper’"; let found = parse_findings(msg); assert_eq!(found.len(), 1); assert_eq!(found[0].0, PathBuf::from("/p/Main.agda")); - assert_eq!(found[0].1, Some(3)); - assert_eq!(found[0].2, "unused import 'Unused'"); + assert_eq!(found[0].1, Some(5)); + assert_eq!(found[0].2, "unused import ‘Helper’"); } } diff --git a/tests/fixtures/unused/Helper.agda b/tests/fixtures/unused/Helper.agda index a15ed48..04dbc6c 100644 --- a/tests/fixtures/unused/Helper.agda +++ b/tests/fixtures/unused/Helper.agda @@ -1,6 +1,6 @@ +{-# OPTIONS --safe --without-K #-} module Helper where --- A trivial, dependency-free definition. Nothing references it, so a --- whole-project (`--global`) agda-unused pass should also flag it. +-- A trivial, dependency-free definition. helper : Set₁ helper = Set diff --git a/tests/fixtures/unused/Main.agda b/tests/fixtures/unused/Main.agda index 1cf2724..ada4b01 100644 --- a/tests/fixtures/unused/Main.agda +++ b/tests/fixtures/unused/Main.agda @@ -1,5 +1,6 @@ +{-# OPTIONS --safe --without-K #-} module Main where -- Imports Helper but uses nothing from it: a genuine unused import, which is --- exactly what `agda-unused` should report (re-emitted as `unused-import`). +-- exactly what `agda-unused` reports (re-emitted as `unused-import`). open import Helper