feat(config): operator config via .arghda/config.toml

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
+  `<PATH>/.arghda/config.toml` (or an explicit `--config <file>`). 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

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]

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 <regex>`);
-    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 <regex>`); 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
+`<PATH>/.arghda/config.toml`, or an explicit `--config <file>`). 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`.)
 

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<String>,
+}
+
+/// Parse config TOML text into a [`RuleConfig`], overlaying built-in defaults.
+fn parse(text: &str) -> Result<RuleConfig> {
+    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<RuleConfig> {
+    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 `<base>/.arghda/config.toml` if it exists, else built-in defaults.
+pub fn load_from_dir(base: &Path) -> Result<RuleConfig> {
+    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].*$");
+    }
+}

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;