feat(config): operator config via .arghda/config.toml#8
Merged
Conversation
Persists the operator-configurable headline pattern (and any future lint knobs) in `.arghda/config.toml`, the surface the spec's open question calls for — previously it was only a CLI flag. - New `src/config.rs`: a serde/toml `[lint] headline_pattern` schema overlaid on `RuleConfig::default()`. `deny_unknown_fields` so a typo 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` that does not exist is an error; the default location is silently optional. - Reuses the existing `RuleConfig` / `rules_with_config` (from #6); no change to the rule itself. Adds the `toml` dependency. 6 config unit tests (parse/precedence/unknown-key/ malformed/discovery); lib suite 41 → 47. Live-verified end to end: empty config → default pattern flags all headlines; `^thm-` config narrows to one; `--headline-pattern` overrides config; missing `--config` errors cleanly. 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 Completes the v0 DAG schema: each `dag` node now carries the per-node **`headlines`** array the spec defines (`docs/arghda-spec.adoc` lines 128–135) but the builder previously omitted — the sorted, deduped list of top-level headline theorem names the module declares. ## Design - **Reuses the `unpinned-headline` extractor** — no duplicate parsing. `headline_decls` becomes `pub`, and `dag::build` runs it per node with the configured headline `Regex`. - **`build_dag` gains a `headline_pattern: &str` parameter.** `dag` threads the *resolved* pattern through (built-in default < `.arghda/config.toml` < CLI `--headline-pattern`, via the #8 config plumbing), so the DAG honours the same operator configuration as the lint. - Column-0-only extraction means indented `private` helpers are not surfaced (same export-only filter as the rule). ## Verification - `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo build`, `cargo test` all green (7 groups). - New `tests/fixtures/headlines/` + `dag_populates_node_headlines`: asserts `Thm → ["thm-one","thm-two"]`, that the indented `private helper` is excluded, and the import-only `All` entry surfaces `[]`. - **Live:** `arghda dag tests/fixtures/headlines` emits `"headlines": ["thm-one","thm-two"]` on the `Thm` node and `[]` on `All`. Last of three sequenced engine-polish PRs (3 → 2 → 1): `unused-import` (#7), `.arghda/config.toml` (#8), **DAG `headlines`** (this). With these, the v0 Agda lint set and DAG schema in `arghda-spec.adoc` are complete. 🤖 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
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.adoclines 200–202). Until now the pattern was only a CLI flag.Design
src/config.rs— a serde/tomlschema deserialised from.arghda/config.toml, overlaid onRuleConfig::default():deny_unknown_fieldsso a typo (headline_patten) errors rather than being silently ignored; a missing file yields defaults.scan/daggain--config <file>; discovery defaults to<PATH>/.arghda/config.toml.config.toml< CLI--headline-pattern. An explicit--configpointing at a missing file is an error; the default-location lookup is silently optional.RuleConfig/rules_with_config(from feat(lint): unpinned-headline rule (Smoke-pin coverage) #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 testall green (lib suite 41 → 47; 6 new config unit tests: parse / precedence / unknown-key-rejection / malformed-TOML / discovery).[lint] headline_pattern = "^thm-.*$"narrows to justthm-key;--headline-pattern '^foo-.*$'overrides the config file;--config <missing>errors cleanly.Adds the
tomldependency.Second of three sequenced engine-polish PRs (3 → 2 → 1):
unused-import(#7, merged),.arghda/config.toml(this), then the DAGheadlinesfield.🤖 Generated with Claude Code
https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
Generated by Claude Code