diff --git a/CHANGELOG.md b/CHANGELOG.md index 9421d1e..8fbd2d2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,11 @@ All notable changes to arghda-core are documented here. The format follows 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`. +- `.arghda/config.toml` operator configuration (the spec's open-question + surface): `scan` / `dag` read a `[lint] headline_pattern` override from + `/.arghda/config.toml` (or an explicit `--config `). Precedence + is built-in default < `config.toml` < CLI `--headline-pattern`. Missing file + ⇒ defaults; unknown keys are rejected so typos surface. - 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 cb3a3ac..1257871 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -78,6 +78,7 @@ dependencies = [ "serde", "serde_json", "tempfile", + "toml", "walkdir", ] @@ -546,6 +547,15 @@ dependencies = [ "zmij", ] +[[package]] +name = "serde_spanned" +version = "0.6.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf41e0cfaf7226dca15e8197172c295a782857fcb97fad1808a166870dee75a3" +dependencies = [ + "serde", +] + [[package]] name = "strsim" version = "0.11.1" @@ -576,6 +586,47 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "toml" +version = "0.8.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc1beb996b9d83529a9e75c17a1686767d148d70663143c7854d8b4a09ced362" +dependencies = [ + "serde", + "serde_spanned", + "toml_datetime", + "toml_edit", +] + +[[package]] +name = "toml_datetime" +version = "0.6.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "22cddaf88f4fbc13c51aebbf5f8eceb5c7c5a9da2ac40a13519eb5b0a0e8f11c" +dependencies = [ + "serde", +] + +[[package]] +name = "toml_edit" +version = "0.22.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a" +dependencies = [ + "indexmap", + "serde", + "serde_spanned", + "toml_datetime", + "toml_write", + "winnow", +] + +[[package]] +name = "toml_write" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801" + [[package]] name = "unicode-ident" version = "1.0.24" @@ -752,6 +803,15 @@ version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" +[[package]] +name = "winnow" +version = "0.7.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df79d97927682d2fd8adb29682d1140b343be4ac0f08fd68b7765d9c059d3945" +dependencies = [ + "memchr", +] + [[package]] name = "wit-bindgen" version = "0.51.0" diff --git a/Cargo.toml b/Cargo.toml index bf6c878..455e3b2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,6 +17,7 @@ notify = "6" regex = "1" serde = { version = "1", features = ["derive"] } serde_json = "1" +toml = "0.8" walkdir = "2" [dev-dependencies] diff --git a/README.md b/README.md index 2524928..583f79b 100644 --- a/README.md +++ b/README.md @@ -26,10 +26,11 @@ record. - `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`) + pattern is operator-configurable (via `.arghda/config.toml` or + `--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`) - `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 @@ -56,10 +57,18 @@ 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). +Configuration: `scan` and `dag` read `.arghda/config.toml` (from +`/.arghda/config.toml`, or an explicit `--config `). Precedence is +built-in default < `config.toml` < CLI flag. Current schema: + +```toml +[lint] +headline_pattern = "^[a-z][A-Za-z0-9-]*$" +``` + 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 +still unpopulated); the Groove service manifest. (`missing-without-k` is subsumed by `missing-safe-pragma`, which already reports a missing `--without-K`.) diff --git a/src/config.rs b/src/config.rs new file mode 100644 index 0000000..372f684 --- /dev/null +++ b/src/config.rs @@ -0,0 +1,122 @@ +//! Operator configuration from `.arghda/config.toml`. +//! +//! The spec makes the `unpinned-headline` pattern operator-overridable +//! per-workspace (`docs/arghda-spec.adoc` §Open questions). This module loads +//! that override (and any future knobs) from a source tree's or workspace's +//! `.arghda/config.toml`: +//! +//! ```toml +//! [lint] +//! headline_pattern = "^[a-z][A-Za-z0-9-]*$" +//! ``` +//! +//! Precedence (low → high): built-in [`RuleConfig::default`] < `config.toml` +//! < CLI flag (e.g. `--headline-pattern`). A missing file is not an error — +//! defaults apply. Unknown keys are rejected so a typo surfaces rather than +//! being silently ignored. + +use crate::lint::RuleConfig; +use anyhow::{Context, Result}; +use serde::Deserialize; +use std::path::Path; + +/// Conventional config location, relative to a source tree or workspace root. +pub const CONFIG_REL_PATH: &str = ".arghda/config.toml"; + +/// The on-disk `.arghda/config.toml` shape. Mirror of the knobs in +/// [`RuleConfig`], all optional so a partial file overlays defaults. +#[derive(Debug, Default, Deserialize)] +#[serde(deny_unknown_fields)] +struct ConfigFile { + #[serde(default)] + lint: LintTable, +} + +#[derive(Debug, Default, Deserialize)] +#[serde(deny_unknown_fields)] +struct LintTable { + /// Override for the `unpinned-headline` detection regex. + headline_pattern: Option, +} + +/// Parse config TOML text into a [`RuleConfig`], overlaying built-in defaults. +fn parse(text: &str) -> Result { + let file: ConfigFile = toml::from_str(text).context("parsing .arghda/config.toml")?; + let mut cfg = RuleConfig::default(); + if let Some(p) = file.lint.headline_pattern { + cfg.headline_pattern = p; + } + Ok(cfg) +} + +/// Load a config file expected to exist, overlaying defaults. +pub fn load_file(path: &Path) -> Result { + let text = std::fs::read_to_string(path) + .with_context(|| format!("reading config {}", path.display()))?; + parse(&text).with_context(|| format!("in config {}", path.display())) +} + +/// Load `/.arghda/config.toml` if it exists, else built-in defaults. +pub fn load_from_dir(base: &Path) -> Result { + let candidate = base.join(CONFIG_REL_PATH); + if candidate.is_file() { + load_file(&candidate) + } else { + Ok(RuleConfig::default()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; + + #[test] + fn lint_table_overrides_headline_pattern() { + let cfg = parse("[lint]\nheadline_pattern = \"^thm-.*$\"\n").unwrap(); + assert_eq!(cfg.headline_pattern, "^thm-.*$"); + } + + #[test] + fn empty_or_partial_file_keeps_defaults() { + assert_eq!( + parse("").unwrap().headline_pattern, + DEFAULT_HEADLINE_PATTERN + ); + assert_eq!( + parse("[lint]\n").unwrap().headline_pattern, + DEFAULT_HEADLINE_PATTERN + ); + } + + #[test] + fn unknown_keys_are_rejected() { + assert!(parse("[lint]\nheadline_patten = \"x\"\n").is_err()); // typo + assert!(parse("[bogus]\nx = 1\n").is_err()); // unknown table + } + + #[test] + fn malformed_toml_errors() { + assert!(parse("[lint").is_err()); + } + + #[test] + fn load_from_dir_without_config_is_default() { + let dir = tempfile::tempdir().unwrap(); + let cfg = load_from_dir(dir.path()).unwrap(); + assert_eq!(cfg.headline_pattern, DEFAULT_HEADLINE_PATTERN); + } + + #[test] + fn load_from_dir_reads_present_config() { + let dir = tempfile::tempdir().unwrap(); + std::fs::create_dir_all(dir.path().join(".arghda")).unwrap(); + std::fs::write( + dir.path().join(CONFIG_REL_PATH), + "[lint]\nheadline_pattern = \"^[A-Z].*$\"\n", + ) + .unwrap(); + let cfg = load_from_dir(dir.path()).unwrap(); + assert_eq!(cfg.headline_pattern, "^[A-Z].*$"); + } +} diff --git a/src/lib.rs b/src/lib.rs index 1fea9d2..48ff1c1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,7 @@ //! and the diagnostic types. The CLI in `main.rs` is a thin consumer. pub mod agda; +pub mod config; pub mod dag; pub mod diagnostic; pub mod event; diff --git a/src/main.rs b/src/main.rs index 234f9c9..f91c29b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -39,6 +39,10 @@ enum Cmd { /// (`unpinned-headline` rule). Defaults to the spec pattern. #[arg(long)] headline_pattern: Option, + /// Path to an `.arghda/config.toml`. Defaults to + /// `/.arghda/config.toml` if present. + #[arg(long)] + config: 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). @@ -71,6 +75,10 @@ enum Cmd { /// (`unpinned-headline` rule). Defaults to the spec pattern. #[arg(long)] headline_pattern: Option, + /// Path to an `.arghda/config.toml`. Defaults to + /// `/.arghda/config.toml` if present. + #[arg(long)] + config: Option, }, /// Claim a file: inbox -> working. Claim { workspace: PathBuf, file: String }, @@ -106,9 +114,17 @@ fn main() -> Result<()> { path, entry, headline_pattern, + config, + unused, + json, + } => scan( + &path, + &entry, + headline_pattern.as_deref(), + config.as_deref(), unused, json, - } => scan(&path, &entry, headline_pattern.as_deref(), unused, json)?, + )?, Cmd::Check { file, include_root, @@ -118,7 +134,13 @@ fn main() -> Result<()> { path, entry, headline_pattern, - } => dag(&path, &entry, headline_pattern.as_deref())?, + config, + } => dag( + &path, + &entry, + headline_pattern.as_deref(), + config.as_deref(), + )?, Cmd::Claim { workspace, file } => { transition(&workspace, &file, State::Inbox, State::Working)? } @@ -148,10 +170,11 @@ fn scan( include_root: &Path, entry: &[PathBuf], headline_pattern: Option<&str>, + config: Option<&Path>, unused: bool, json: bool, ) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern)?; + let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; let ctx = LintContext { include_root, entry_modules: &roots, @@ -295,13 +318,42 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { Ok(()) } -fn dag(include_root: &Path, entry: &[PathBuf], headline_pattern: Option<&str>) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern)?; +fn dag( + include_root: &Path, + entry: &[PathBuf], + headline_pattern: Option<&str>, + config: Option<&Path>, +) -> Result<()> { + let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; let doc = build_dag(include_root, &roots, &rules)?; println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) } +/// Build the lint `RuleConfig` with precedence default < `.arghda/config.toml` +/// < CLI flag. An explicit `--config` that does not exist is an error; the +/// default discovery location (`/.arghda/config.toml`) is +/// silently optional. +fn resolve_config( + include_root: &Path, + config: Option<&Path>, + headline_pattern: Option<&str>, +) -> Result { + let mut cfg = match config { + Some(p) => { + if !p.is_file() { + anyhow::bail!("config file not found: {}", p.display()); + } + arghda_core::config::load_file(p)? + } + None => arghda_core::config::load_from_dir(include_root)?, + }; + if let Some(p) = headline_pattern { + cfg.headline_pattern = p.to_string(); + } + Ok(cfg) +} + /// 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 @@ -311,6 +363,7 @@ fn resolve_roots_and_rules( include_root: &Path, entry: &[PathBuf], headline_pattern: Option<&str>, + config: Option<&Path>, ) -> Result<(Vec, RuleSet)> { for e in entry { if !e.is_file() { @@ -322,10 +375,7 @@ 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 cfg = resolve_config(include_root, config, headline_pattern)?; let rules: RuleSet = if roots.is_empty() { eprintln!( "note: no root modules (All.agda/Smoke.agda) found under {}; skipping orphan-module rule",