From edf44d08d68f2932bfd5ec8ab34a61439384d92a Mon Sep 17 00:00:00 2001 From: 1cbyc Date: Fri, 9 Oct 2026 00:23:47 +0000 Subject: [PATCH 1/2] Report unclosed Markdown fences during audit Co-authored-by: insisong --- autoform_cli/README.md | 17 ++++++++++------- autoform_cli/audit.py | 12 ++++++++++++ autoform_cli/markdown.py | 22 +++++++++++++++++++++- tests/test_audit.py | 29 ++++++++++++++++++++++++----- 4 files changed, 67 insertions(+), 13 deletions(-) diff --git a/autoform_cli/README.md b/autoform_cli/README.md index 5aba76795..190b8fcd1 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 `unclosed-code-fence` before that +can corrupt the chapter. 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. diff --git a/autoform_cli/audit.py b/autoform_cli/audit.py index 8e5a489bc..31519b63d 100644 --- a/autoform_cli/audit.py +++ b/autoform_cli/audit.py @@ -33,6 +33,7 @@ from .markdown import is_placeholder as _is_placeholder from .markdown import local_target_issue as _local_target_issue from .markdown import markdown_links as _markdown_links +from .markdown import unclosed_fence_lines as _unclosed_fence_lines from .markdown import visible_prose as _visible_prose #: More siblings than this at one level is a table of contents, not a chapter. @@ -169,6 +170,17 @@ def audit_graph( children = contained.get(node_id, ()) article = _read_article(node.path) + unclosed_fences = _unclosed_fence_lines(node.path.read_text(encoding="utf-8").splitlines()) + if unclosed_fences: + lines = ", ".join(str(line) for line in unclosed_fences) + findings.append( + AuditFinding( + article_path, + "unclosed-code-fence", + f"code fence opened on line {lines} never closes", + ) + ) + if node.formalizable: if children: findings.append( diff --git a/autoform_cli/markdown.py b/autoform_cli/markdown.py index a48db1563..888d2b1a7 100644 --- a/autoform_cli/markdown.py +++ b/autoform_cli/markdown.py @@ -665,8 +665,25 @@ def mask_fences_and_comments(lines: list[str]) -> list[str]: return _mask_fences_and_comments(lines, set(), unclosed_fence_is_text=True) +def unclosed_fence_lines(lines: list[str]) -> tuple[int, ...]: + """Return the one-based source lines of fences that never close.""" + + unclosed: set[int] = set() + _mask_fences_and_comments( + lines, + set(), + unclosed_fence_is_text=True, + unclosed_fence_lines=unclosed, + ) + return tuple(line + 1 for line in sorted(unclosed)) + + 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_fence_lines: set[int] | None = None, ) -> list[str]: masked: list[str] = [] fence: tuple[str, int] | None = None @@ -682,6 +699,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_fence_lines is not None: + unclosed_fence_lines.add(opened[0]) index, in_comment = opened del masked[index:] hidden.difference_update(range(index, len(lines))) @@ -809,5 +828,6 @@ def _is_within(path: Path, directory: Path) -> bool: "rendered_visible_text", "site_converter", "strip_line_comments", + "unclosed_fence_lines", "visible_prose", ] diff --git a/tests/test_audit.py b/tests/test_audit.py index cd1ebaa85..21b3e41bb 100644 --- a/tests/test_audit.py +++ b/tests/test_audit.py @@ -863,9 +863,23 @@ 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_statement_findings_say_what_is_wrong(tmp_path: Path) -> None: @@ -900,9 +914,14 @@ def test_audit_leaves_a_placeholder_alone_outside_formalizable_articles(tmp_path assert "roadmap/chapter/README.md" not in _finding_map(blueprint) -def test_bundled_example_has_no_statement_text_finding(repo_root: Path) -> None: +def test_bundled_example_has_no_statement_or_unclosed_fence_finding(repo_root: Path) -> None: blueprint = repo_root / "skills" / "setup" / "assets" / "cabannes-thesis-project" / "blueprint" codes = {finding.code for finding in audit_blueprint(blueprint).findings} - assert not codes & {"missing-statement-text", "empty-statement-text", "placeholder-statement-text"} + assert not codes & { + "missing-statement-text", + "empty-statement-text", + "placeholder-statement-text", + "unclosed-code-fence", + } From 5b383e4106e3c694c824c84b993b0461019e315d Mon Sep 17 00:00:00 2001 From: 1cbyc Date: Sun, 11 Oct 2026 04:23:15 +0000 Subject: [PATCH 2/2] Address unclosed fence review feedback Co-authored-by: insisong --- autoform_cli/README.md | 11 +++++---- autoform_cli/audit.py | 15 ++++++++---- autoform_cli/markdown.py | 27 +++++++++++----------- autoform_cli/render.py | 2 +- tests/test_audit.py | 50 ++++++++++++++++++++++++++++++++++++++++ tests/test_markdown.py | 6 +++++ 6 files changed, 87 insertions(+), 24 deletions(-) diff --git a/autoform_cli/README.md b/autoform_cli/README.md index 190b8fcd1..560ab349c 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -64,8 +64,8 @@ and the published theorem box both read that span. A fence closes only on a 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 `unclosed-code-fence` before that -can corrupt the chapter. A later bare fence line of the same character and at +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 @@ -824,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 31519b63d..10ad8a852 100644 --- a/autoform_cli/audit.py +++ b/autoform_cli/audit.py @@ -28,12 +28,13 @@ ) 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 from .markdown import local_target_issue as _local_target_issue from .markdown import markdown_links as _markdown_links -from .markdown import unclosed_fence_lines as _unclosed_fence_lines from .markdown import visible_prose as _visible_prose #: More siblings than this at one level is a table of contents, not a chapter. @@ -170,14 +171,12 @@ def audit_graph( children = contained.get(node_id, ()) article = _read_article(node.path) - unclosed_fences = _unclosed_fence_lines(node.path.read_text(encoding="utf-8").splitlines()) - if unclosed_fences: - lines = ", ".join(str(line) for line in unclosed_fences) + if article.unclosed_fence is not None: findings.append( AuditFinding( article_path, "unclosed-code-fence", - f"code fence opened on line {lines} never closes", + f"code fence opened on line {article.unclosed_fence} never closes", ) ) @@ -261,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: @@ -270,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 888d2b1a7..6af444373 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,26 +656,27 @@ 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 unclosed_fence_lines(lines: list[str]) -> tuple[int, ...]: - """Return the one-based source lines of fences that never close.""" +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_fence_lines=unclosed, + unclosed_openers=unclosed, ) - return tuple(line + 1 for line in sorted(unclosed)) + return min(unclosed, default=None) def _mask_fences_and_comments( @@ -683,7 +684,7 @@ def _mask_fences_and_comments( hidden: set[int], *, unclosed_fence_is_text: bool = False, - unclosed_fence_lines: set[int] | None = None, + unclosed_openers: set[int] | None = None, ) -> list[str]: masked: list[str] = [] fence: tuple[str, int] | None = None @@ -699,8 +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_fence_lines is not None: - unclosed_fence_lines.add(opened[0]) + 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))) @@ -828,6 +829,6 @@ def _is_within(path: Path, directory: Path) -> bool: "rendered_visible_text", "site_converter", "strip_line_comments", - "unclosed_fence_lines", + "first_unclosed_fence", "visible_prose", ] diff --git a/autoform_cli/render.py b/autoform_cli/render.py index cb44c7caa..bdb08103a 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 21b3e41bb..2d720b3e0 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 @@ -882,6 +883,55 @@ def test_audit_reports_an_unclosed_code_fence(tmp_path: Path) -> None: ] +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#