feat(lint): unpinned-headline rule (Smoke-pin coverage)#6
Merged
Conversation
Implements the spec's `unpinned-headline` lint (arghda-spec.adoc §Linter rules): 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. - Warn severity (per spec): not every matching definition is a headline the operator wants pinned, and the default pattern is intentionally broad. - Headline detection keys on top-level (column-0) type signatures `name : T` (and `a b c : T`), which yields 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. 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, so `LintContext` and the other rules' tests are untouched. Persisting it in `.arghda/config.toml` remains a follow-up. Adds the `regex` dependency. 12 unit tests; dogfooded against the echo-types corpus (fires as a non-blocking warn, pins read correctly). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
hyperpolymath
added a commit
that referenced
this pull request
Jun 20, 2026
## Summary Persists the operator-configurable headline pattern (and any future lint knobs) in `.arghda/config.toml` — the per-workspace surface the spec's open question calls for (`docs/arghda-spec.adoc` lines 200–202). Until now the pattern was only a CLI flag. ## Design - **`src/config.rs`** — a serde/`toml` schema deserialised from `.arghda/config.toml`, overlaid on `RuleConfig::default()`: ```toml [lint] headline_pattern = "^[a-z][A-Za-z0-9-]*$" ``` `deny_unknown_fields` so a typo (`headline_patten`) **errors** rather than being silently ignored; a missing file yields defaults. - **`scan` / `dag`** gain `--config <file>`; discovery defaults to `<PATH>/.arghda/config.toml`. - **Precedence (low → high):** built-in default < `config.toml` < CLI `--headline-pattern`. An explicit `--config` pointing at a missing file is an error; the default-location lookup is silently optional. - Reuses the existing `RuleConfig` / `rules_with_config` (from #6) — **no change to the rule itself**, just where its pattern comes from. ## Verification - `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo build`, `cargo test` all green (lib suite 41 → 47; 6 new config unit tests: parse / precedence / unknown-key-rejection / malformed-TOML / discovery). - **Live end-to-end:** empty config → default pattern flags all headlines; `[lint] headline_pattern = "^thm-.*$"` narrows to just `thm-key`; `--headline-pattern '^foo-.*$'` overrides the config file; `--config <missing>` errors cleanly. Adds the `toml` dependency. Second of three sequenced engine-polish PRs (3 → 2 → 1): `unused-import` (#7, merged), **`.arghda/config.toml`** (this), then the DAG `headlines` field. 🤖 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)_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Implements the spec's
unpinned-headlinelint (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.agdavia ausing ( … )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
missing-safe-pragma/orphan-module/unjustified-postulateare 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.name : T(and the multi-namea b c : Tform). Column-0-only gives the export-only filter for free, sinceprivate-block definitions are indented.using ( … )list across theSmoke.agdafiles among the entry modules; tolerant of multi-lineusinglists.Smoke.agdais in scope (e.g. a single-filecheck), and never lints aSmoke.agdafor its own headlines.--headline-pattern <regex>onscan/dag; default^[a-z][A-Za-z0-9-]*$per the spec open question. The pattern lives on the rule instance (UnpinnedHeadline { matcher }), soLintContextand every other rule's test constructor are untouched.Changes
src/lint/unpinned_headline.rs(+ 12 unit tests).RuleConfig/rules_with_configinsrc/lint/mod.rs;default_rules()unchanged in behaviour.--headline-patternflag threaded throughscan/dag.regexdependency.unpinned-headlineremoved from "Not yet".Verification
cargo fmt --check,cargo clippy --all-targets -- -D warnings,cargo build,cargo testall green (lib suite 23 → 35).warn(432 hits under the broad default), pins read correctly fromSmoke.agda+Ordinal/Buchholz/Smoke.agda.Follow-ups (noted in README)
.arghda/config.toml(currently a CLI flag; config-discovery needs a small design decision sincescan/dagaren't workspace-scoped).headlinesarray (the extractor now exists).🤖 Generated with Claude Code
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
Generated by Claude Code