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

## Summary

Implements the spec's `unpinned-headline` lint (`docs/arghda-spec.adoc`
§Linter rules) — the last remaining v0 Agda lint that was filed under
README "Not yet".

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**. This enforces the estate *"every headline pinned in
Smoke"* discipline: a renamed or silently-dropped headline surfaces as a
missing pin rather than a quiet regression.

## Design

- **Warn severity** (per spec —
`missing-safe-pragma`/`orphan-module`/`unjustified-postulate` are the
hard-blocks; the rest are warns). Not every matching definition is a
headline the operator wants pinned, and the default pattern is
deliberately broad.
- **Headline detection** keys on top-level (column-0) type signatures
`name : T` (and the multi-name `a b c : T` form). Column-0-only gives
the **export-only filter for free**, since `private`-block definitions
are indented.
- **Pins** are the union of every `using ( … )` list across the
`Smoke.agda` files among the entry modules; tolerant of multi-line
`using` lists.
- **Self-skips** when no `Smoke.agda` is in scope (e.g. a single-file
`check`), and never lints a `Smoke.agda` for its own headlines.
- **Operator-configurable regex** via `--headline-pattern <regex>` on
`scan`/`dag`; default `^[a-z][A-Za-z0-9-]*$` per the spec open question.
The pattern lives on the **rule instance** (`UnpinnedHeadline { matcher
}`), so `LintContext` and every other rule's test constructor are
untouched.

## Changes

- New `src/lint/unpinned_headline.rs` (+ 12 unit tests).
- `RuleConfig` / `rules_with_config` in `src/lint/mod.rs`;
`default_rules()` unchanged in behaviour.
- `--headline-pattern` flag threaded through `scan`/`dag`.
- Adds the `regex` dependency.
- README + CHANGELOG updated; `unpinned-headline` removed from "Not
yet".

## Verification

- `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`,
`cargo build`, `cargo test` all green (lib suite 23 → 35).
- Dogfooded against the echo-types corpus: fires as a non-blocking
`warn` (432 hits under the broad default), pins read correctly from
`Smoke.agda` + `Ordinal/Buchholz/Smoke.agda`.

## Follow-ups (noted in README)

- Persist the headline pattern in `.arghda/config.toml` (currently a CLI
flag; config-discovery needs a small design decision since `scan`/`dag`
aren't workspace-scoped).
- Populate the DAG schema's per-node `headlines` array (the extractor
now exists).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs

---
_Generated by [Claude
Code](https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs)_

Author: hyperpolymath

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.lock

@@ -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"

Cargo.toml

@@ -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
 

README.md

@@ -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/lib.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(