diff --git a/autoform_cli/README.md b/autoform_cli/README.md index 5aba7679..560ab349 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -61,13 +61,16 @@ An article's statement is its body from the end of the frontmatter to the first `##` heading, without the H1 line. A deeper heading does not end it, and neither does a `##` line inside a fenced code block or an HTML comment. `autoform audit` and the published theorem box both read that span. A fence closes only on a -bare fence line; one that never closes is plain text on the page and hides no -heading and no dependency link. A later bare fence line of the same character -and at least the opener's length closes it here, though the page asks for the -opener's exact length and indent, so close each fence with its own line. The -page can also pair an unclosed backtick fence line with a later backtick run in -the same paragraph and show the text between them as inline code; a link there -is not a link on the page but is still read as a dependency. +bare fence line. A fence that never closes is read as plain text when its +article is inspected alone, so it hides no heading or dependency link there, +but on a chapter page it can pair with a later article's closing fence and hide +everything between them. The audit reports a fence with no closing line as +`unclosed-code-fence`. A later bare fence line of the same character and at +least the opener's length closes it here, though the page asks for the opener's +exact length and indent, so close each fence with its own line. The page can +also pair an unclosed backtick fence line with a later backtick run in the same +paragraph and show the text between them as inline code; a link there is not a +link on the page but is still read as a dependency. `## Depends on` lists what the article needs in order to be *stated*; `## Proof depends on` lists what only its *proof* needs. Both are graph edges. @@ -821,9 +824,10 @@ that may be regenerated at any time. ## Audit contract `autoform audit` reports structured findings at blueprint-relative paths. It -checks that formalizable articles are declaration-sized leaves with statement -text (prose in the statement, outside code blocks, HTML comments, and headings) -and an explicit dependency section, that asserted Mathlib facts are +checks that no article leaves a code fence open, that formalizable articles are +declaration-sized leaves with statement text (prose in the statement, outside +code blocks, HTML comments, and headings) 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 diff --git a/autoform_cli/audit.py b/autoform_cli/audit.py index 8e5a489b..10ad8a85 100644 --- a/autoform_cli/audit.py +++ b/autoform_cli/audit.py @@ -28,6 +28,8 @@ ) from .markdown import article_parts as _article_parts from .markdown import content_lines as _content_lines +from .markdown import first_unclosed_fence as _first_unclosed_fence +from .markdown import frontmatter_end as _frontmatter_end from .markdown import has_substance as _has_substance from .markdown import HEADING as _HEADING from .markdown import is_placeholder as _is_placeholder @@ -169,6 +171,15 @@ def audit_graph( children = contained.get(node_id, ()) article = _read_article(node.path) + if article.unclosed_fence is not None: + findings.append( + AuditFinding( + article_path, + "unclosed-code-fence", + f"code fence opened on line {article.unclosed_fence} never closes", + ) + ) + if node.formalizable: if children: findings.append( @@ -249,6 +260,8 @@ def audit_graph( class _ArticleShape: statement: str has_depends_section: bool + #: The one-based source line of the first fence that never closes. + unclosed_fence: int | None = None def _read_article(path: Path) -> _ArticleShape: @@ -258,9 +271,13 @@ def _read_article(path: Path) -> _ArticleShape: return _ArticleShape(statement="", has_depends_section=False) parts = _article_parts(text) + lines = text.splitlines() + start = _frontmatter_end(lines) + unclosed = _first_unclosed_fence(lines[start:]) return _ArticleShape( statement=parts.statement, has_depends_section=any(section.title.casefold() == "depends on" for section in parts.sections), + unclosed_fence=None if unclosed is None else start + unclosed + 1, ) diff --git a/autoform_cli/markdown.py b/autoform_cli/markdown.py index a48db156..6af44437 100644 --- a/autoform_cli/markdown.py +++ b/autoform_cli/markdown.py @@ -66,7 +66,7 @@ EXTERNAL_SCHEMES = frozenset({"http", "https"}) HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$") -FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})") +FENCE = re.compile(r"^ {0,3}(`{3,}(?=[^`]*$)|~{3,})") INLINE_CODE = re.compile(r"(`+).*?\1") HTML_COMMENT = re.compile(r"|$)", re.DOTALL) @@ -656,17 +656,35 @@ def local_target_issue( def mask_fences_and_comments(lines: list[str]) -> list[str]: """Return ``lines`` with fenced blocks and HTML comments blanked. - This is how the graph, the audit and the page agree on which headings and - links an article has. The site draws a fence without a closing line as - plain text, with the headings and links after it in view, so such a fence - hides nothing here. + This is how the graph and the audit agree on which headings and links an + article has. A fence without a closing line is read as plain text, so it + hides nothing here. A one-article page draws it the same way, but a chapter + page can pair it with a later article's fence, so the audit reports it as + ``unclosed-code-fence``. """ return _mask_fences_and_comments(lines, set(), unclosed_fence_is_text=True) +def first_unclosed_fence(lines: list[str]) -> int | None: + """Return the index of the first fence line that never closes, if any.""" + + unclosed: set[int] = set() + _mask_fences_and_comments( + lines, + set(), + unclosed_fence_is_text=True, + unclosed_openers=unclosed, + ) + return min(unclosed, default=None) + + def _mask_fences_and_comments( - lines: list[str], hidden: set[int], *, unclosed_fence_is_text: bool = False + lines: list[str], + hidden: set[int], + *, + unclosed_fence_is_text: bool = False, + unclosed_openers: set[int] | None = None, ) -> list[str]: masked: list[str] = [] fence: tuple[str, int] | None = None @@ -682,6 +700,8 @@ def _mask_fences_and_comments( if index == len(lines): # Read on from the fence's first line as text. unclosed[fence[0]] = fence[1] + if unclosed_openers is not None: + unclosed_openers.add(opened[0]) index, in_comment = opened del masked[index:] hidden.difference_update(range(index, len(lines))) @@ -809,5 +829,6 @@ def _is_within(path: Path, directory: Path) -> bool: "rendered_visible_text", "site_converter", "strip_line_comments", + "first_unclosed_fence", "visible_prose", ] diff --git a/autoform_cli/render.py b/autoform_cli/render.py index cb44c7ca..bdb08103 100644 --- a/autoform_cli/render.py +++ b/autoform_cli/render.py @@ -27,7 +27,7 @@ from .status import is_definition _HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$") -_FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})") +_FENCE = re.compile(r"^ {0,3}(`{3,}(?=[^`]*$)|~{3,})") _MARKDOWN_LINK = re.compile(r"(?[^\]]*)\]\(\s*(?P[^)\s]+)(?:\s+[^)]*)?\)") #: A reference-style link definition, `[label]: target "title"`. Markdown #: resolves `[Paper][paper]` through one of these, so a rewrite that only sees diff --git a/tests/test_audit.py b/tests/test_audit.py index cd1ebaa8..2d720b3e 100644 --- a/tests/test_audit.py +++ b/tests/test_audit.py @@ -7,6 +7,7 @@ import autoform_cli.audit as audit_module from autoform_cli.audit import audit_blueprint +from autoform_cli.graph import load_graph from autoform_cli.lean import LeanSourceError @@ -863,9 +864,72 @@ def test_audit_reports_one_statement_finding_at_a_time(tmp_path: Path) -> None: assert _statement_codes(tmp_path, "") == {"missing-statement-text"} -def test_a_statement_the_site_publishes_from_a_fence_that_never_closes_is_not_missing(tmp_path: Path) -> None: - assert _statement_codes(tmp_path, "```\nFor all n, P(n) holds.") == set() - assert _statement_codes(tmp_path, "```\nTODO") == {"placeholder-statement-text"} +def test_a_statement_from_a_fence_that_never_closes_keeps_its_statement_finding(tmp_path: Path) -> None: + assert _statement_codes(tmp_path, "```\nFor all n, P(n) holds.") == {"unclosed-code-fence"} + assert _statement_codes(tmp_path, "```\nTODO") == { + "placeholder-statement-text", + "unclosed-code-fence", + } + + +def test_audit_reports_an_unclosed_code_fence(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _coverage(blueprint) + path = _article(blueprint, "chapter/result.md", declaration="theorem") + path.write_text(path.read_text(encoding="utf-8") + "\n```lean\n#check result\n", encoding="utf-8") + + assert _finding_map(blueprint)["roadmap/chapter/result.md"] == [ + ("unclosed-code-fence", "code fence opened on line 13 never closes") + ] + + +def test_audit_reports_an_unclosed_code_fence_in_a_chapter_article(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _coverage(blueprint) + _article(blueprint, "chapter/result.md", declaration="theorem") + readme = blueprint / "roadmap" / "chapter" / "README.md" + readme.write_text("# Chapter\n\n```text\nsketch\n", encoding="utf-8") + + assert ("unclosed-code-fence", "code fence opened on line 3 never closes") in _finding_map(blueprint)[ + "roadmap/chapter/README.md" + ] + + +def test_audit_does_not_treat_inline_backticks_as_a_fence(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _coverage(blueprint) + path = _article(blueprint, "chapter/result.md", declaration="theorem") + path.write_text(path.read_text(encoding="utf-8") + "\n```x``` is inline code here.\n", encoding="utf-8") + + codes = { + code + for code, _reason in _finding_map(blueprint).get(path.relative_to(blueprint).as_posix(), []) + } + assert "unclosed-code-fence" not in codes + + +def test_audit_graph_does_not_reread_an_article_for_fences(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _coverage(blueprint) + path = _article(blueprint, "chapter/result.md", declaration="theorem") + graph = load_graph(blueprint) + path.unlink() + + result = audit_module.audit_graph(graph) + + assert "unclosed-code-fence" not in {finding.code for finding in result.findings} + + +def test_audit_ignores_fence_like_text_in_frontmatter(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _coverage(blueprint) + path = _article(blueprint, "chapter/result.md", declaration="theorem") + text = path.read_text(encoding="utf-8") + path.write_text(text.replace("---\n", "---\n#