diff --git a/CHANGELOG.md b/CHANGELOG.md index c63d409..df7dab1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,6 +24,13 @@ All notable changes to arghda-core are documented here. The format follows - Lint rules: `unjustified-postulate` (hard-block), `escape-hatch` (warn: `TERMINATING`-family pragmas + `believe_me` / `primTrustMe`), `tab-mix` (warn). +- `unpinned-headline` (warn): flags a top-level theorem whose name matches + the headline pattern but is not pinned in any `Smoke.agda` via a + `using ( … )` clause. The pattern is operator-configurable via + `--headline-pattern ` on `scan` / `dag` (default + `^[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. - 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/Cargo.lock b/Cargo.lock index 3957216..cb3a3ac 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,15 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "aho-corasick" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" +dependencies = [ + "memchr", +] + [[package]] name = "anstream" version = "1.0.0" @@ -65,6 +74,7 @@ dependencies = [ "anyhow", "clap", "notify", + "regex", "serde", "serde_json", "tempfile", @@ -436,6 +446,35 @@ dependencies = [ "bitflags 2.11.1", ] +[[package]] +name = "regex" +version = "1.12.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1292b7759ae1cb9ec195452d1390a074f0cd8541ab7a5a8c31cd6db45d4a6ba" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" + [[package]] name = "rustix" version = "1.1.4" diff --git a/Cargo.toml b/Cargo.toml index 9567821..bf6c878 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,7 @@ path = "src/main.rs" anyhow = "1" clap = { version = "4", features = ["derive"] } notify = "6" +regex = "1" serde = { version = "1", features = ["derive"] } serde_json = "1" walkdir = "2" diff --git a/README.md b/README.md index 374ba2e..052275a 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,13 @@ record. `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and trust primitives (`believe_me`/`primTrustMe`) - `tab-mix` (warn) — a tab in leading whitespace + - `unpinned-headline` (warn) — a top-level theorem whose name matches the + headline pattern is not pinned in any `Smoke.agda` via a `using ( … )` + clause (the estate "every headline pinned in Smoke" discipline). The + pattern is operator-configurable (`--headline-pattern `); + 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`) - Workspace state machine — transitions are file moves, each logged to `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`, `invalidate`) @@ -44,11 +51,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: `unpinned-headline` (needs `Smoke.agda` parsing + a configurable -regex) and `unused-import` (shells out to `agda-unused`); content-hash -invalidation of `proven`; the Groove service manifest; and the -`.machine_readable/` RSR retrofit. (`missing-without-k` is subsumed by -`missing-safe-pragma`, which already reports a missing `--without-K`.) +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`.) ## Build diff --git a/src/lib.rs b/src/lib.rs index 29dac5a..f1b0fc2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -20,5 +20,5 @@ 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 lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; pub use workspace::{StaleEntry, State, Workspace}; diff --git a/src/lint/mod.rs b/src/lint/mod.rs index c3f31c1..649d2b9 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -7,6 +7,7 @@ pub mod orphan_module; pub mod postulate; pub mod safe_pragma; pub mod tab_mix; +pub mod unpinned_headline; /// Context handed to every rule. #[derive(Clone, Debug)] @@ -25,14 +26,42 @@ pub trait LintRule: Send + Sync { fn run(&self, file: &Path, ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()>; } -pub fn default_rules() -> Vec> { - vec![ +/// Operator-configurable lint settings (the `.arghda/config.toml` surface +/// the spec calls for; currently set via the CLI `--headline-pattern` flag). +#[derive(Clone, Debug)] +pub struct RuleConfig { + /// Regex a top-level definition name must match to be treated as a + /// pinnable headline by the `unpinned-headline` rule. + pub headline_pattern: String, +} + +impl Default for RuleConfig { + fn default() -> Self { + Self { + headline_pattern: unpinned_headline::DEFAULT_HEADLINE_PATTERN.to_string(), + } + } +} + +/// The standard lint pack, parameterised by operator config. Fails only if a +/// supplied pattern (e.g. `headline_pattern`) is not a valid regex. +pub fn rules_with_config(cfg: &RuleConfig) -> Result>> { + Ok(vec![ Box::new(safe_pragma::SafePragma), Box::new(orphan_module::OrphanModule), Box::new(postulate::UnjustifiedPostulate), Box::new(escape_hatch::EscapeHatch), Box::new(tab_mix::TabMix), - ] + Box::new(unpinned_headline::UnpinnedHeadline::new( + &cfg.headline_pattern, + )?), + ]) +} + +/// The standard lint pack with default config. The default pattern is a +/// known-good literal, so this is infallible. +pub fn default_rules() -> Vec> { + rules_with_config(&RuleConfig::default()).expect("default rule config is valid") } pub fn run_lints( diff --git a/src/lint/unpinned_headline.rs b/src/lint/unpinned_headline.rs new file mode 100644 index 0000000..94713c2 --- /dev/null +++ b/src/lint/unpinned_headline.rs @@ -0,0 +1,420 @@ +//! `unpinned-headline` (warn) — a module declares a top-level theorem whose +//! name matches the headline pattern, but the name is not pinned in any +//! `Smoke.agda` via a `using ( … )` clause. +//! +//! The estate discipline (echo-types' CLAUDE.md "Working rules": *every +//! headline theorem must be pinned in `Smoke.agda` via a `using` clause*) +//! is what keeps a `--safe` suite honest — a renamed or silently-dropped +//! headline surfaces as a broken pin rather than a quiet regression. This +//! rule makes the *missing* pin visible. It is a `warn`, not a hard-block: +//! not every top-level definition matching the pattern is a headline the +//! operator wants pinned, and the pattern is operator-configurable. +//! +//! Headline detection: top-level (column-0) type signatures `name : T` +//! (or `a b c : T`, which declares each of `a`, `b`, `c`) whose name +//! matches the configured regex. The column-0-only rule gives the +//! "export-only" filter for free — `private`-block definitions are indented +//! and so are never considered. +//! +//! Pins: the union of every `using ( … )` list across the `Smoke.agda` +//! files among the workspace's entry modules. If no `Smoke.agda` is in +//! scope (e.g. a single-file `check`), the rule self-skips rather than +//! flagging every headline. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use regex::Regex; +use std::collections::BTreeSet; +use std::fs; +use std::path::Path; + +/// Spec default (`docs/arghda-spec.adoc` §Open questions): a lowercase-initial +/// ASCII identifier, hyphens allowed, fully anchored. +pub const DEFAULT_HEADLINE_PATTERN: &str = r"^[a-z][A-Za-z0-9-]*$"; + +/// Reserved openers that begin a top-level form but never declare a +/// pinnable headline name (so a `record … : Set where` line is not read +/// as a theorem signature). +const NON_DECL_KEYWORDS: &[&str] = &[ + "module", + "open", + "import", + "private", + "record", + "data", + "postulate", + "infix", + "infixl", + "infixr", + "mutual", + "abstract", + "instance", + "field", + "syntax", + "pattern", + "variable", + "primitive", + "where", + "renaming", + "using", + "hiding", + "constructor", + "interleaved", + "unquoteDecl", + "unquoteDef", + "macro", + "tactic", +]; + +pub struct UnpinnedHeadline { + matcher: Regex, +} + +impl UnpinnedHeadline { + /// Build the rule with an operator-supplied headline pattern. Returns an + /// error if the pattern is not a valid regex. + pub fn new(pattern: &str) -> Result { + let matcher = Regex::new(pattern) + .with_context(|| format!("compiling headline pattern `{pattern}`"))?; + Ok(Self { matcher }) + } +} + +impl Default for UnpinnedHeadline { + fn default() -> Self { + Self::new(DEFAULT_HEADLINE_PATTERN).expect("default headline pattern is a valid regex") + } +} + +impl LintRule for UnpinnedHeadline { + fn name(&self) -> &'static str { + "unpinned-headline" + } + + fn run(&self, file: &Path, ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + // The Smoke files are the pin registry, not theorem modules; never + // lint them for their own headlines. + if is_smoke(file) { + return Ok(()); + } + + // Union the pin set across every Smoke.agda among the entry modules. + let mut pinned: BTreeSet = BTreeSet::new(); + let mut any_smoke = false; + for entry in ctx.entry_modules { + if !is_smoke(entry) { + continue; + } + any_smoke = true; + let contents = fs::read_to_string(entry) + .with_context(|| format!("reading Smoke file {}", entry.display()))?; + collect_pinned(&contents, &mut pinned); + } + if !any_smoke { + // Nothing pins anything in scope; can't judge pinning. + return Ok(()); + } + + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + + let mut reported: BTreeSet = BTreeSet::new(); + for (name, line) in headline_decls(&contents, &self.matcher) { + if pinned.contains(&name) || !reported.insert(name.clone()) { + continue; + } + report.push(Diagnostic { + rule: self.name().to_string(), + severity: Severity::Warn, + file: file.to_path_buf(), + message: format!( + "headline `{name}` is not pinned in any Smoke.agda via a `using` clause" + ), + line: Some(line), + }); + } + Ok(()) + } +} + +fn is_smoke(path: &Path) -> bool { + path.file_name().and_then(|s| s.to_str()) == Some("Smoke.agda") +} + +/// Strip an Agda line comment for token analysis: a whole-line `--` comment +/// becomes empty; an inline ` --` comment is cut. Mirrors the convention the +/// `escape-hatch` rule uses. +fn strip_comment(line: &str) -> &str { + if line.trim_start().starts_with("--") { + return ""; + } + line.split(" --").next().unwrap_or(line) +} + +fn is_ident_char(c: char) -> bool { + c.is_alphanumeric() || c == '_' || c == '-' || c == '\'' +} + +/// Collect the names appearing in `using ( … )` clauses of `contents` into +/// `out`. Tolerant of multi-line `using` lists; entries are `;`-separated. +fn collect_pinned(contents: &str, out: &mut BTreeSet) { + // Strip comments first so a `-- … using (…)` header does not register. + let cleaned: String = contents + .lines() + .map(strip_comment) + .collect::>() + .join("\n"); + + let mut i = 0usize; + while let Some(rel) = cleaned[i..].find("using") { + let start = i + rel; + let end = start + "using".len(); + i = end; + + // Left word boundary: the char before `using` must not be part of a + // longer identifier (so `reusing` does not match). + let left_ok = start == 0 || !is_ident_char(cleaned[..start].chars().next_back().unwrap()); + if !left_ok { + continue; + } + + // Skip whitespace, then require `(`. (This also enforces the right + // word boundary: `usingFoo` has no `(` after `using`.) + let rest = &cleaned[end..]; + let mut off = 0usize; + for c in rest.chars() { + if c.is_whitespace() { + off += c.len_utf8(); + } else { + break; + } + } + if !rest[off..].starts_with('(') { + continue; + } + + let inner_start = off + 1; + let Some(close_rel) = rest[inner_start..].find(')') else { + continue; + }; + let inner = &rest[inner_start..inner_start + close_rel]; + for entry in inner.split(';') { + let n = entry.trim(); + if !n.is_empty() { + out.insert(n.to_string()); + } + } + i = end + inner_start + close_rel + 1; + } +} + +/// Top-level (column-0) type-signature names matching `matcher`, paired with +/// the 1-based line they were declared on. `a b c : T` yields each name. +fn headline_decls(contents: &str, matcher: &Regex) -> Vec<(String, usize)> { + let mut out = Vec::new(); + let mut in_block_comment = false; + + for (idx, raw) in contents.lines().enumerate() { + if in_block_comment { + if raw.contains("-}") { + in_block_comment = false; + } + continue; + } + // Only column-0 lines are top-level (export-only filter): an indented + // line is inside a module / record / private block. + if raw.is_empty() || raw.starts_with(char::is_whitespace) { + continue; + } + // Whole-line comment. + if raw.starts_with("--") { + continue; + } + // Pragma (`{-# … #-}`) or block-comment opener (`{- …`). Handled + // before comment-stripping so an OPTIONS pragma carrying `--safe` + // is never mistaken for a `--` comment. + if raw.starts_with("{-") { + if !raw.contains("-}") { + in_block_comment = true; + } + continue; + } + + let line = strip_comment(raw); + let tokens: Vec<&str> = line.split_whitespace().collect(); + // Need the `name … :` shape: a standalone `:` token after ≥1 name. + let Some(colon) = tokens.iter().position(|&t| t == ":") else { + continue; + }; + if colon == 0 || NON_DECL_KEYWORDS.contains(&tokens[0]) { + continue; + } + for name in &tokens[..colon] { + if matcher.is_match(name) { + out.push(((*name).to_string(), idx + 1)); + } + } + } + out +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + use std::path::PathBuf; + + /// Lint `module` (written as `Foo.agda`) for unpinned headlines, with an + /// optional sibling `Smoke.agda` registered as the sole entry module. + fn run_rule(module: &str, smoke: Option<&str>, pattern: &str) -> LintReport { + let dir = tempfile::tempdir().unwrap(); + let modpath = dir.path().join("Foo.agda"); + std::fs::write(&modpath, module).unwrap(); + let mut roots: Vec = Vec::new(); + if let Some(s) = smoke { + let sp = dir.path().join("Smoke.agda"); + std::fs::write(&sp, s).unwrap(); + roots.push(sp); + } + let ctx = LintContext { + include_root: dir.path(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(UnpinnedHeadline::new(pattern).unwrap())]; + run_lints(&modpath, &ctx, &rules).unwrap() + } + + #[test] + fn unpinned_headline_is_warned() { + let r = run_rule( + "module Foo where\nfoo-bar : Set\nfoo-bar = Set\n", + Some("module Smoke where\nopen import Bar using ( something-else )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(!r.has_hard_block()); + assert_eq!(r.warns().count(), 1, "got: {:?}", r.diagnostics); + assert!(r.diagnostics[0].message.contains("foo-bar")); + assert_eq!(r.diagnostics[0].line, Some(2)); + } + + #[test] + fn pinned_headline_is_clean() { + let r = run_rule( + "module Foo where\nfoo-bar : Set\nfoo-bar = Set\n", + Some("module Smoke where\nopen import Foo using ( foo-bar )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn multi_name_signature_flags_only_unpinned() { + let r = run_rule( + "module Foo where\nlemma-a lemma-b : Set\n", + Some("module Smoke where\nopen import Foo using ( lemma-a )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert_eq!(r.warns().count(), 1, "got: {:?}", r.diagnostics); + assert!(r.diagnostics[0].message.contains("lemma-b")); + } + + #[test] + fn private_indented_decl_is_not_a_headline() { + // `helper-fn` is indented under `private` → not column-0 → ignored. + let r = run_rule( + "module Foo where\nprivate\n helper-fn : Set\n", + Some("module Smoke where\nopen import Bar using ( x )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn uppercase_name_is_not_matched_by_default_pattern() { + let r = run_rule( + "module Foo where\nC-monotone : Set\n", + Some("module Smoke where\nopen import Bar using ( x )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn custom_pattern_can_match_uppercase() { + let r = run_rule( + "module Foo where\nC-monotone : Set\n", + Some("module Smoke where\nopen import Bar using ( x )\n"), + r"^[A-Za-z][A-Za-z0-9-]*$", + ); + assert_eq!(r.warns().count(), 1, "got: {:?}", r.diagnostics); + assert!(r.diagnostics[0].message.contains("C-monotone")); + } + + #[test] + fn no_smoke_in_scope_skips() { + let r = run_rule( + "module Foo where\nfoo-bar : Set\n", + None, + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn multiline_using_list_pins() { + let r = run_rule( + "module Foo where\nfoo-bar : Set\nbaz-qux : Set\n", + Some("module Smoke where\nopen import Foo using\n ( foo-bar\n ; baz-qux\n )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn options_pragma_is_not_read_as_a_decl() { + // The `--safe` in the pragma must not derail signature detection on + // the following line. + let r = run_rule( + "{-# OPTIONS --safe --without-K #-}\nmodule Foo where\nfoo-bar : Set\n", + Some("module Smoke where\nopen import Foo using ( foo-bar )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn smoke_file_itself_is_skipped() { + // A file *named* Smoke.agda is never linted for headlines, even if it + // carries a signature. + let dir = tempfile::tempdir().unwrap(); + let smoke = dir.path().join("Smoke.agda"); + std::fs::write(&smoke, "module Smoke where\nlocal-lemma : Set\n").unwrap(); + let roots = [smoke.clone()]; + let ctx = LintContext { + include_root: dir.path(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new( + UnpinnedHeadline::new(DEFAULT_HEADLINE_PATTERN).unwrap(), + )]; + let r = run_lints(&smoke, &ctx, &rules).unwrap(); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } + + #[test] + fn invalid_pattern_is_an_error() { + assert!(UnpinnedHeadline::new("[").is_err()); + } + + #[test] + fn record_signature_is_not_a_headline() { + // `record Foo : Set where` has a `:` but opens a record, not a theorem. + let r = run_rule( + "module Foo where\nrecord Wrap : Set where\n", + Some("module Smoke where\nopen import Bar using ( x )\n"), + DEFAULT_HEADLINE_PATTERN, + ); + assert!(r.diagnostics.is_empty(), "got: {:?}", r.diagnostics); + } +} diff --git a/src/main.rs b/src/main.rs index 6b9d7fd..91b63a7 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,8 +1,8 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ - build_dag, check_file, default_rules, event, graph, run_lints, watcher, LintRule, State, - Workspace, + build_dag, check_file, default_rules, event, graph, rules_with_config, run_lints, watcher, + LintRule, RuleConfig, State, Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -35,6 +35,10 @@ enum Cmd { /// `All.agda`/`Smoke.agda` discovered under PATH. #[arg(long)] entry: Vec, + /// Regex a name must match to count as a pinnable headline + /// (`unpinned-headline` rule). Defaults to the spec pattern. + #[arg(long)] + headline_pattern: Option, /// Emit the report as JSON instead of human-readable text. #[arg(long)] json: bool, @@ -58,6 +62,10 @@ enum Cmd { /// `All.agda`/`Smoke.agda` discovered under PATH. #[arg(long)] entry: Vec, + /// Regex a name must match to count as a pinnable headline + /// (`unpinned-headline` rule). Defaults to the spec pattern. + #[arg(long)] + headline_pattern: Option, }, /// Claim a file: inbox -> working. Claim { workspace: PathBuf, file: String }, @@ -89,13 +97,22 @@ fn main() -> Result<()> { let ws = Workspace::init(&path)?; println!("initialised workspace at {}", ws.root().display()); } - Cmd::Scan { path, entry, json } => scan(&path, &entry, json)?, + Cmd::Scan { + path, + entry, + headline_pattern, + json, + } => scan(&path, &entry, headline_pattern.as_deref(), json)?, Cmd::Check { file, include_root, json, } => check(&file, include_root.as_deref(), json)?, - Cmd::Dag { path, entry } => dag(&path, &entry)?, + Cmd::Dag { + path, + entry, + headline_pattern, + } => dag(&path, &entry, headline_pattern.as_deref())?, Cmd::Claim { workspace, file } => { transition(&workspace, &file, State::Inbox, State::Working)? } @@ -121,8 +138,13 @@ fn main() -> Result<()> { Ok(()) } -fn scan(include_root: &Path, entry: &[PathBuf], json: bool) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry)?; +fn scan( + include_root: &Path, + entry: &[PathBuf], + headline_pattern: Option<&str>, + json: bool, +) -> Result<()> { + let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern)?; let ctx = LintContext { include_root, entry_modules: &roots, @@ -241,8 +263,8 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { Ok(()) } -fn dag(include_root: &Path, entry: &[PathBuf]) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry)?; +fn dag(include_root: &Path, entry: &[PathBuf], headline_pattern: Option<&str>) -> Result<()> { + let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern)?; let doc = build_dag(include_root, &roots, &rules)?; println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) @@ -256,6 +278,7 @@ fn dag(include_root: &Path, entry: &[PathBuf]) -> Result<()> { fn resolve_roots_and_rules( include_root: &Path, entry: &[PathBuf], + headline_pattern: Option<&str>, ) -> Result<(Vec, RuleSet)> { for e in entry { if !e.is_file() { @@ -267,17 +290,21 @@ fn resolve_roots_and_rules( } else { entry.to_vec() }; + let mut cfg = RuleConfig::default(); + if let Some(p) = headline_pattern { + cfg.headline_pattern = p.to_string(); + } 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() + rules_with_config(&cfg)? .into_iter() .filter(|r| r.name() != "orphan-module") .collect() } else { - default_rules() + rules_with_config(&cfg)? }; Ok((roots, rules)) }