feat(lint): unpinned-headline rule (Smoke-pin coverage)

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 <regex>` 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

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"

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 <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`)
 - 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
 

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};

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<Box<dyn LintRule>> {
-    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<Vec<Box<dyn LintRule>>> {
+    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<Box<dyn LintRule>> {
+    rules_with_config(&RuleConfig::default()).expect("default rule config is valid")
 }
 
 pub fn run_lints(