diff --git a/README.md b/README.md index adc500a..e7ce920 100644 --- a/README.md +++ b/README.md @@ -12,12 +12,37 @@ record. - `Workspace` struct with four-state dir layout (`inbox`, `working`, `proven`, `rejected`) - Filesystem watcher (`notify`-based) -- Two linter rules: +- Linter rules: - `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}` - - `orphan-module` — `.agda` file not imported from `All.agda` -- CLI (`arghda`) with subcommands: `init`, `scan`, `watch` - -Not yet: `promote`, `reject`, `dag` (v0.1.x). + - `orphan-module` — `.agda` file not reachable from any CI root (roots + are auto-discovered as `All.agda`/`Smoke.agda`, or passed via `--entry`; + reachability is the *union*, so a module verified from any root is not + an orphan) + - `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` comment +- Workspace state machine — transitions are file moves, each logged to + `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`, + `invalidate`) +- `dag` — emits the dependency-DAG JSON (nodes + import edges + blocked + list) for a source tree: the contract a visual layer consumes +- `check` — runs Agda on a file and combines the typecheck verdict with the + lint report (degrades gracefully when `agda` is absent) +- First-class import graph (the `graph` module, lifted out of the orphan rule) +- CLI (`arghda`): `init`, `scan`, `check`, `dag`, `claim`, `promote`, + `reject`, `requeue`, `invalidate`, `events`, `watch` + +Dogfooded against the echo-types corpus (193 modules): `dag` emits the +903-edge import graph; multi-root discovery (5 roots: `All.agda`, +`Smoke.agda`, `Ordinal/Buchholz/Smoke.agda`, `characteristic/All.agda`, +`examples/All.agda`) narrows orphan reports from 38 to the 17 genuine +orphans — the `experimental/echo-additive/` tree (including +`VarianceGate.agda`, the orphan the 2026-06-16 trust audit found by hand) +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: the remaining lint rules (`missing-without-k`, `unpinned-headline`, +`unused-import`, `tab-mix`), content-hash invalidation of `proven`, the +Groove service manifest, and the `.machine_readable/` RSR retrofit. ## Build diff --git a/src/agda.rs b/src/agda.rs new file mode 100644 index 0000000..9894541 --- /dev/null +++ b/src/agda.rs @@ -0,0 +1,81 @@ +//! Shelling out to `agda` to typecheck a file. +//! +//! ArghDA never proves anything itself — it asks Agda. This module runs +//! the typechecker and captures the verdict. If `agda` is not on `PATH` +//! it degrades gracefully (`available: false`) rather than erroring, so +//! the rest of the engine still works in an Agda-less environment (CI +//! linting, DAG extraction, triage moves). + +use anyhow::Result; +use serde::Serialize; +use std::path::Path; +use std::process::Command; + +const TAIL_LINES: usize = 40; + +/// Result of a typecheck attempt. +#[derive(Clone, Debug, Serialize)] +pub struct AgdaOutcome { + /// Whether the `agda` binary was found and executed. + pub available: bool, + /// Process exit code, if the process ran. + pub exit_code: Option, + /// `true` iff agda exited 0. + pub ok: bool, + /// Last few lines of combined stdout+stderr (for surfacing errors). + pub output_tail: String, +} + +impl AgdaOutcome { + fn unavailable() -> Self { + Self { + available: false, + exit_code: None, + ok: false, + output_tail: String::new(), + } + } +} + +/// Typecheck `file` with `include_root` on the search path +/// (`agda -i `). +pub fn check_file(file: &Path, include_root: &Path) -> Result { + let output = Command::new("agda") + .arg("-i") + .arg(include_root) + .arg(file) + .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)); + Ok(AgdaOutcome { + available: true, + exit_code: out.status.code(), + ok: out.status.success(), + output_tail: tail(&combined, TAIL_LINES), + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => Ok(AgdaOutcome::unavailable()), + Err(e) => Err(e.into()), + } +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn tail_keeps_last_n_lines() { + assert_eq!(tail("a\nb\nc\nd", 2), "c\nd"); + assert_eq!(tail("only", 5), "only"); + assert_eq!(tail("", 3), ""); + } +} diff --git a/src/dag.rs b/src/dag.rs new file mode 100644 index 0000000..d6b0f54 --- /dev/null +++ b/src/dag.rs @@ -0,0 +1,152 @@ +//! The DAG document — the JSON contract a visual layer consumes. +//! +//! Builds on the import graph (`crate::graph`) plus a lint pass over every +//! node. The schema follows `docs/arghda-spec.adoc`; `status` is honest +//! about what the engine knows without a typecheck: it is lint-derived +//! (`clean` / `warn` / `blocked`), not a claim of `proven`. Triage status +//! (proven/rejected) attaches when files flow through a workspace and are +//! checked with Agda. + +use crate::diagnostic::Severity; +use crate::graph::{self, Edge}; +use crate::lint::{run_lints, LintContext, LintRule}; +use crate::timestamp::now_rfc3339; +use anyhow::Result; +use serde::Serialize; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::{Path, PathBuf}; + +/// Per-node lint summary: the rule names that fired, by severity. +#[derive(Clone, Debug, Default, Serialize)] +pub struct LintSummary { + pub hard_block: Vec, + pub warn: Vec, +} + +/// A DAG node: an in-tree module with its lint-derived status. +#[derive(Clone, Debug, Serialize)] +pub struct DagNode { + pub id: String, + pub file: PathBuf, + /// `clean` | `warn` | `blocked` (lint-derived; not a proof claim). + pub status: &'static str, + pub lint: LintSummary, +} + +/// A module that cannot advance, and why. +#[derive(Clone, Debug, Serialize)] +pub struct Blocked { + pub node: String, + pub blocked_by: Vec, + pub reason: String, +} + +/// The full emitted document. +#[derive(Clone, Debug, Serialize)] +pub struct DagDocument { + pub version: &'static str, + pub include_root: PathBuf, + pub entry_modules: Vec, + pub generated_at: String, + pub nodes: Vec, + pub edges: Vec, + pub blocked: Vec, +} + +/// Build the DAG document for the source tree at `include_root`, using +/// `entry_modules` (the union of CI roots) for the orphan-reachability rule +/// and `rules` as the lint pack. +pub fn build( + include_root: &Path, + entry_modules: &[PathBuf], + rules: &[Box], +) -> Result { + let graph = graph::build(include_root)?; + let ctx = LintContext { + include_root, + entry_modules, + }; + + let mut nodes = Vec::with_capacity(graph.nodes.len()); + let mut self_blocked: BTreeMap> = BTreeMap::new(); + + for gn in &graph.nodes { + let abs = include_root.join(&gn.file); + let report = run_lints(&abs, &ctx, rules)?; + + let mut summary = LintSummary::default(); + for d in &report.diagnostics { + match d.severity { + Severity::HardBlock => summary.hard_block.push(d.rule.clone()), + Severity::Warn => summary.warn.push(d.rule.clone()), + } + } + summary.hard_block.sort(); + summary.hard_block.dedup(); + summary.warn.sort(); + summary.warn.dedup(); + + let status = if !summary.hard_block.is_empty() { + self_blocked.insert(gn.id.clone(), summary.hard_block.clone()); + "blocked" + } else if !summary.warn.is_empty() { + "warn" + } else { + "clean" + }; + + nodes.push(DagNode { + id: gn.id.clone(), + file: gn.file.clone(), + status, + lint: summary, + }); + } + + let blocked = compute_blocked(&self_blocked, &graph.edges); + + Ok(DagDocument { + version: "0.1", + include_root: include_root.to_path_buf(), + entry_modules: entry_modules.to_vec(), + generated_at: now_rfc3339(), + nodes, + edges: graph.edges, + blocked, + }) +} + +/// A node is blocked if it hard-blocks on its own (`reason` = the rule +/// names) or if any module it imports is itself hard-blocked +/// (`blocked_by` = those prerequisites). Both are surfaced so the visual +/// layer can colour a node red for its own fault *and* show the upstream +/// wall it is waiting on. +fn compute_blocked(self_blocked: &BTreeMap>, edges: &[Edge]) -> Vec { + let mut out = Vec::new(); + + for (node, rules) in self_blocked { + out.push(Blocked { + node: node.clone(), + blocked_by: Vec::new(), + reason: rules.join(", "), + }); + } + + // Group each node's hard-blocked direct prerequisites. + let mut deps: BTreeMap> = BTreeMap::new(); + for e in edges { + if self_blocked.contains_key(&e.to) { + deps.entry(e.from.clone()).or_default().insert(e.to.clone()); + } + } + for (node, prereqs) in deps { + out.push(Blocked { + node, + blocked_by: prereqs.into_iter().collect(), + reason: "prerequisite not clean".to_string(), + }); + } + + out.sort_by(|a, b| (&a.node, &a.reason).cmp(&(&b.node, &b.reason))); + out +} diff --git a/src/event.rs b/src/event.rs new file mode 100644 index 0000000..9026162 --- /dev/null +++ b/src/event.rs @@ -0,0 +1,111 @@ +//! The triage event stream. +//! +//! Every state transition appends one JSON object (one line) to +//! `/.arghda/events.jsonl`. The log is append-only and is the +//! audit trail a downstream visual layer replays to reconstruct history. + +use crate::timestamp::now_rfc3339; +use crate::workspace::State; +use anyhow::{Context, Result}; +use serde::{Deserialize, Serialize}; +use std::fs::{self, OpenOptions}; +use std::io::Write; +use std::path::{Path, PathBuf}; + +/// What happened. Mirrors the transition table in `arghda-spec.adoc`. +#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum EventKind { + Claim, + Promote, + Reject, + Requeue, + Invalidate, +} + +/// A single transition record. +#[derive(Clone, Debug, Serialize, Deserialize)] +pub struct Event { + pub ts: String, + pub kind: EventKind, + pub file: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub from: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub to: Option, + #[serde(skip_serializing_if = "Option::is_none")] + pub note: Option, +} + +impl Event { + pub fn new(kind: EventKind, file: impl Into) -> Self { + Self { + ts: now_rfc3339(), + kind, + file: file.into(), + from: None, + to: None, + note: None, + } + } + + pub fn with_from(mut self, from: State) -> Self { + self.from = Some(from); + self + } + + pub fn with_to(mut self, to: State) -> Self { + self.to = Some(to); + self + } + + pub fn with_note(mut self, note: Option) -> Self { + self.note = note; + self + } +} + +/// File name of the rolling event log, under `/.arghda/`. +pub const EVENTS_FILE: &str = "events.jsonl"; + +fn events_path(ws_root: &Path) -> PathBuf { + ws_root.join(".arghda").join(EVENTS_FILE) +} + +/// Append one event as a JSON line. Creates `.arghda/` if absent. +pub fn append(ws_root: impl AsRef, ev: &Event) -> Result<()> { + let ws_root = ws_root.as_ref(); + let meta = ws_root.join(".arghda"); + fs::create_dir_all(&meta).with_context(|| format!("creating {}", meta.display()))?; + let path = events_path(ws_root); + let mut line = serde_json::to_string(ev).context("serialising event")?; + line.push('\n'); + let mut f = OpenOptions::new() + .create(true) + .append(true) + .open(&path) + .with_context(|| format!("opening {}", path.display()))?; + f.write_all(line.as_bytes()) + .with_context(|| format!("appending to {}", path.display()))?; + Ok(()) +} + +/// Read the whole event log in order. Empty if the log does not exist yet. +pub fn read_all(ws_root: impl AsRef) -> Result> { + let path = events_path(ws_root.as_ref()); + if !path.is_file() { + return Ok(Vec::new()); + } + let contents = + fs::read_to_string(&path).with_context(|| format!("reading {}", path.display()))?; + let mut out = Vec::new(); + for (i, line) in contents.lines().enumerate() { + if line.trim().is_empty() { + continue; + } + let ev: Event = serde_json::from_str(line) + .with_context(|| format!("parsing {} line {}", path.display(), i + 1))?; + out.push(ev); + } + Ok(out) +} diff --git a/src/graph.rs b/src/graph.rs new file mode 100644 index 0000000..faf837f --- /dev/null +++ b/src/graph.rs @@ -0,0 +1,293 @@ +//! First-class Agda import graph. +//! +//! The reachability primitives (`module_name_of`, `module_to_path`, +//! `direct_imports`, `transitive_imports`) used to live private inside the +//! `orphan-module` lint rule, which computed the edges and then threw them +//! away. They are promoted here so the `dag` command (and any downstream +//! visual layer) can consume the actual dependency graph. The orphan rule +//! now reuses these. +//! +//! Edges are kept only to modules that resolve to a file *inside* the +//! include root: the graph is the project's internal dependency DAG, so +//! stdlib / external imports are intentionally omitted. + +use anyhow::{Context, Result}; +use serde::Serialize; +use std::collections::{BTreeMap, HashSet}; +use std::fs; +use std::path::{Path, PathBuf}; +use walkdir::WalkDir; + +/// Relative module path for `file` under `include_root`, dotted +/// (`Ordinal/Closure.agda` → `Ordinal.Closure`). `None` if `file` is +/// outside the root or has a non-normal component. +pub fn module_name_of(file: &Path, include_root: &Path) -> Option { + let rel = file.strip_prefix(include_root).ok()?; + let stem = rel.with_extension(""); + let mut parts = Vec::new(); + for comp in stem.components() { + let std::path::Component::Normal(s) = comp else { + return None; + }; + parts.push(s.to_str()?.to_string()); + } + if parts.is_empty() { + return None; + } + Some(parts.join(".")) +} + +/// Inverse of [`module_name_of`]: dotted module name → file path. +pub fn module_to_path(module: &str, include_root: &Path) -> PathBuf { + let mut p = include_root.to_path_buf(); + for part in module.split('.') { + p.push(part); + } + p.set_extension("agda"); + p +} + +/// Extract module names appearing in `import …` / `open import …` +/// top-level forms of `file`. Tolerant: takes the first token after +/// `import`; ignores `hiding`/`using`/`as`/`public` modifiers and `--` +/// line comments. +pub fn direct_imports(file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + let mut out = Vec::new(); + for line in contents.lines() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; + } + let tokens: Vec<&str> = trimmed.split_whitespace().collect(); + let Some(i) = tokens.iter().position(|&t| t == "import") else { + continue; + }; + // Require `import` to be top-level or directly after `open`, so we + // don't trip on the word appearing mid-expression. + if i > 0 && tokens[i - 1] != "open" { + continue; + } + let Some(module) = tokens.get(i + 1) else { + continue; + }; + let cleaned = + module.trim_end_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); + if !cleaned.is_empty() { + out.push(cleaned.to_string()); + } + } + Ok(out) +} + +/// Set of module names transitively reachable from `entry` by following +/// `open import` edges. Missing files (stdlib / external) are skipped. +pub fn transitive_imports(entry: &Path, include_root: &Path) -> Result> { + let mut reachable: HashSet = HashSet::new(); + let mut worklist: Vec = Vec::new(); + + if let Some(m) = module_name_of(entry, include_root) { + reachable.insert(m.clone()); + worklist.push(m); + } else { + for imp in direct_imports(entry)? { + if reachable.insert(imp.clone()) { + worklist.push(imp); + } + } + } + + while let Some(module) = worklist.pop() { + let path = module_to_path(&module, include_root); + if !path.is_file() { + continue; + } + for imp in direct_imports(&path)? { + if reachable.insert(imp.clone()) { + worklist.push(imp); + } + } + } + + Ok(reachable) +} + +/// Union of the modules reachable from each root in `roots`. A module +/// verified from *any* CI entry point counts as reachable. +pub fn reachable_from_roots(roots: &[PathBuf], include_root: &Path) -> Result> { + let mut all = HashSet::new(); + for root in roots { + for m in transitive_imports(root, include_root)? { + all.insert(m); + } + } + Ok(all) +} + +/// Discover conventional CI root modules under `include_root`: every file +/// named `All.agda` or `Smoke.agda`, at any depth. These are the entry +/// points an estate `--safe --without-K` workspace registers its verified +/// suite from (e.g. echo-types has `All.agda`, `Smoke.agda`, +/// `characteristic/All.agda`, `examples/All.agda`, `tutorial/All.agda`). +pub fn discover_roots(include_root: &Path) -> Vec { + let mut roots = Vec::new(); + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("agda") { + continue; + } + if matches!( + path.file_name().and_then(|s| s.to_str()), + Some("All.agda") | Some("Smoke.agda") + ) { + roots.push(path.to_path_buf()); + } + } + roots.sort(); + roots +} + +/// A node in the import graph: a `.agda` source file and its module name. +#[derive(Clone, Debug, Serialize)] +pub struct GraphNode { + pub id: String, + /// Path relative to the include root. + pub file: PathBuf, +} + +/// An `imports` edge from one in-tree module to another. +#[derive(Clone, Debug, Serialize)] +pub struct Edge { + pub from: String, + pub to: String, + pub kind: &'static str, +} + +/// The internal import DAG of an Agda source tree. +#[derive(Clone, Debug, Serialize)] +pub struct ImportGraph { + pub nodes: Vec, + pub edges: Vec, +} + +/// Walk every `.agda` file under `include_root` and build the internal +/// import graph. Output is deterministic (nodes and edges are sorted), +/// which keeps the emitted DAG stable for diffing and tests. +pub fn build(include_root: &Path) -> Result { + // module id -> relative file path, for every in-tree module. + let mut by_id: BTreeMap = BTreeMap::new(); + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("agda") { + continue; + } + if let Some(id) = module_name_of(path, include_root) { + let rel = path + .strip_prefix(include_root) + .unwrap_or(path) + .to_path_buf(); + by_id.insert(id, rel); + } + } + + let nodes: Vec = by_id + .iter() + .map(|(id, file)| GraphNode { + id: id.clone(), + file: file.clone(), + }) + .collect(); + + let mut edges = Vec::new(); + for id in by_id.keys() { + let path = module_to_path(id, include_root); + for imp in direct_imports(&path)? { + // Keep only edges to modules that exist in-tree. + if by_id.contains_key(&imp) { + edges.push(Edge { + from: id.clone(), + to: imp, + kind: "imports", + }); + } + } + } + edges.sort_by(|a, b| (&a.from, &a.to).cmp(&(&b.from, &b.to))); + edges.dedup_by(|a, b| a.from == b.from && a.to == b.to); + + Ok(ImportGraph { nodes, edges }) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn module_name_roundtrip() { + let root = Path::new("/r"); + let file = Path::new("/r/Ordinal/Closure.agda"); + let name = module_name_of(file, root).unwrap(); + assert_eq!(name, "Ordinal.Closure"); + assert_eq!( + module_to_path(&name, root), + PathBuf::from("/r/Ordinal/Closure.agda") + ); + } + + #[test] + fn parses_open_import_with_modifiers() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "module M where\n\ + open import Data.Nat using (ℕ)\n\ + open import Foo.Bar\n\ + import Baz as B\n\ + -- open import IgnoredComment\n", + ) + .unwrap(); + let imports = direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Data.Nat".to_string())); + assert!(imports.contains(&"Foo.Bar".to_string())); + assert!(imports.contains(&"Baz".to_string())); + assert!(!imports.iter().any(|i| i.contains("Ignored"))); + } + + #[test] + fn discover_and_reach_over_multiple_roots() { + let tmp = tempfile::tempdir().unwrap(); + let r = tmp.path(); + std::fs::write(r.join("All.agda"), "module All where\nopen import Used\n").unwrap(); + std::fs::write( + r.join("Smoke.agda"), + "module Smoke where\nopen import Other\n", + ) + .unwrap(); + std::fs::write(r.join("Used.agda"), "module Used where\n").unwrap(); + std::fs::write(r.join("Other.agda"), "module Other where\n").unwrap(); + std::fs::write(r.join("Orphan.agda"), "module Orphan where\n").unwrap(); + + let roots = discover_roots(r); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert_eq!(roots.len(), 2, "discovers All.agda + Smoke.agda: {names:?}"); + assert!(names.contains(&"All.agda".to_string())); + assert!(names.contains(&"Smoke.agda".to_string())); + + // Reachability is the UNION: Used (via All) and Other (via Smoke) + // are both reachable; Orphan (via neither) is not. + let reachable = reachable_from_roots(&roots, r).unwrap(); + assert!(reachable.contains("Used")); + assert!(reachable.contains("Other")); + assert!(!reachable.contains("Orphan")); + } +} diff --git a/src/lib.rs b/src/lib.rs index db103bd..5087e00 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -3,11 +3,20 @@ //! Public surface is intentionally small: `Workspace`, the lint traits, //! and the diagnostic types. The CLI in `main.rs` is a thin consumer. +pub mod agda; +pub mod dag; pub mod diagnostic; +pub mod event; +pub mod graph; pub mod lint; +pub mod timestamp; pub mod watcher; pub mod workspace; +pub use agda::{check_file, AgdaOutcome}; +pub use dag::{build as build_dag, DagDocument}; pub use diagnostic::{Diagnostic, LintReport, Severity}; +pub use event::{Event, EventKind}; +pub use graph::{build as build_graph, ImportGraph}; pub use lint::{default_rules, run_lints, LintRule}; pub use workspace::{State, Workspace}; diff --git a/src/lint/mod.rs b/src/lint/mod.rs index b4ec3b8..0d0b5dd 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -1,8 +1,9 @@ use crate::diagnostic::LintReport; use anyhow::Result; -use std::path::Path; +use std::path::{Path, PathBuf}; pub mod orphan_module; +pub mod postulate; pub mod safe_pragma; /// Context handed to every rule. @@ -11,8 +12,10 @@ pub struct LintContext<'a> { /// Agda include root; `.agda` files' module names are computed /// relative to this path. pub include_root: &'a Path, - /// Path to the `All.agda` (or equivalent) entry module. - pub entry_module: &'a Path, + /// The root modules (e.g. `All.agda`, `Smoke.agda`). Reachability is + /// computed from the *union* of these, so a module verified from any + /// CI entry point is not an orphan. + pub entry_modules: &'a [PathBuf], } pub trait LintRule: Send + Sync { @@ -24,6 +27,7 @@ pub fn default_rules() -> Vec> { vec![ Box::new(safe_pragma::SafePragma), Box::new(orphan_module::OrphanModule), + Box::new(postulate::UnjustifiedPostulate), ] } diff --git a/src/lint/orphan_module.rs b/src/lint/orphan_module.rs index 327a5a6..bd33a99 100644 --- a/src/lint/orphan_module.rs +++ b/src/lint/orphan_module.rs @@ -1,9 +1,8 @@ use super::{LintContext, LintRule}; use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use crate::graph::{module_name_of, reachable_from_roots}; use anyhow::{Context, Result}; -use std::collections::HashSet; -use std::fs; -use std::path::{Path, PathBuf}; +use std::path::Path; pub struct OrphanModule; @@ -17,18 +16,17 @@ impl LintRule for OrphanModule { return Ok(()); // file sits outside include_root; nothing to say }; - // The entry module itself is never an orphan of itself. - if Some(module.as_str()) == module_name_of(ctx.entry_module, ctx.include_root).as_deref() { + // A root module is never an orphan of itself. + let is_root = ctx + .entry_modules + .iter() + .any(|root| module_name_of(root, ctx.include_root).as_deref() == Some(module.as_str())); + if is_root { return Ok(()); } - let reachable = - transitive_imports(ctx.entry_module, ctx.include_root).with_context(|| { - format!( - "computing transitive imports from {}", - ctx.entry_module.display() - ) - })?; + let reachable = reachable_from_roots(ctx.entry_modules, ctx.include_root) + .context("computing reachability from root modules")?; if !reachable.contains(&module) { report.push(Diagnostic { @@ -36,9 +34,9 @@ impl LintRule for OrphanModule { severity: Severity::HardBlock, file: file.to_path_buf(), message: format!( - "module `{}` is not reachable via imports from `{}`", + "module `{}` is not reachable via imports from any of the {} root module(s)", module, - ctx.entry_module.display() + ctx.entry_modules.len() ), line: None, }); @@ -47,135 +45,3 @@ impl LintRule for OrphanModule { Ok(()) } } - -/// Relative module path for `file` under `include_root`. -/// Returns `None` if `file` is outside the root or not a `.agda` source. -fn module_name_of(file: &Path, include_root: &Path) -> Option { - let rel = file.strip_prefix(include_root).ok()?; - let stem = rel.with_extension(""); - let mut parts = Vec::new(); - for comp in stem.components() { - let std::path::Component::Normal(s) = comp else { - return None; - }; - parts.push(s.to_str()?.to_string()); - } - if parts.is_empty() { - return None; - } - Some(parts.join(".")) -} - -fn module_to_path(module: &str, include_root: &Path) -> PathBuf { - let mut p = include_root.to_path_buf(); - for part in module.split('.') { - p.push(part); - } - p.set_extension("agda"); - p -} - -fn transitive_imports(entry: &Path, include_root: &Path) -> Result> { - let mut reachable: HashSet = HashSet::new(); - let mut worklist: Vec = Vec::new(); - - if let Some(m) = module_name_of(entry, include_root) { - reachable.insert(m.clone()); - worklist.push(m); - } else { - // Entry is outside the include root; seed with its imports directly. - for imp in direct_imports(entry)? { - if reachable.insert(imp.clone()) { - worklist.push(imp); - } - } - } - - while let Some(module) = worklist.pop() { - let path = module_to_path(&module, include_root); - // Missing files (stdlib, external deps) are silently skipped. - if !path.is_file() { - continue; - } - for imp in direct_imports(&path)? { - if reachable.insert(imp.clone()) { - worklist.push(imp); - } - } - } - - Ok(reachable) -} - -/// Extract module names appearing in `import ...` / `open import ...` -/// top-level forms of `file`. Tolerant: stops at the first token after -/// `import`; ignores `hiding`, `using`, `as`, `public` modifiers. -fn direct_imports(file: &Path) -> Result> { - let contents = - fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; - let mut out = Vec::new(); - for line in contents.lines() { - let trimmed = line.trim_start(); - if trimmed.starts_with("--") { - continue; - } - // Accept `import X`, `open import X`, `open import X as Y`, etc. - let tokens: Vec<&str> = trimmed.split_whitespace().collect(); - let idx = tokens.iter().position(|&t| t == "import"); - let Some(i) = idx else { continue }; - // Reject lines where `import` is inside a string literal or embedded - // in a larger identifier; a cheap heuristic is to require that the - // token before `import` is empty, `open`, or absent. - if i > 0 { - let prev = tokens[i - 1]; - if prev != "open" { - continue; - } - } - let Some(module) = tokens.get(i + 1) else { - continue; - }; - // Strip trailing punctuation Agda never allows in module paths. - let cleaned = - module.trim_end_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); - if cleaned.is_empty() { - continue; - } - out.push(cleaned.to_string()); - } - Ok(out) -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn module_name_roundtrip() { - let root = Path::new("/r"); - let file = Path::new("/r/Ordinal/Closure.agda"); - let name = module_name_of(file, root).unwrap(); - assert_eq!(name, "Ordinal.Closure"); - let back = module_to_path(&name, root); - assert_eq!(back, PathBuf::from("/r/Ordinal/Closure.agda")); - } - - #[test] - fn parses_open_import_with_modifiers() { - let tmp = tempfile::NamedTempFile::new().unwrap(); - std::fs::write( - tmp.path(), - "module M where\n\ - open import Data.Nat using (ℕ)\n\ - open import Foo.Bar\n\ - import Baz as B\n\ - -- open import IgnoredComment\n", - ) - .unwrap(); - let imports = direct_imports(tmp.path()).unwrap(); - assert!(imports.contains(&"Data.Nat".to_string())); - assert!(imports.contains(&"Foo.Bar".to_string())); - assert!(imports.contains(&"Baz".to_string())); - assert!(!imports.iter().any(|i| i.contains("Ignored"))); - } -} diff --git a/src/lint/postulate.rs b/src/lint/postulate.rs new file mode 100644 index 0000000..a335494 --- /dev/null +++ b/src/lint/postulate.rs @@ -0,0 +1,111 @@ +//! `unjustified-postulate` — flag `postulate` openers that lack an +//! adjacent `-- JUSTIFY:` rationale. +//! +//! Postulates are the canonical way a "proof" hides a hole, so the estate +//! discipline (echo-types / absolute-zero) is: a postulate is permitted +//! only if it is explicitly justified. This rule makes the bare case a +//! hard-block, matching `arghda-spec.adoc`'s rule list. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct UnjustifiedPostulate; + +impl LintRule for UnjustifiedPostulate { + fn name(&self) -> &'static str { + "unjustified-postulate" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + let lines: Vec<&str> = contents.lines().collect(); + + for (i, line) in lines.iter().enumerate() { + if !is_postulate_opener(line) { + continue; + } + if !justified_above(&lines, i) { + report.push(Diagnostic { + rule: self.name().to_string(), + severity: Severity::HardBlock, + file: file.to_path_buf(), + message: "`postulate` without an adjacent `-- JUSTIFY:` comment".to_string(), + line: Some(i + 1), + }); + } + } + Ok(()) + } +} + +/// A line whose first token is `postulate` (a block opener `postulate` on +/// its own line, or an inline `postulate name : T`). Comment lines are +/// excluded. +fn is_postulate_opener(line: &str) -> bool { + let t = line.trim_start(); + if t.starts_with("--") { + return false; + } + t == "postulate" || t.starts_with("postulate ") || t.starts_with("postulate\t") +} + +/// True if the nearest non-blank line above `idx` is a `-- JUSTIFY:` comment. +fn justified_above(lines: &[&str], idx: usize) -> bool { + for j in (0..idx).rev() { + let t = lines[j].trim(); + if t.is_empty() { + continue; + } + return t.starts_with("-- JUSTIFY:"); + } + false +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + + fn lint_str(body: &str) -> LintReport { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), body).unwrap(); + let roots = [tmp.path().to_path_buf()]; + let ctx = LintContext { + include_root: tmp.path().parent().unwrap(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(UnjustifiedPostulate)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn bare_postulate_is_flagged() { + let r = lint_str("module M where\npostulate\n foo : Set\n"); + assert!(r.has_hard_block()); + assert_eq!(r.diagnostics[0].line, Some(2)); + } + + #[test] + fn justified_postulate_is_clean() { + let r = lint_str( + "module M where\n-- JUSTIFY: classical axiom, see ADR-007\npostulate\n lem : Set\n", + ); + assert!(!r.has_hard_block(), "got: {:?}", r.diagnostics); + } + + #[test] + fn inline_postulate_without_justify_is_flagged() { + let r = lint_str("module M where\npostulate foo : Set\n"); + assert!(r.has_hard_block()); + } + + #[test] + fn word_postulated_is_not_an_opener() { + let r = lint_str("module M where\n-- this is postulated elsewhere\nfoo : Set\n"); + assert!(!r.has_hard_block()); + } +} diff --git a/src/main.rs b/src/main.rs index f035efa..a6cd7cc 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,11 +1,17 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; -use arghda_core::{default_rules, run_lints, watcher, Workspace}; +use arghda_core::{ + build_dag, check_file, default_rules, event, graph, run_lints, watcher, LintRule, State, + Workspace, +}; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; use std::time::Duration; use walkdir::WalkDir; +/// A lint pack (boxed trait objects). +type RuleSet = Vec>; + #[derive(Parser)] #[command( name = "arghda", @@ -25,14 +31,46 @@ enum Cmd { Scan { /// Directory containing `.agda` files; treated as the include root. path: PathBuf, - /// Entry module used for orphan detection. Defaults to - /// `/All.agda`. + /// Root module for orphan detection; repeatable. Defaults to every + /// `All.agda`/`Smoke.agda` discovered under PATH. #[arg(long)] - entry: Option, + entry: Vec, /// Emit the report as JSON instead of human-readable text. #[arg(long)] json: bool, }, + /// Typecheck one file with Agda and lint it; report the verdict. + Check { + /// The `.agda` file to check. + file: PathBuf, + /// Agda include root. Defaults to the file's directory. + #[arg(long)] + include_root: Option, + /// Emit the report as JSON. + #[arg(long)] + json: bool, + }, + /// Emit the dependency DAG (JSON) for the source tree at PATH. + Dag { + /// Directory containing `.agda` files; treated as the include root. + path: PathBuf, + /// Root module for orphan detection; repeatable. Defaults to every + /// `All.agda`/`Smoke.agda` discovered under PATH. + #[arg(long)] + entry: Vec, + }, + /// Claim a file: inbox -> working. + Claim { workspace: PathBuf, file: String }, + /// Promote a file: working -> proven. + Promote { workspace: PathBuf, file: String }, + /// Reject a file: working -> rejected. + Reject { workspace: PathBuf, file: String }, + /// Re-queue a file: rejected -> inbox. + Requeue { workspace: PathBuf, file: String }, + /// Invalidate a proven file: proven -> inbox. + Invalidate { workspace: PathBuf, file: String }, + /// Print the workspace event log. + Events { workspace: PathBuf }, /// Watch `inbox/` and `working/` in a workspace; print events. Watch { workspace: PathBuf }, } @@ -44,29 +82,39 @@ fn main() -> Result<()> { let ws = Workspace::init(&path)?; println!("initialised workspace at {}", ws.root().display()); } - Cmd::Scan { path, entry, json } => scan(&path, entry.as_deref(), json)?, + Cmd::Scan { path, entry, json } => scan(&path, &entry, json)?, + Cmd::Check { + file, + include_root, + json, + } => check(&file, include_root.as_deref(), json)?, + Cmd::Dag { path, entry } => dag(&path, &entry)?, + Cmd::Claim { workspace, file } => { + transition(&workspace, &file, State::Inbox, State::Working)? + } + Cmd::Promote { workspace, file } => { + transition(&workspace, &file, State::Working, State::Proven)? + } + Cmd::Reject { workspace, file } => { + transition(&workspace, &file, State::Working, State::Rejected)? + } + Cmd::Requeue { workspace, file } => { + transition(&workspace, &file, State::Rejected, State::Inbox)? + } + Cmd::Invalidate { workspace, file } => { + transition(&workspace, &file, State::Proven, State::Inbox)? + } + Cmd::Events { workspace } => events(&workspace)?, Cmd::Watch { workspace } => watch(&workspace)?, } Ok(()) } -fn scan(include_root: &Path, entry: Option<&Path>, json: bool) -> Result<()> { - let entry_buf; - let entry = match entry { - Some(e) => e, - None => { - entry_buf = include_root.join("All.agda"); - &entry_buf - } - }; - if !entry.is_file() { - anyhow::bail!("entry module not found: {}", entry.display()); - } - - let rules = default_rules(); +fn scan(include_root: &Path, entry: &[PathBuf], json: bool) -> Result<()> { + let (roots, rules) = resolve_roots_and_rules(include_root, entry)?; let ctx = LintContext { include_root, - entry_module: entry, + entry_modules: &roots, }; let mut reports = Vec::new(); @@ -92,7 +140,7 @@ fn scan(include_root: &Path, entry: Option<&Path>, json: bool) -> Result<()> { let payload = serde_json::json!({ "version": "0.1", "include_root": include_root, - "entry_module": entry, + "entry_modules": roots, "files_scanned": reports.len(), "hard_blocks": hard_blocks, "warns": warns, @@ -106,11 +154,7 @@ fn scan(include_root: &Path, entry: Option<&Path>, json: bool) -> Result<()> { } println!("{}", report.file.display()); for d in &report.diagnostics { - let tag = match d.severity { - arghda_core::Severity::HardBlock => "BLOCK", - arghda_core::Severity::Warn => "warn", - }; - println!(" [{}] {}: {}", tag, d.rule, d.message); + println!(" [{}] {}: {}", sev_tag(d.severity), d.rule, d.message); } } println!( @@ -123,10 +167,133 @@ fn scan(include_root: &Path, entry: Option<&Path>, json: bool) -> Result<()> { Ok(()) } +fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { + if !file.is_file() { + anyhow::bail!("file not found: {}", file.display()); + } + let root_buf; + let include_root = match include_root { + Some(r) => r, + None => { + root_buf = file.parent().unwrap_or(Path::new(".")).to_path_buf(); + &root_buf + } + }; + + // The orphan rule self-skips when the file is its own root, which is + // exactly what a single-file check wants. + let rules = default_rules(); + let roots = [file.to_path_buf()]; + let ctx = LintContext { + include_root, + entry_modules: &roots, + }; + let report = + run_lints(file, &ctx, &rules).with_context(|| format!("linting {}", file.display()))?; + let agda = check_file(file, include_root)?; + + let verdict = if !agda.available { + "agda-unavailable" + } else if agda.ok && !report.has_hard_block() { + "proven-eligible" + } else { + "rejected" + }; + + if json { + let payload = serde_json::json!({ + "version": "0.1", + "file": file, + "agda": agda, + "lint": report, + "verdict": verdict, + }); + println!("{}", serde_json::to_string_pretty(&payload)?); + } else { + println!("{}", file.display()); + if agda.available { + println!( + " agda: exit {}, {}", + agda.exit_code + .map(|c| c.to_string()) + .unwrap_or_else(|| "?".into()), + if agda.ok { "ok" } else { "FAILED" } + ); + } else { + println!(" agda: not found on PATH (typecheck skipped)"); + } + for d in &report.diagnostics { + println!(" [{}] {}: {}", sev_tag(d.severity), d.rule, d.message); + } + println!(" verdict: {verdict}"); + } + Ok(()) +} + +fn dag(include_root: &Path, entry: &[PathBuf]) -> Result<()> { + let (roots, rules) = resolve_roots_and_rules(include_root, entry)?; + let doc = build_dag(include_root, &roots, &rules)?; + println!("{}", serde_json::to_string_pretty(&doc)?); + Ok(()) +} + +/// Resolve the root modules and the matching lint pack for `scan`/`dag`. +/// Explicit `--entry` values win; otherwise roots are auto-discovered +/// (`All.agda`/`Smoke.agda`). When no roots can be found, the +/// orphan-module rule is dropped (with a note) rather than flagging every +/// module as an orphan. +fn resolve_roots_and_rules( + include_root: &Path, + entry: &[PathBuf], +) -> Result<(Vec, RuleSet)> { + for e in entry { + if !e.is_file() { + anyhow::bail!("entry module not found: {}", e.display()); + } + } + let roots = if entry.is_empty() { + graph::discover_roots(include_root) + } else { + entry.to_vec() + }; + let rules: RuleSet = if roots.is_empty() { + eprintln!( + "note: no root modules (All.agda/Smoke.agda) found under {}; skipping orphan-module rule", + include_root.display() + ); + default_rules() + .into_iter() + .filter(|r| r.name() != "orphan-module") + .collect() + } else { + default_rules() + }; + Ok((roots, rules)) +} + +fn transition(workspace: &Path, file: &str, from: State, to: State) -> Result<()> { + let ws = Workspace::open(workspace)?; + ws.transition(file, from, to, None)?; + println!("{file}: {} -> {}", from.dir_name(), to.dir_name()); + Ok(()) +} + +fn events(workspace: &Path) -> Result<()> { + let events = event::read_all(workspace)?; + if events.is_empty() { + println!("(no events)"); + return Ok(()); + } + for ev in &events { + println!("{}", serde_json::to_string(ev)?); + } + Ok(()) +} + fn watch(workspace_path: &Path) -> Result<()> { let ws = Workspace::open(workspace_path)?; - let inbox = ws.state_dir(arghda_core::State::Inbox); - let working = ws.state_dir(arghda_core::State::Working); + let inbox = ws.state_dir(State::Inbox); + let working = ws.state_dir(State::Working); let (_w_inbox, rx_inbox) = watcher::watch(&inbox, false)?; let (_w_working, rx_working) = watcher::watch(&working, false)?; @@ -143,3 +310,10 @@ fn watch(workspace_path: &Path) -> Result<()> { } } } + +fn sev_tag(sev: arghda_core::Severity) -> &'static str { + match sev { + arghda_core::Severity::HardBlock => "BLOCK", + arghda_core::Severity::Warn => "warn", + } +} diff --git a/src/timestamp.rs b/src/timestamp.rs new file mode 100644 index 0000000..c3d1cd7 --- /dev/null +++ b/src/timestamp.rs @@ -0,0 +1,71 @@ +//! Dependency-free UTC timestamps. +//! +//! Emits RFC 3339 / ISO-8601 strings (e.g. `2026-06-18T11:45:32Z`) without +//! pulling in `chrono`/`time`, so the build stays hermetic against the +//! committed lockfile. The calendar conversion is Howard Hinnant's +//! `civil_from_days` algorithm (proleptic Gregorian, exact for all i64 days). + +use std::time::{SystemTime, UNIX_EPOCH}; + +/// Current UTC time as an RFC 3339 string. Falls back to the epoch if the +/// system clock is set before 1970 (it never is in practice). +pub fn now_rfc3339() -> String { + let secs = SystemTime::now() + .duration_since(UNIX_EPOCH) + .map(|d| d.as_secs() as i64) + .unwrap_or(0); + rfc3339_from_unix(secs) +} + +/// Format a Unix timestamp (seconds since 1970-01-01T00:00:00Z) as RFC 3339. +pub fn rfc3339_from_unix(secs: i64) -> String { + let days = secs.div_euclid(86_400); + let rem = secs.rem_euclid(86_400); + let (hh, mm, ss) = (rem / 3600, (rem % 3600) / 60, rem % 60); + let (y, m, d) = civil_from_days(days); + format!("{y:04}-{m:02}-{d:02}T{hh:02}:{mm:02}:{ss:02}Z") +} + +/// Convert days-since-epoch to a `(year, month, day)` civil date. +/// `month` is 1..=12, `day` is 1..=31. +fn civil_from_days(days: i64) -> (i64, u32, u32) { + let z = days + 719_468; + let era = if z >= 0 { z } else { z - 146_096 } / 146_097; + let doe = z - era * 146_097; // [0, 146096] + let yoe = (doe - doe / 1460 + doe / 36_524 - doe / 146_096) / 365; // [0, 399] + let y = yoe + era * 400; + let doy = doe - (365 * yoe + yoe / 4 - yoe / 100); // [0, 365] + let mp = (5 * doy + 2) / 153; // [0, 11] + let d = (doy - (153 * mp + 2) / 5 + 1) as u32; // [1, 31] + let m = (if mp < 10 { mp + 3 } else { mp - 9 }) as u32; // [1, 12] + (if m <= 2 { y + 1 } else { y }, m, d) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn epoch_is_unix_zero() { + assert_eq!(rfc3339_from_unix(0), "1970-01-01T00:00:00Z"); + } + + #[test] + fn known_timestamp_round_trips() { + // 1_700_000_000 = 2023-11-14T22:13:20Z (a well-known reference point). + assert_eq!(rfc3339_from_unix(1_700_000_000), "2023-11-14T22:13:20Z"); + } + + #[test] + fn leap_day_2024() { + // 2024-02-29T00:00:00Z = 1_709_164_800. + assert_eq!(rfc3339_from_unix(1_709_164_800), "2024-02-29T00:00:00Z"); + } + + #[test] + fn now_has_expected_shape() { + let s = now_rfc3339(); + assert_eq!(s.len(), 20, "RFC3339 Z form is 20 chars: {s}"); + assert!(s.ends_with('Z')); + } +} diff --git a/src/workspace.rs b/src/workspace.rs index bb3534d..0785306 100644 --- a/src/workspace.rs +++ b/src/workspace.rs @@ -1,3 +1,4 @@ +use crate::event::{self, Event, EventKind}; use anyhow::{Context, Result}; use serde::{Deserialize, Serialize}; use std::fs; @@ -83,4 +84,59 @@ impl Workspace { } Ok(out) } + + /// Which state currently holds `file_name` (a basename), if any. + pub fn state_of(&self, file_name: &str) -> Option { + [State::Inbox, State::Working, State::Proven, State::Rejected] + .into_iter() + .find(|&state| self.state_dir(state).join(file_name).is_file()) + } + + /// Move `file_name` from `from` to `to`, appending the transition to the + /// event log. Rejects transitions not in the spec's state machine, and + /// fails if the file is not actually in `from`. Returns the new path. + pub fn transition( + &self, + file_name: &str, + from: State, + to: State, + note: Option, + ) -> Result { + let Some(kind) = transition_kind(from, to) else { + anyhow::bail!( + "disallowed transition {} -> {}", + from.dir_name(), + to.dir_name() + ); + }; + let src = self.state_dir(from).join(file_name); + if !src.is_file() { + anyhow::bail!("`{}` is not in `{}`", file_name, from.dir_name()); + } + let dst = self.state_dir(to).join(file_name); + fs::rename(&src, &dst) + .with_context(|| format!("moving {} -> {}", src.display(), dst.display()))?; + + let ev = Event::new(kind, file_name) + .with_from(from) + .with_to(to) + .with_note(note); + event::append(&self.root, &ev) + .with_context(|| format!("logging {:?} for {}", kind, file_name))?; + Ok(dst) + } +} + +/// The event kind for a transition, or `None` if the pair is not a legal +/// move in the spec's state machine. +pub fn transition_kind(from: State, to: State) -> Option { + use State::*; + match (from, to) { + (Inbox, Working) => Some(EventKind::Claim), + (Working, Proven) => Some(EventKind::Promote), + (Working, Rejected) => Some(EventKind::Reject), + (Rejected, Inbox) => Some(EventKind::Requeue), + (Proven, Inbox) => Some(EventKind::Invalidate), + _ => None, + } } diff --git a/tests/dag.rs b/tests/dag.rs new file mode 100644 index 0000000..f46205e --- /dev/null +++ b/tests/dag.rs @@ -0,0 +1,67 @@ +//! `dag` document construction over the fixtures. + +use arghda_core::{build_dag, default_rules}; +use std::path::PathBuf; + +fn fixture(name: &str) -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push(name); + p +} + +#[test] +fn dag_over_orphan_fixture_has_expected_shape() { + let root = fixture("orphan"); + let roots = [root.join("All.agda")]; + let doc = build_dag(&root, &roots, &default_rules()).unwrap(); + + // Nodes are deterministic and sorted by module id. + let ids: Vec<&str> = doc.nodes.iter().map(|n| n.id.as_str()).collect(); + assert_eq!(ids, vec!["All", "Orphan", "Used"]); + + // The real import edge is present; nothing imports the orphan. + assert!(doc + .edges + .iter() + .any(|e| e.from == "All" && e.to == "Used" && e.kind == "imports")); + assert!(!doc.edges.iter().any(|e| e.to == "Orphan")); + + // Orphan is blocked by the orphan-module rule; others are clean. + let orphan = doc.nodes.iter().find(|n| n.id == "Orphan").unwrap(); + assert_eq!(orphan.status, "blocked"); + assert!(orphan + .lint + .hard_block + .contains(&"orphan-module".to_string())); + assert_eq!(orphan.file, PathBuf::from("Orphan.agda")); + assert_eq!( + doc.nodes.iter().find(|n| n.id == "Used").unwrap().status, + "clean" + ); + assert_eq!( + doc.nodes.iter().find(|n| n.id == "All").unwrap().status, + "clean" + ); + + // The blocked list names the orphan. + assert!(doc.blocked.iter().any(|b| b.node == "Orphan")); +} + +#[test] +fn dag_over_wellformed_fixture_is_all_clean() { + let root = fixture("wellformed"); + let roots = [root.join("All.agda")]; + let doc = build_dag(&root, &roots, &default_rules()).unwrap(); + + assert_eq!(doc.version, "0.1"); + assert!( + doc.nodes.iter().all(|n| n.status == "clean"), + "all nodes clean; got: {:?}", + doc.nodes + ); + assert!(doc.blocked.is_empty()); + assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Good")); + assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Util")); +} diff --git a/tests/smoke.rs b/tests/smoke.rs index 0ac667f..eab65a4 100644 --- a/tests/smoke.rs +++ b/tests/smoke.rs @@ -32,10 +32,11 @@ fn collect_hard_blocks(include_root: &Path) -> Vec<(String, String)> { include_root.display() ); + let roots = [entry]; let rules = default_rules(); let ctx = LintContext { include_root, - entry_module: &entry, + entry_modules: &roots, }; let mut hits = Vec::new(); diff --git a/tests/transitions.rs b/tests/transitions.rs new file mode 100644 index 0000000..ded4257 --- /dev/null +++ b/tests/transitions.rs @@ -0,0 +1,78 @@ +//! Workspace state-machine transitions and the event log. + +use arghda_core::{event, EventKind, State, Workspace}; +use std::fs; + +#[test] +fn full_lifecycle_moves_file_and_logs_events() { + let tmp = tempfile::tempdir().unwrap(); + let root = tmp.path(); + let ws = Workspace::init(root).unwrap(); + + fs::write( + ws.state_dir(State::Inbox).join("Foo.agda"), + "module Foo where\n", + ) + .unwrap(); + assert_eq!(ws.state_of("Foo.agda"), Some(State::Inbox)); + + ws.transition("Foo.agda", State::Inbox, State::Working, None) + .unwrap(); + assert_eq!(ws.state_of("Foo.agda"), Some(State::Working)); + + ws.transition( + "Foo.agda", + State::Working, + State::Proven, + Some("typecheck clean".into()), + ) + .unwrap(); + assert_eq!(ws.state_of("Foo.agda"), Some(State::Proven)); + + let events = event::read_all(root).unwrap(); + assert_eq!(events.len(), 2, "two transitions logged"); + assert_eq!(events[0].kind, EventKind::Claim); + assert_eq!(events[0].from, Some(State::Inbox)); + assert_eq!(events[0].to, Some(State::Working)); + assert_eq!(events[1].kind, EventKind::Promote); + assert_eq!(events[1].note.as_deref(), Some("typecheck clean")); + // Timestamps are RFC3339 Z-form. + assert!(events[0].ts.ends_with('Z') && events[0].ts.len() == 20); +} + +#[test] +fn disallowed_transition_is_rejected_and_leaves_no_trace() { + let tmp = tempfile::tempdir().unwrap(); + let ws = Workspace::init(tmp.path()).unwrap(); + fs::write(ws.state_dir(State::Inbox).join("Bar.agda"), "x").unwrap(); + + // inbox -> proven is not a legal move. + assert!(ws + .transition("Bar.agda", State::Inbox, State::Proven, None) + .is_err()); + + // File stays put; nothing is logged. + assert_eq!(ws.state_of("Bar.agda"), Some(State::Inbox)); + assert!(event::read_all(tmp.path()).unwrap().is_empty()); +} + +#[test] +fn transition_of_absent_file_errors() { + let tmp = tempfile::tempdir().unwrap(); + let ws = Workspace::init(tmp.path()).unwrap(); + assert!(ws + .transition("Ghost.agda", State::Inbox, State::Working, None) + .is_err()); +} + +#[test] +fn requeue_round_trips_back_to_inbox() { + let tmp = tempfile::tempdir().unwrap(); + let ws = Workspace::init(tmp.path()).unwrap(); + fs::write(ws.state_dir(State::Rejected).join("Re.agda"), "x").unwrap(); + ws.transition("Re.agda", State::Rejected, State::Inbox, None) + .unwrap(); + assert_eq!(ws.state_of("Re.agda"), Some(State::Inbox)); + let events = event::read_all(tmp.path()).unwrap(); + assert_eq!(events[0].kind, EventKind::Requeue); +}