From 73eb38377f6395a88795a00bc5d040311cbccea1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 01:53:57 +0000 Subject: [PATCH] feat(dag): populate per-node headlines field MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the v0 DAG schema (docs/arghda-spec.adoc lines 128-135): each `dag` node now carries the sorted, deduped list of top-level headline theorem names the module declares — previously the schema defined `headlines` but the builder omitted it. - Reuses the `unpinned-headline` extractor: `headline_decls` is now `pub`, and `dag::build` runs it per node with the configured headline pattern. - `build_dag` gains a `headline_pattern: &str` parameter; `dag` threads the resolved pattern through (default < config.toml < CLI), so the DAG honours the same operator configuration as the lint. - New `tests/fixtures/headlines/` and a `dag_populates_node_headlines` test asserting `Thm -> [thm-one, thm-two]` (and that the indented `private` helper and the import-only entry module surface nothing). Live: `arghda dag tests/fixtures/headlines` emits `"headlines": ["thm-one", "thm-two"]` on the Thm node, `[]` on All. fmt/clippy/test green (7 groups). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs --- CHANGELOG.md | 4 ++++ README.md | 12 +++++------- src/dag.rs | 28 ++++++++++++++++++++++++---- src/lint/unpinned_headline.rs | 5 ++++- src/main.rs | 12 +++++++----- tests/dag.rs | 24 ++++++++++++++++++++++-- tests/fixtures/headlines/All.agda | 5 +++++ tests/fixtures/headlines/Thm.agda | 15 +++++++++++++++ 8 files changed, 86 insertions(+), 19 deletions(-) create mode 100644 tests/fixtures/headlines/All.agda create mode 100644 tests/fixtures/headlines/Thm.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 8fbd2d2..839a1e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,10 @@ All notable changes to arghda-core are documented here. The format follows `/.arghda/config.toml` (or an explicit `--config `). Precedence is built-in default < `config.toml` < CLI `--headline-pattern`. Missing file ⇒ defaults; unknown keys are rejected so typos surface. +- DAG `headlines` field: each `dag` node now carries the sorted, deduped list + of top-level headline theorem names it declares (the spec's per-node + `headlines` array), extracted with the same logic as `unpinned-headline` and + honouring the configured headline pattern. Completes the v0 DAG schema. - 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 diff --git a/README.md b/README.md index 583f79b..60eddc6 100644 --- a/README.md +++ b/README.md @@ -39,8 +39,9 @@ record. - Workspace state machine — transitions are file moves, each logged to `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`, `invalidate`) -- `dag` — emits the dependency-DAG JSON (nodes + import edges + blocked - list) for a source tree: the contract a visual layer consumes +- `dag` — emits the dependency-DAG JSON (nodes — each with its lint status + and declared `headlines` — plus import edges and a blocked list) for a + source tree: the contract a visual layer consumes - `check` — runs Agda on a file and combines the typecheck verdict with the lint report (degrades gracefully when `agda` is absent) - First-class import graph (the `graph` module, lifted out of the orphan rule) @@ -66,11 +67,8 @@ built-in default < `config.toml` < CLI flag. Current schema: 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); the Groove service manifest. (`missing-without-k` is -subsumed by `missing-safe-pragma`, which already reports a missing -`--without-K`.) +Not yet: the Groove service manifest. (`missing-without-k` is subsumed by +`missing-safe-pragma`, which already reports a missing `--without-K`.) ## Build diff --git a/src/dag.rs b/src/dag.rs index d6b0f54..30a7894 100644 --- a/src/dag.rs +++ b/src/dag.rs @@ -9,9 +9,10 @@ use crate::diagnostic::Severity; use crate::graph::{self, Edge}; -use crate::lint::{run_lints, LintContext, LintRule}; +use crate::lint::{run_lints, unpinned_headline, LintContext, LintRule}; use crate::timestamp::now_rfc3339; -use anyhow::Result; +use anyhow::{Context, Result}; +use regex::Regex; use serde::Serialize; use std::collections::{BTreeMap, BTreeSet}; use std::path::{Path, PathBuf}; @@ -31,6 +32,9 @@ pub struct DagNode { /// `clean` | `warn` | `blocked` (lint-derived; not a proof claim). pub status: &'static str, pub lint: LintSummary, + /// Top-level theorem names this module declares that match the headline + /// pattern (sorted, deduped). The spec's per-node `headlines` array. + pub headlines: Vec, } /// A module that cannot advance, and why. @@ -54,13 +58,17 @@ pub struct DagDocument { } /// Build the DAG document for the source tree at `include_root`, using -/// `entry_modules` (the union of CI roots) for the orphan-reachability rule -/// and `rules` as the lint pack. +/// `entry_modules` (the union of CI roots) for the orphan-reachability rule, +/// `rules` as the lint pack, and `headline_pattern` (the same regex the +/// `unpinned-headline` rule uses) to populate each node's `headlines` array. pub fn build( include_root: &Path, entry_modules: &[PathBuf], rules: &[Box], + headline_pattern: &str, ) -> Result { + let headline_matcher = Regex::new(headline_pattern) + .with_context(|| format!("compiling headline pattern `{headline_pattern}`"))?; let graph = graph::build(include_root)?; let ctx = LintContext { include_root, @@ -95,11 +103,23 @@ pub fn build( "clean" }; + // Headline theorem names this module declares (sorted, deduped), + // extracted with the same logic as the `unpinned-headline` rule. + let contents = std::fs::read_to_string(&abs).unwrap_or_default(); + let mut headlines: Vec = + unpinned_headline::headline_decls(&contents, &headline_matcher) + .into_iter() + .map(|(name, _line)| name) + .collect(); + headlines.sort(); + headlines.dedup(); + nodes.push(DagNode { id: gn.id.clone(), file: gn.file.clone(), status, lint: summary, + headlines, }); } diff --git a/src/lint/unpinned_headline.rs b/src/lint/unpinned_headline.rs index 94713c2..4a47775 100644 --- a/src/lint/unpinned_headline.rs +++ b/src/lint/unpinned_headline.rs @@ -211,7 +211,10 @@ fn collect_pinned(contents: &str, out: &mut BTreeSet) { /// Top-level (column-0) type-signature names matching `matcher`, paired with /// the 1-based line they were declared on. `a b c : T` yields each name. -fn headline_decls(contents: &str, matcher: &Regex) -> Vec<(String, usize)> { +/// +/// Public so the `dag` builder can populate each node's `headlines` array +/// (the spec's DAG schema) from the same extractor this rule uses. +pub fn headline_decls(contents: &str, matcher: &Regex) -> Vec<(String, usize)> { let mut out = Vec::new(); let mut in_block_comment = false; diff --git a/src/main.rs b/src/main.rs index f91c29b..0df60ed 100644 --- a/src/main.rs +++ b/src/main.rs @@ -174,7 +174,8 @@ fn scan( unused: bool, json: bool, ) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; + let (roots, rules, _cfg) = + resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; let ctx = LintContext { include_root, entry_modules: &roots, @@ -324,8 +325,9 @@ fn dag( headline_pattern: Option<&str>, config: Option<&Path>, ) -> Result<()> { - let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; - let doc = build_dag(include_root, &roots, &rules)?; + let (roots, rules, cfg) = + resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; + let doc = build_dag(include_root, &roots, &rules, &cfg.headline_pattern)?; println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) } @@ -364,7 +366,7 @@ fn resolve_roots_and_rules( entry: &[PathBuf], headline_pattern: Option<&str>, config: Option<&Path>, -) -> Result<(Vec, RuleSet)> { +) -> Result<(Vec, RuleSet, RuleConfig)> { for e in entry { if !e.is_file() { anyhow::bail!("entry module not found: {}", e.display()); @@ -388,7 +390,7 @@ fn resolve_roots_and_rules( } else { rules_with_config(&cfg)? }; - Ok((roots, rules)) + Ok((roots, rules, cfg)) } fn transition(workspace: &Path, file: &str, from: State, to: State) -> Result<()> { diff --git a/tests/dag.rs b/tests/dag.rs index f46205e..3936a29 100644 --- a/tests/dag.rs +++ b/tests/dag.rs @@ -1,5 +1,6 @@ //! `dag` document construction over the fixtures. +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; use arghda_core::{build_dag, default_rules}; use std::path::PathBuf; @@ -15,7 +16,7 @@ fn fixture(name: &str) -> PathBuf { fn dag_over_orphan_fixture_has_expected_shape() { let root = fixture("orphan"); let roots = [root.join("All.agda")]; - let doc = build_dag(&root, &roots, &default_rules()).unwrap(); + let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); // Nodes are deterministic and sorted by module id. let ids: Vec<&str> = doc.nodes.iter().map(|n| n.id.as_str()).collect(); @@ -53,7 +54,7 @@ fn dag_over_orphan_fixture_has_expected_shape() { fn dag_over_wellformed_fixture_is_all_clean() { let root = fixture("wellformed"); let roots = [root.join("All.agda")]; - let doc = build_dag(&root, &roots, &default_rules()).unwrap(); + let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); assert_eq!(doc.version, "0.1"); assert!( @@ -65,3 +66,22 @@ fn dag_over_wellformed_fixture_is_all_clean() { assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Good")); assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Util")); } + +#[test] +fn dag_populates_node_headlines() { + let root = fixture("headlines"); + let roots = [root.join("All.agda")]; + let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); + + // `Thm` declares two top-level headline signatures (sorted, deduped); its + // indented `private` helper is not top-level and is not surfaced. + let thm = doc.nodes.iter().find(|n| n.id == "Thm").unwrap(); + assert_eq!( + thm.headlines, + vec!["thm-one".to_string(), "thm-two".to_string()] + ); + + // The entry module has only imports, so no headlines. + let all = doc.nodes.iter().find(|n| n.id == "All").unwrap(); + assert!(all.headlines.is_empty()); +} diff --git a/tests/fixtures/headlines/All.agda b/tests/fixtures/headlines/All.agda new file mode 100644 index 0000000..e2350bc --- /dev/null +++ b/tests/fixtures/headlines/All.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe --without-K #-} + +module All where + +open import Thm diff --git a/tests/fixtures/headlines/Thm.agda b/tests/fixtures/headlines/Thm.agda new file mode 100644 index 0000000..9e6af55 --- /dev/null +++ b/tests/fixtures/headlines/Thm.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} + +module Thm where + +-- Two top-level headline signatures the DAG should surface, plus an +-- indented (non-top-level) helper that must NOT be surfaced. +thm-one : Set₁ +thm-one = Set + +thm-two : Set₁ +thm-two = Set + +private + helper : Set₁ + helper = Set