Merge pull request #459 from facebookresearch/fix/454-followups

Follow up #454: Mathlib row wording, example and test pins

Author: Deicyde

autoform_cli/README.md

@@ -220,8 +220,8 @@ An article asserts only facts a human or agent verified:
 | `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. 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. |
-| `mathlib_declaration: add_comm` | Mathlib name(s) the article restates; `audit` requires one on a `mathlib: true` article. Render shows each on the article's page as text, without a link, since nothing checks it against the pinned Mathlib. |
-| `mathlib_file: Mathlib/Algebra/Group/Defs.lean` | The Mathlib file that declares it, as a portable relative path; `search` reports it. |
+| `mathlib_declaration: Nat.exists_infinite_primes` | Mathlib name(s) the article restates; `audit` requires one on a `mathlib: true` article. Render lists each in a Mathlib row of the article's statement box, as text without a link, since nothing checks it against the pinned Mathlib. |
+| `mathlib_file: Mathlib/Data/Nat/Prime/Infinite.lean` | The Mathlib file that declares the `mathlib_declaration` name(s), as a portable relative path; `search` reports it. |
 | `not_ready: true` | Needs more blueprint work before it can be attempted. |
 | `lean: Ns.decl` | Declaration name(s) that discharge the article. |
 | `discussion: 42` | Issue number or URL where the article is being discussed. |
@@ -254,7 +254,7 @@ is stated or retracted but not proved
 dependency counts together with whatever its statement prerequisites reach, and
 a proved dependency passes on
 everything it reaches. The site colours it violet, never green, and lists those
-open statements in an `Assumes` row on the article page. It is never
+open statements in an `Assumes` row of its statement box. It is never
 `fully_proved`, which keeps its meaning in both policies; a conditional result
 is complete only once every open statement it assumes is proved. The
 palette and state names follow

autoform_cli/render.py

@@ -2997,8 +2997,7 @@ def _render_environment(
     source_link = _vault_source_link(node, repo_root=repo_root, linker=linker)
     meta_rows = implementation_rows
     if mathlib_names := declaration_names(node.mathlib_declaration or ""):
-        # As text: render links only bytes it matched to a commit, and it never
-        # reads the pinned Mathlib.
+        # As text: nothing checks these names against the pinned Mathlib.
         meta_rows.append(("Mathlib", " · ".join(f"<code>{html.escape(name)}</code>" for name in mathlib_names)))
     if node_status.key == "conditional":
         # A conditional proof must never read as finished, so the open

tests/test_render.py

@@ -734,12 +734,12 @@ def test_a_mathlib_article_shows_its_mathlib_declarations_as_text(tmp_path: Path
     upstream = project / "blueprint/roadmap/upstream.md"
     upstream.write_text(article.format(names=""), encoding="utf-8")
     without = render_site(project / "blueprint", tmp_path / "without", lean_root=project)
-    upstream.write_text(article.format(names="mathlib_declaration: add_comm, «a&b»\n"), encoding="utf-8")
+    upstream.write_text(article.format(names="mathlib_declaration: add_comm, «a<b&c»\n"), encoding="utf-8")
     shown = render_site(project / "blueprint", tmp_path / "shown", lean_root=project)
 
     row = (
         '<div class="bp-row"><span class="bp-key">Mathlib</span>'
-        '<span class="bp-value"><code>add_comm</code> · <code>«a&amp;b»</code></span></div>'
+        '<span class="bp-value"><code>add_comm</code> · <code>«a&lt;b&amp;c»</code></span></div>'
     )
     page = (tmp_path / "shown/roadmap/README.md").read_text(encoding="utf-8")
     assert page.count(row) == 1
@@ -3085,6 +3085,8 @@ def test_a_conditional_proof_names_the_open_statements_it_assumes(
     for variable in ("GITHUB_REPOSITORY", "GITHUB_SERVER_URL", "GITHUB_SHA"):
         monkeypatch.delenv(variable, raising=False)
     project = _conditional_project(tmp_path, "allowed")
+    # Not mathlib: true, yet its Mathlib name is shown too.
+    _edit(project / "blueprint/roadmap/top.md", "discussion: 42\n", "discussion: 42\nmathlib_declaration: add_comm\n")
 
     render_site(project / "blueprint", tmp_path / "out", lean_root=project, repository_url="", ref="")
     page = (tmp_path / "out/roadmap/README.md").read_text(encoding="utf-8")
@@ -3099,9 +3101,9 @@ def test_a_conditional_proof_names_the_open_statements_it_assumes(
     ) in top
     # Only the conditional proof carries the row; the open statement assumes nothing.
     assert page.count('<span class="bp-key">Assumes</span>') == 1
-    # The row follows the implementation row and precedes Discussion.
+    # The row follows the Lean and Mathlib rows and precedes Discussion.
     meta = top[top.index('<div class="bp-meta">'):top.index('<details class="bp-dependencies">')]
-    assert re.findall(r'<span class="bp-key">([^<]+)</span>', meta) == ["Lean", "Assumes", "Discussion"]
+    assert re.findall(r'<span class="bp-key">([^<]+)</span>', meta) == ["Lean", "Mathlib", "Assumes", "Discussion"]
 
     css = (tmp_path / "out/stylesheets/blueprint.css").read_text(encoding="utf-8")
     assert ".bp-ref-conditional::before, .bp-swatch-conditional { background: #E9DFFC; border-color: #6B3FCF; }" in css