diff --git a/autoform_cli/README.md b/autoform_cli/README.md index c316452a..3d09413a 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -83,9 +83,9 @@ An article asserts only facts a human or agent verified: | Key | Meaning | | --- | --- | -| `statement: formalized` | The Lean statement exists and compiles. | +| `statement: formalized` | The Lean statement exists and compiles. Requires `lean:`. | | `statement: retracted` | A revision retracted the statement while `lean:` still names the old declaration, which stays in the build until Formalize restates the article and records `statement: formalized` in its place. Requires `lean:`; invalid with `proof: formalized` or `mathlib: true`. CI's `autoform check` at an older `AUTOFORM_REF` rejects the marker, so move the pin first; until then, retract by removing `statement` and `proof` and keeping `lean:`. | -| `proof: formalized` | The Lean proof compiles. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. | +| `proof: formalized` | The Lean proof compiles. Requires `statement: formalized` and `lean:`. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. | | `mathlib: true` | The result is upstreamed into Mathlib. | | `not_ready: true` | Needs more blueprint work before it can be attempted. | | `lean: Ns.decl` | Declaration name(s) that discharge the article. | @@ -533,12 +533,11 @@ target. The article revision hashes that article's bytes alone. A Lean target's local scan does not find the declaration. The scan skips build output and nested checkouts, meaning any subdirectory with a `.git` entry, such as a worker's worktree or a submodule. Blockers are unmet dependency IDs or one of -`roadmap:not-a-formalizable-leaf`, `roadmap:proof-without-statement`, -`roadmap:missing-article-id`, `roadmap:missing-article-revision`, and -`roadmap:not-ready`. The claim target prefers durable `article_id` metadata. -`work list` fails explicitly if an unfinished formalizable leaf lacks one; plan -the missing IDs with `autoform migrate article-ids` and add them to the -frontmatter. `work context` may still select that article by its path ID to +`roadmap:not-a-formalizable-leaf`, `roadmap:missing-article-id`, +`roadmap:missing-article-revision`, and `roadmap:not-ready`. The claim target +prefers durable `article_id` metadata. `work list` fails explicitly if an +unfinished formalizable leaf lacks one; plan the missing IDs with `autoform +migrate article-ids` and add them to the frontmatter. `work context` may still select that article by its path ID to report the migration blocker. An item whose article records `statement: retracted` is a revision: it carries `revision` true in JSON, and the text of `work list` adds a `revision:` line and `work context` a `Revision:` line saying @@ -605,22 +604,29 @@ SECONDS` sets the probe's budget, 600 seconds by default. The report lists: - helpers that no article names, each with an owner when one exists: the article naming its nearest ancestor by name, such as `Foo` for `Foo.aux`; - impacted articles without a Markdown dependency path to the revised article; +- in `unused_statement_dependencies`, the stated articles whose Markdown + statement rests on the revised article, directly or through other statement + dependencies, but which are not statement-impacted: a dependent whose Lean + inlines a revised definition's body instead of naming it shows no use, yet + its statement changes meaning with the revision; - every deprecated project declaration with its replacement, its users, not counting companions Lean generates for it such as `X.eq_1`, and the other articles whose `lean:` names it, and in `deprecated_unused` those with no users and no such article; - the claim targets: the revised article's first, then every impacted - article's, every helper owner's, and, for a helper without an owner, a - `lean/-` key derived from its name, so two revisions touching - the same helper contend for the same claim; each helper reports its key as - `claim_target`. A revised declaration that no article names is claimed the - same way, under its owner's target or its own key. - -A revision is `contained` when no other article uses it and every helper it -impacts or revises belongs to the revised article, so its only claim target is -that article's; it can then be made in place under -that article's claim. A declaration derived from a revised one without naming -it in its statement changes with it, but `work impact` does not report that + article's, every unused statement dependency's, every helper owner's, and, + for a helper without an owner, a `lean/-` key derived from its + name, so two revisions touching the same helper contend for the same claim; + each helper reports its key as `claim_target`. A revised declaration that no + article names is claimed the same way, under its owner's target or its own + key. + +A revision is `contained` when no other article uses it, it has no unused +statement dependency, and every helper it impacts or revises belongs to the +revised article, so its only claim target is that article's; it can then be +made in place under that article's claim. A declaration derived from a +revised one without naming it in its statement changes with it, but `work +impact` does not report that declaration's users: the additive form `to_additive` writes, which goes unreported itself, or a direction `alias ⟨mp, mpr⟩ :=` takes of an `Iff`, which shows only as proof-impacted. Check such derivations on the revised set by @@ -702,8 +708,10 @@ example](../skills/setup/assets/cabannes-thesis-project/mkdocs.yml). `autoform check` rejects cycles, missing targets, escaping paths, self-dependencies, cycles introduced at any rolled-up containment level, -missing or multiple H1 titles, unsupported frontmatter keys, and assertion -values it does not recognize. With `--lean-root` it also fails on a `lean:` name +missing or multiple H1 titles, unsupported frontmatter keys, assertion values +it does not recognize, and assertions the Lean cannot back: `proof: formalized` +without `statement: formalized`, or either without a `lean:` name, even beside +`mathlib: true`. With `--lean-root` it also fails on a `lean:` name absent from the sources, as `leanblueprint checkdecls` does for LaTeX blueprints. It validates structure and leaves mathematical correctness to the agent and the Lean kernel. @@ -715,8 +723,8 @@ that may be regenerated at any time. `autoform audit` reports structured findings at blueprint-relative paths. It checks that formalizable articles are declaration-sized leaves with statement -text and an explicit dependency section, that asserted proof and Mathlib facts -are internally consistent, and that cited work resolves to local source +text and an explicit dependency section, that asserted Mathlib facts are +internally consistent, and that cited work resolves to local source material without escaping the blueprint. Coverage files are checked for broken links and explicitly declared gaps. With `--lean-root`, local declaration names and declaration kinds are checked against the Lean source index. @@ -931,7 +939,8 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5). deprecated, `sorry`'d X, show "conditional, assumes R" although R's text now describes X', and keep X out of `deprecated_unused`, so R could never record its proof. The claim set is every article whose frontmatter or - Lean changes: R, the statement-impacted articles, and, in that case, the + Lean changes: R, the statement-impacted articles, the unused statement + dependencies, and, in that case, the proof-impacted ones. - **In place**, only when X and X' cannot coexist, for example an instance or a structure change: the claim set is every `claim_targets` entry. @@ -951,6 +960,12 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5). uses it. When neither applies, the revision is blocked: release the claims and report it. Record what happened under `## Execution notes` of each touched article. + + An unused statement dependency, which rules out the contained route, is + re-reviewed under X's new meaning like a statement-impacted article: it + keeps `statement` only after an Agent Review of its source faithfulness; + otherwise it records `statement: retracted`, loses `proof`, and keeps + `lean:`. 3. Claim the route's claim set with one `autoform claim acquire`. When it is refused, release everything and report the held claim as the blocker. After acquiring, re-run `work impact`; if the set grew, release and start over diff --git a/autoform_cli/audit.py b/autoform_cli/audit.py index dfed3402..0517447c 100644 --- a/autoform_cli/audit.py +++ b/autoform_cli/audit.py @@ -203,15 +203,6 @@ def audit_graph( ) ) - if node.proof_formalized and not node.statement_formalized: - findings.append( - AuditFinding( - article_path, - "proof-without-statement", - "proof is marked formalized but the statement is not marked formalized", - ) - ) - if node.mathlib and not declaration_names(node.mathlib_declaration or ""): findings.append( AuditFinding( @@ -387,16 +378,6 @@ def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]: node = graph.nodes[node_id] article_path = _relative_path(node.path, graph.blueprint_dir) names = declaration_names(node.lean or "") - if (node.statement_formalized or node.proof_formalized) and not names: - findings.append( - AuditFinding( - article_path, - "missing-lean-target", - "formalized local work has no lean declaration target", - ) - ) - continue - resolved = [] for name in names: declaration = index.find(name) diff --git a/autoform_cli/doctor.py b/autoform_cli/doctor.py index d855c160..4e2a8c11 100644 --- a/autoform_cli/doctor.py +++ b/autoform_cli/doctor.py @@ -31,7 +31,6 @@ "lean-target-deprecated", "lean-target-kind-mismatch", "lean-target-not-found", - "missing-lean-target", } ) _CHECK_NAMES = ("blueprint", "runtime", "graph", "references", "audit", "lean targets") diff --git a/autoform_cli/graph.py b/autoform_cli/graph.py index aa08c31c..ebf73854 100644 --- a/autoform_cli/graph.py +++ b/autoform_cli/graph.py @@ -15,6 +15,8 @@ from pathlib import Path from urllib.parse import unquote, urlsplit +from .lean import declaration_names + _HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$") _FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})") @@ -488,6 +490,14 @@ def _parse_frontmatter(node_id: str, lines: list[str]) -> tuple[dict[str, str], issues.append(f"{node_id}: proof: formalized needs statement: formalized, not retracted") if metadata.get("mathlib") in _TRUE: issues.append(f"{node_id}: a mathlib: true article cannot record statement: retracted") + # Load errors rather than audit findings: the generated workflows never run + # the audit, so either state would otherwise publish as proved with no Lean + # statement behind it. `mathlib: true` exempts neither. + if metadata.get("proof") == _FORMALIZED and metadata.get("statement") not in {_FORMALIZED, _RETRACTED}: + issues.append(f"{node_id}: proof: formalized needs statement: formalized") + formalized = [key for key in ("statement", "proof") if metadata.get(key) == _FORMALIZED] + if formalized and not declaration_names(metadata.get("lean", "")): + issues.append(f"{node_id}: {formalized[0]}: formalized needs the lean: declaration that formalizes it") return metadata, end + 1, issues diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py index a749da2a..53f4555a 100644 --- a/autoform_cli/impact.py +++ b/autoform_cli/impact.py @@ -301,6 +301,8 @@ class ImpactArticle: article_id: str | None declarations: tuple[str, ...] dependencies: tuple[str, ...] = () + statement_dependencies: tuple[str, ...] = () + stated: bool = False @property def claim_target(self) -> str: @@ -388,6 +390,10 @@ class ImpactReport: proof_impacted: tuple[ImpactedArticle, ...] helpers: tuple[ImpactHelper, ...] undeclared_dependencies: tuple[str, ...] + #: Stated articles whose Markdown statement rests on the revised article, + #: through statement edges only, that are not statement-impacted: their Lean + #: may inline a revised definition's body instead of naming it. + unused_statement_dependencies: tuple[str, ...] deprecated: tuple[DeprecatedConstant, ...] deprecated_unused: tuple[str, ...] claim_targets: tuple[str, ...] @@ -399,9 +405,10 @@ def contained(self) -> bool: A helper the revised article owns, such as a structure's generated constructor or recursor, is repaired under that article's claim, so it does not count; any other helper, owned or not, does, and so does a - revised declaration that belongs to another article or to none. The - revision is contained exactly when its only claim target is the - revised article's. + revised declaration that belongs to another article or to none, or a + stated article whose Markdown statement rests on the revised one, even + when its Lean shows no use. The revision is contained exactly when its + only claim target is the revised article's. """ return self.claim_targets == (self.article.claim_target,) @@ -421,6 +428,7 @@ def as_dict(self) -> dict[str, object]: "proof_impacted": [item.as_dict() for item in self.proof_impacted], "helpers": [helper.as_dict() for helper in self.helpers], "undeclared_dependencies": list(self.undeclared_dependencies), + "unused_statement_dependencies": list(self.unused_statement_dependencies), "deprecated": [item.as_dict() for item in self.deprecated], "deprecated_unused": list(self.deprecated_unused), "claim_targets": list(self.claim_targets), @@ -523,6 +531,18 @@ def compute_impact( impacted = (*statement_impacted, *proof_impacted) undeclared = sorted(item.id for item in impacted if not _reaches(item.id, revised.id, by_id)) + # The probe sees only names, so a dependent whose Lean inlines a revised + # definition's body instead of naming it would keep its statement under the + # old meaning; its Markdown statement dependency is the only trace. + statement_ids = {item.id for item in statement_impacted} + unused = sorted( + article.id + for article in articles + if article.stated + and article.id != revised.id + and article.id not in statement_ids + and _reaches(article.id, revised.id, by_id, statement_only=True) + ) deprecated_users: dict[str, set[str]] = {} for record in records.values(): @@ -542,7 +562,11 @@ def compute_impact( # A helper is repaired under its owner's claim, so the owner is claimed # too; an unowned helper is repaired under a claim keyed by its own name. # A revised declaration no article names is claimed the same way. - others = {item.claim_target for item in impacted} | {helper.claim_target for helper in helpers} + others = ( + {item.claim_target for item in impacted} + | {by_id[article_id].claim_target for article_id in unused} + | {helper.claim_target for helper in helpers} + ) for name in revised_names: if name not in named: owner = _owner(records[name], records, named) @@ -556,6 +580,7 @@ def compute_impact( proof_impacted=tuple(proof_impacted), helpers=tuple(helpers), undeclared_dependencies=tuple(undeclared), + unused_statement_dependencies=tuple(unused), deprecated=deprecated, deprecated_unused=tuple(item.name for item in deprecated if not item.users and not item.articles), claim_targets=claim_targets, @@ -642,14 +667,17 @@ def _descends_from(record: ConstantRecord, ancestor: str, records: Mapping[str, return False -def _reaches(start: str, target: str, articles: Mapping[str, ImpactArticle]) -> bool: - """Whether ``start`` reaches ``target`` through Markdown dependencies.""" +def _reaches( + start: str, target: str, articles: Mapping[str, ImpactArticle], *, statement_only: bool = False +) -> bool: + """Whether ``start`` reaches ``target`` through Markdown dependencies, or only statement ones.""" seen = {start} work = [start] while work: article = articles.get(work.pop()) - for dependency in article.dependencies if article is not None else (): + edges = () if article is None else article.statement_dependencies if statement_only else article.dependencies + for dependency in edges: if dependency == target: return True if dependency not in seen: @@ -716,6 +744,8 @@ def revision_impact( node.article_id, tuple(dict.fromkeys(target.declaration for target in node.lean_targets)), tuple(node.dependencies), + tuple(node.statement_dependencies), + node.status.stated, ) for node in runtime.nodes } @@ -798,6 +828,11 @@ def format_impact(report: ImpactReport) -> list[str]: "Impacted without a Markdown dependency path to the revised article: " + ", ".join(report.undeclared_dependencies) ) + if report.unused_statement_dependencies: + lines.append( + "Statement dependents in Markdown that are not statement impacted: " + + ", ".join(report.unused_statement_dependencies) + ) if report.deprecated: lines.append("Deprecated:") for item in report.deprecated: diff --git a/autoform_cli/work.py b/autoform_cli/work.py index 89661fd4..55642928 100644 --- a/autoform_cli/work.py +++ b/autoform_cli/work.py @@ -105,7 +105,7 @@ def _blockers(node: RuntimeNode) -> tuple[str, ...]: if not node.dispatchable: return ("roadmap:not-a-formalizable-leaf",) if node.status.proved: - return () if node.status.stated else ("roadmap:proof-without-statement",) + return () metadata_blockers: list[str] = [] if node.article_id is None: metadata_blockers.append("roadmap:missing-article-id") diff --git a/tests/test_audit.py b/tests/test_audit.py index 7d576fd2..24bb6823 100644 --- a/tests/test_audit.py +++ b/tests/test_audit.py @@ -109,7 +109,7 @@ def test_clean_audit_has_stable_machine_readable_representation(tmp_path: Path) assert str(tmp_path) not in first.to_json() -def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp_path: Path) -> None: +def test_audit_reports_formalizable_structure(tmp_path: Path) -> None: blueprint = tmp_path / "blueprint" _coverage(blueprint) _article( @@ -118,7 +118,6 @@ def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp prose="", depends=False, declaration="theorem", - proof="formalized", ) _article(blueprint, "chapter/child.md", declaration="lemma") @@ -129,7 +128,6 @@ def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp "formalizable-container", "missing-depends-section", "missing-statement-text", - "proof-without-statement", } assert all(reason for _code, reason in findings) @@ -222,12 +220,6 @@ def test_audit_validates_lean_targets_only_when_root_is_supplied(tmp_path: Path) statement="formalized", lean="Project.missing", ) - _article( - blueprint, - "untargeted.md", - declaration="lemma", - statement="formalized", - ) _article( blueprint, "wrong-kind.md", @@ -246,9 +238,6 @@ def test_audit_validates_lean_targets_only_when_root_is_supplied(tmp_path: Path) assert with_lean["roadmap/missing.md"] == [ ("lean-target-not-found", "Lean declaration target was not found: Project.missing") ] - assert with_lean["roadmap/untargeted.md"] == [ - ("missing-lean-target", "formalized local work has no lean declaration target") - ] assert with_lean["roadmap/wrong-kind.md"] == [ ("lean-target-kind-mismatch", "Lean target kind def does not match declaration intent theorem") ] diff --git a/tests/test_contract.py b/tests/test_contract.py index 6f7d590b..f09a4cbc 100644 --- a/tests/test_contract.py +++ b/tests/test_contract.py @@ -68,7 +68,8 @@ def _generate(rng: random.Random) -> list[_Spec]: lean = None if rng.random() < 0.6: lean = f"Gen.{name}" if rng.random() < 0.8 else f"Gen.{name}, Gen.{name}_aux" - statements = [None, "formalized"] + (["retracted"] if lean and not mathlib else []) + # The loader requires lean: for a formalized statement or proof. + statements = [None] + (["formalized"] if lean else []) + (["retracted"] if lean and not mathlib else []) statement = rng.choices(statements, weights=[35, 45, 20][: len(statements)])[0] statement_dependencies: list[str] = [] proof_dependencies: list[str] = [] @@ -83,7 +84,7 @@ def _generate(rng: random.Random) -> list[_Spec]: name=name, declaration=declaration, statement=statement, - proof=statement != "retracted" and rng.random() < 0.35, + proof=statement == "formalized" and rng.random() < 0.35, mathlib=mathlib, not_ready=rng.random() < 0.1, lean=lean, @@ -127,12 +128,12 @@ def _open_statements(specs: list[_Spec], open_policy: bool) -> dict[str, frozens """The open statements each article's proof rests on, from the frontmatter alone. An open statement is a theorem that is not proved but is stated or records - ``statement: retracted``; its own proof is the ``sorry``. A stated one need - not name ``lean:``, but only those that do appear in the contract, so only - they can be open there. A dependency that is open contributes itself and - what its statement prerequisites reach, a proved dependency or a definition - naming ``lean:`` passes on everything it reaches, and anything else (an - unstated theorem, a Mathlib article) reaches nothing. + ``statement: retracted``; its own proof is the ``sorry``. Either way it + names ``lean:``, which the loader requires. A dependency that is open + contributes itself and what its statement prerequisites reach, a proved + dependency or a definition naming ``lean:`` passes on everything it + reaches, and anything else (an unstated theorem, a Mathlib article) + reaches nothing. """ reaches: dict[str, frozenset[str]] = {} assumes: dict[str, frozenset[str]] = {} @@ -153,13 +154,18 @@ def _open_statements(specs: list[_Spec], open_policy: bool) -> dict[str, frozens return assumes -_RETRACTION_FAULTS = { +_LOAD_FAULTS = { "no lean": ( {"lean": None}, "{name}: statement: retracted needs the lean: declaration it retracts; without lean:, omit statement", ), "proof": ({"proof": True}, "{name}: proof: formalized needs statement: formalized, not retracted"), "mathlib": ({"mathlib": True}, "{name}: a mathlib: true article cannot record statement: retracted"), + "formalized without lean": ( + {"statement": "formalized", "lean": None}, + "{name}: statement: formalized needs the lean: declaration that formalizes it", + ), + "proof without statement": ({"statement": None, "proof": True}, "{name}: proof: formalized needs statement: formalized"), } @@ -282,7 +288,6 @@ def transitive(name: str) -> set[str]: assert article.declarations == tuple(declaration_names(spec.lean or "")) assert (article.state, article.assumes) == (status.key, status.assumes) assert set(article.allowed_open_declarations) <= open_declarations, name - # A stated theorem without lean: is still assumed, but names nothing to allow. allowed = { declaration for assumed in status.assumes @@ -320,9 +325,10 @@ def test_random_roadmaps_keep_the_wiki_and_lean_contract(repo_root: Path, tmp_pa except AssertionError as error: raise AssertionError(f"seed {seed}, policy {policy}: {error}") from error - # 11. Each invalid retraction is refused at load, with its own message. - fault = rng.choice(sorted(_RETRACTION_FAULTS)) - changes, message = _RETRACTION_FAULTS[fault] + # 11. Each invalid retraction, and each formalized assertion the Lean + # cannot back, is refused at load, with its own message. + fault = rng.choice(sorted(_LOAD_FAULTS)) + changes, message = _LOAD_FAULTS[fault] victim = rng.randrange(len(specs)) fields = {"statement": "retracted", "lean": f"Gen.{specs[victim].name}", "proof": False, "mathlib": False} broken = replace(specs[victim], **{**fields, **changes}) @@ -339,7 +345,7 @@ def test_random_roadmaps_keep_the_wiki_and_lean_contract(repo_root: Path, tmp_pa expected |= {f"allowed:{state.key}" for state in STATES} expected |= {"work:statement", "work:proof", "work:missing-article-id"} expected |= {"contract:open", "contract:retracted-open", "contract:mathlib"} - expected |= {f"invalid:{fault}" for fault in _RETRACTION_FAULTS} + expected |= {f"invalid:{fault}" for fault in _LOAD_FAULTS} assert expected <= seen, sorted(expected - seen) diff --git a/tests/test_graph.py b/tests/test_graph.py index 7a7da9fe..762eca4d 100644 --- a/tests/test_graph.py +++ b/tests/test_graph.py @@ -329,6 +329,50 @@ def test_rejects_a_retracted_statement_that_cannot_keep_its_declaration( assert raised.value.issues == (message,) +@pytest.mark.parametrize( + ("metadata", "issues"), + [ + ( + {"proof": "formalized", "lean": "Ns.result"}, + ("result: proof: formalized needs statement: formalized",), + ), + ( + {"proof": "formalized", "lean": "Ns.result", "mathlib": "true"}, + ("result: proof: formalized needs statement: formalized",), + ), + ( + {"statement": "formalized"}, + ("result: statement: formalized needs the lean: declaration that formalizes it",), + ), + ( + {"statement": "formalized", "proof": "formalized", "mathlib": "true"}, + ("result: statement: formalized needs the lean: declaration that formalizes it",), + ), + ( + {"statement": "formalized", "lean": ","}, + ("result: statement: formalized needs the lean: declaration that formalizes it",), + ), + ( + {"proof": "formalized"}, + ( + "result: proof: formalized needs statement: formalized", + "result: proof: formalized needs the lean: declaration that formalizes it", + ), + ), + ], +) +def test_rejects_formalized_work_the_lean_does_not_show( + tmp_path: Path, metadata: dict[str, str], issues: tuple[str, ...] +) -> None: + blueprint = tmp_path / "blueprint" + _node(blueprint, "result.md", "# Result\n", declaration="theorem", **metadata) + + with pytest.raises(GraphValidationError) as raised: + load_graph(blueprint) + + assert raised.value.issues == issues + + def test_records_origin_and_source_links_without_treating_them_as_edges(tmp_path: Path) -> None: blueprint = tmp_path / "blueprint" source = blueprint / "sources" / "paper.md" diff --git a/tests/test_impact.py b/tests/test_impact.py index b349f6c2..8985940a 100644 --- a/tests/test_impact.py +++ b/tests/test_impact.py @@ -53,9 +53,14 @@ def _records(*records: ConstantRecord) -> dict[str, ConstantRecord]: def _article( - node_id: str, *declarations: str, article_id: str | None = None, dependencies: tuple[str, ...] = () + node_id: str, + *declarations: str, + article_id: str | None = None, + dependencies: tuple[str, ...] = (), + statement_dependencies: tuple[str, ...] = (), + stated: bool = False, ) -> ImpactArticle: - return ImpactArticle(node_id, article_id, declarations, dependencies) + return ImpactArticle(node_id, article_id, declarations, dependencies, statement_dependencies, stated) def _impact(records, articles, revised: str, declarations=None, **kwargs): @@ -284,6 +289,61 @@ def test_undeclared_dependencies_and_claim_targets() -> None: assert report.claim_targets == ("af_base", "af_detached", "af_direct", "af_loose", "chapter/transitive") +def test_stated_markdown_statement_dependents_the_lean_does_not_show_are_reported() -> None: + records = _records( + _rec("A.base", "def"), + _rec("A.direct", type_uses=("A.base",)), + _rec("A.inlined"), + _rec("A.proofOnly", value_uses=("A.base",)), + _rec("A.unstated"), + _rec("A.viaProof"), + ) + + def stated(node_id: str, *declarations: str, on: str = "base", **fields: object) -> ImpactArticle: + return _article(node_id, *declarations, dependencies=(on,), statement_dependencies=(on,), stated=True, **fields) + + articles = [ + _article("base", "A.base", article_id="af_base", stated=True), + stated("direct", "A.direct"), + # Unstated and named by no article: it only carries the statement edge. + _article("middle", dependencies=("base",), statement_dependencies=("base",)), + stated("inlined", "A.inlined", on="middle", article_id="af_inlined"), + stated("proof-only", "A.proofOnly"), + _article("unstated", "A.unstated", dependencies=("base",), statement_dependencies=("base",)), + _article("via-proof", "A.viaProof", dependencies=("base",), stated=True), + ] + + report = _impact(records, articles, "base") + + assert _ids(report.statement_impacted) == ["direct"] + assert _ids(report.proof_impacted) == ["proof-only"] + assert report.unused_statement_dependencies == ("inlined", "proof-only") + assert report.as_dict()["unused_statement_dependencies"] == ["inlined", "proof-only"] + assert report.claim_targets == ("af_base", "af_inlined", "direct", "proof-only") + assert "Statement dependents in Markdown that are not statement impacted: inlined, proof-only" in ( + format_impact(report) + ) + + +def test_an_unused_statement_dependency_alone_keeps_a_revision_from_being_contained() -> None: + records = _records(_rec("A.leaf", "def"), _rec("A.inlined")) + articles = [ + _article("leaf", "A.leaf", stated=True), + _article("inlined", "A.inlined", dependencies=("leaf",), statement_dependencies=("leaf",), stated=True), + ] + + report = _impact(records, articles, "leaf") + + assert not report.contained + assert report.claim_targets == ("leaf", "inlined") + assert format_impact(report) == [ + "Revising A.leaf of leaf", + "Graph source revision: rev", + "Statement dependents in Markdown that are not statement impacted: inlined", + "Claim targets: leaf, inlined", + ] + + def test_deprecated_constants_report_users_through_internal_details() -> None: records = _records( _rec("A.new"), @@ -830,7 +890,7 @@ def _write_article( def _blueprint_project(tmp_path: Path, prefix: str) -> Path: - """A roadmap whose articles name ``{prefix}.base``, ``.uses``, ``.loose`` and nothing.""" + """A roadmap whose articles name ``{prefix}.base``, ``.uses``, ``.loose``, ``.inlines`` and nothing.""" project = tmp_path / "project" _write_article(project, "README.md", title="Chapter", metadata=["article_id: af_0000000000000000000000c0"]) @@ -850,6 +910,12 @@ def _blueprint_project(tmp_path: Path, prefix: str) -> Path: "loose.md", metadata=["declaration: theorem", "statement: formalized", f"lean: {prefix}.loose"], ) + _write_article( + project, + "inlines.md", + metadata=["declaration: theorem", "statement: formalized", f"lean: {prefix}.inlines"], + depends=("base.md",), + ) _write_article(project, "empty.md", metadata=["declaration: theorem"]) return project @@ -870,6 +936,7 @@ def _stub_lean_root(tmp_path: Path) -> Path: _payload("Demo.uses", type_uses=["Demo.base"]), _payload("Demo.base_eq", type_uses=["Demo.base"]), _payload("Demo.loose", value_uses=["Demo.base", "Demo.old"], uses_deprecated=["Demo.old"]), + _payload("Demo.inlines"), _payload("Demo.old", deprecated=True, replacement="Demo.base_eq"), _payload("Demo.gone", deprecated=True), ] @@ -928,12 +995,19 @@ def test_cli_writes_the_impact_report_as_canonical_json(tmp_path: Path, monkeypa } ], "undeclared_dependencies": ["chapter/loose"], + "unused_statement_dependencies": ["chapter/inlines"], "deprecated": [ {"name": "Demo.gone", "replacement": None, "users": [], "articles": []}, {"name": "Demo.old", "replacement": "Demo.base_eq", "users": ["Demo.loose"], "articles": []}, ], "deprecated_unused": ["Demo.gone"], - "claim_targets": [_BASE_ID, _USES_ID, "chapter/loose", "lean/demo-base-eq-7f17aa41d1461243"], + "claim_targets": [ + _BASE_ID, + _USES_ID, + "chapter/inlines", + "chapter/loose", + "lean/demo-base-eq-7f17aa41d1461243", + ], } (call,) = calls assert call["label"] == "impact probe" @@ -962,10 +1036,11 @@ def test_cli_text_report_lists_each_section(tmp_path: Path, monkeypatch, capsys) "Helpers no article names:", " Demo.base_eq (theorem, statement) Demo.lean:5; no owner; claim lean/demo-base-eq-7f17aa41d1461243", "Impacted without a Markdown dependency path to the revised article: chapter/loose", + "Statement dependents in Markdown that are not statement impacted: chapter/inlines", "Deprecated:", " Demo.gone: no users, safe to delete", " Demo.old -> Demo.base_eq: used by Demo.loose", - f"Claim targets: {_BASE_ID}, {_USES_ID}, chapter/loose, lean/demo-base-eq-7f17aa41d1461243", + f"Claim targets: {_BASE_ID}, {_USES_ID}, chapter/inlines, chapter/loose, lean/demo-base-eq-7f17aa41d1461243", ] assert calls[0]["timeout"] == skeleton.DEFAULT_PROBE_TIMEOUT @@ -1349,6 +1424,8 @@ def recorded(*args: object, **kwargs: object) -> str: ("Imp.usesOld", "theorem", "statement", "Imp/Extra.lean", 10, None), ] assert report["undeclared_dependencies"] == ["chapter/simp"] + # proved.md states on uses.md in Markdown, but its Lean statement does not mention base. + assert report["unused_statement_dependencies"] == ["chapter/proved"] # The equation lemma `@[simp]` gives oldSeed goes when oldSeed does. assert report["deprecated"] == [ {"name": "Imp.oldEq", "replacement": "Imp.base_eq", "users": ["Imp.usesOld"], "articles": []}, diff --git a/tests/test_render.py b/tests/test_render.py index c80e6809..c4a06c88 100644 --- a/tests/test_render.py +++ b/tests/test_render.py @@ -373,9 +373,12 @@ def test_overview_carries_the_counts_without_a_separate_progress_page(tmp_path: def test_statement_only_theorems_never_count_as_complete(tmp_path: Path) -> None: project = _project(tmp_path) roadmap = project / "blueprint/roadmap" + (project / "Project" / "Blocker.lean").write_text( + "namespace Project\n\ntheorem blocker : True := trivial\n\nend Project\n", encoding="utf-8" + ) blocker = roadmap / "blocker.md" blocker.write_text( - "---\ndeclaration: theorem\nstatement: formalized\n---\n\n# Blocker\n", + "---\ndeclaration: theorem\nstatement: formalized\nlean: Project.blocker\n---\n\n# Blocker\n", encoding="utf-8", ) top = roadmap / "top.md" @@ -396,7 +399,7 @@ def test_statement_only_theorems_never_count_as_complete(tmp_path: Path) -> None assert "1 of 3 targets complete" in blocked blocker.write_text( - "---\ndeclaration: theorem\nstatement: formalized\nproof: formalized\n---\n\n" + "---\ndeclaration: theorem\nstatement: formalized\nproof: formalized\nlean: Project.blocker\n---\n\n" "# Blocker\n", encoding="utf-8", ) @@ -1289,8 +1292,11 @@ def _conditional_project(tmp_path: Path, policy: str) -> Path: "## Results\n\n- [Open](open.md)\n- [Top](top.md)\n", encoding="utf-8", ) + (project / "Project" / "Open.lean").write_text( + "namespace Project\n\ntheorem openStatement : True := sorry\n\nend Project\n", encoding="utf-8" + ) (roadmap / "open.md").write_text( - "---\ndeclaration: theorem\nstatement: formalized\n---\n\n" + "---\ndeclaration: theorem\nstatement: formalized\nlean: Project.openStatement\n---\n\n" "# Open\n\nA statement whose proof is still sorry.\n\n## Depends on\n\n- [Base](base.md)\n", encoding="utf-8", ) diff --git a/tests/test_runtime.py b/tests/test_runtime.py index 35fd2d7d..ae829f99 100644 --- a/tests/test_runtime.py +++ b/tests/test_runtime.py @@ -303,7 +303,14 @@ def _policy_project(tmp_path: Path, policy: str | None) -> Path: **theorem, ) _article(project, "chapter/section/gap.md", title="Gap", declaration="theorem") - _article(project, "chapter/section/waiting.md", title="Waiting", proof_dependencies=("gap.md",), **theorem) + _article( + project, + "chapter/section/waiting.md", + title="Waiting", + lean="Project.waiting", + proof_dependencies=("gap.md",), + **theorem, + ) return project diff --git a/tests/test_status.py b/tests/test_status.py index 8112ac53..7d94232e 100644 --- a/tests/test_status.py +++ b/tests/test_status.py @@ -11,6 +11,9 @@ def _node(blueprint: Path, relative: str, body: str = "", **metadata: str) -> None: path = blueprint / "roadmap" / relative path.parent.mkdir(parents=True, exist_ok=True) + if "formalized" in (metadata.get("statement"), metadata.get("proof")): + # The graph rejects formalized work without a lean: name; status never reads it. + metadata.setdefault("lean", f"Project.{path.stem}") properties = [*(f"{key}: {value}" for key, value in metadata.items())] title = relative.removesuffix(".md").replace("-", " ").title() path.write_text( diff --git a/tests/test_visualization.py b/tests/test_visualization.py index 12bdf497..2aa02227 100644 --- a/tests/test_visualization.py +++ b/tests/test_visualization.py @@ -22,6 +22,9 @@ def _write_node( **metadata: str, ) -> None: path.parent.mkdir(parents=True, exist_ok=True) + if "formalized" in (metadata.get("statement"), metadata.get("proof")): + # The graph rejects formalized work without a lean: name. + metadata.setdefault("lean", f"Project.{path.stem}") properties = [*(f"{key}: {value}" for key, value in metadata.items())] lines = ["---", *properties, "---", "", f"# {title}"] if dependencies: diff --git a/tests/test_work.py b/tests/test_work.py index 70f766b5..b608e47d 100644 --- a/tests/test_work.py +++ b/tests/test_work.py @@ -220,21 +220,6 @@ def test_finished_articles_and_containers_need_no_identity(tmp_path: Path) -> No assert chapter.blockers == ("roadmap:not-a-formalizable-leaf",) -def test_proof_without_statement_returns_to_roadmap(tmp_path: Path) -> None: - project = _project(tmp_path) - _edit( - project, - "state.md", - "declaration: theorem\n", - "declaration: theorem\nproof: formalized\nlean: Project.state\n", - ) - - assert "chapter/state" not in {item.node_id for item in list_ready_work(project).items} - _, item = work_context(project, "chapter/state") - assert item.phase is None - assert item.blockers == ("roadmap:proof-without-statement",) - - def test_article_revision_tracks_only_its_own_article(tmp_path: Path) -> None: project = _project(tmp_path) article = project / "blueprint/roadmap/chapter/state.md" @@ -536,7 +521,7 @@ def _policy_project(tmp_path: Path, policy: str | None) -> Path: title="Upstream", metadata=["declaration: theorem", "mathlib: true", "lean: Project.upstream"], ) - _article(project, "unnamed.md", title="Unnamed", metadata=["declaration: def", "statement: formalized"]) + _article(project, "unnamed.md", title="Unnamed", metadata=[]) return project @@ -870,28 +855,6 @@ def test_work_assumptions_keeps_a_retracted_theorem_while_its_lean_names_the_old assert articles["chapter/reduction"]["allowed_open_declarations"] == list(allowed) -@pytest.mark.parametrize("policy", ["forbidden", "allowed"]) -def test_work_assumptions_bounds_a_proof_recorded_without_its_statement( - tmp_path: Path, capsys, policy: str -) -> None: - """`proof: formalized` without `statement: formalized` still declares Lean the CI probe must bound.""" - project = _policy_project(tmp_path, policy) - _edit(project, "reduction.md", "statement: formalized\n", "") - allowed = ("Project.open_aux", "Project.open_thm") if policy == "allowed" else () - - assert cli.main(["work", "assumptions", str(project), "--json"]) == 0 - articles = {article["id"]: article for article in json.loads(capsys.readouterr().out)["articles"]} - - assert articles["chapter/reduction"] == _contract_article( - "chapter/reduction", - "af_00000000000000000000000c", - "conditional" if policy == "allowed" else "proved", - ["Project.reduction"], - assumes=("chapter/open",) if policy == "allowed" else (), - allowed=allowed, - ) - - def test_work_assumptions_does_not_open_a_never_stated_theorem_naming_a_draft_lean(tmp_path: Path, capsys) -> None: """A draft `lean:` name on a theorem that was never stated is no assumption, so CI rejects its sorry.""" project = _policy_project(tmp_path, "allowed") @@ -914,13 +877,13 @@ def test_work_assumptions_does_not_open_a_never_stated_theorem_naming_a_draft_le def test_work_assumptions_text_labels_only_conditional_articles_as_conditional(tmp_path: Path, capsys) -> None: - """A conditional article without `lean:` is named too; an unproved one that assumes something is not conditional.""" + """An unproved article that assumes something is not conditional.""" project = _policy_project(tmp_path, "allowed") _article( project, "bare.md", title="Bare", - metadata=["declaration: theorem", "statement: formalized", "proof: formalized"], + metadata=["declaration: theorem", "statement: formalized", "proof: formalized", "lean: Project.bare"], proof_depends="open.md", ) _article( @@ -933,7 +896,7 @@ def test_work_assumptions_text_labels_only_conditional_articles_as_conditional(t assert cli.main(["work", "assumptions", str(project), "--json"]) == 0 articles = {article["id"]: article for article in json.loads(capsys.readouterr().out)["articles"]} - assert "chapter/bare" not in articles + assert articles["chapter/bare"]["state"] == "conditional" assert articles["chapter/old"] == _contract_article( "chapter/old", None,