.asString
+ let statement := render .statement
+ let proof := render .proof
+ hasSubstr statement "Statement uses 1" &&
+ hasSubstr statement "def:graft.statement.dep" &&
+ !hasSubstr statement "def:graft.proof.dep" &&
+ hasSubstr statement "class=\"bp_extra_slot bp_extra_slot_group\"" &&
+ hasSubstr statement "class=\"bp_extra_slot bp_extra_slot_used_by\"" &&
+ hasSubstr statement "bp_code_panel_wrapper" &&
+ hasSubstr proof "Proof uses 1" &&
+ hasSubstr proof "def:graft.proof.dep" &&
+ !hasSubstr proof "def:graft.statement.dep" &&
+ !hasSubstr proof "class=\"bp_extra_slot bp_extra_slot_group\"" &&
+ !hasSubstr proof "class=\"bp_extra_slot bp_extra_slot_used_by\"" &&
+ !hasSubstr proof "bp_code_panel_wrapper"
+
+/- Manifest construction keeps statement code associations off the proof facet. -/
+/-- info: true -/
+#guard_msgs in
+#eval
+ show IO Bool from do
+ let files ← buildManualPreviewDataFiles manualImpls facetCodeProjectionDoc
+ let label := Lean.Name.mkSimple "thm:graft.facet.code"
+ let statementKey := Informal.PreviewCache.statementKey label
+ let proofKey := Informal.PreviewCache.proofKey label
+ let some statementEntry := files.manifest.previews.find? (·.key == statementKey)
+ | return false
+ let some proofEntry := files.manifest.previews.find? (·.key == proofKey)
+ | return false
+ let ctx :=
+ Informal.Graft.RenderContext.ofPreviewData? (some files.manifest) (some files.htmlCache)
+ let statementNode :=
+ (({ label := "thm:graft.facet.code" } :
+ Informal.Graft.BlueprintNodeConfig).toNode)
+ let proofNode :=
+ (({ label := "thm:graft.facet.code", facet := some "proof" } :
+ Informal.Graft.BlueprintNodeConfig).toNode)
+ let statementHtml ←
+ Informal.Graft.renderNodeFromManifestCache {} ctx statementNode
+ let proofHtml ←
+ Informal.Graft.renderNodeFromManifestCache {} ctx proofNode
+ pure <|
+ !statementEntry.leanCodePreviewKeys.isEmpty &&
+ statementEntry.codeData.isSome &&
+ proofEntry.leanCodePreviewKeys.isEmpty &&
+ proofEntry.codeData.isNone &&
+ hasSubstr statementHtml.asString "graftFacetCodeWitness" &&
+ hasSubstr statementHtml.asString "bp_code_panel_wrapper" &&
+ !hasSubstr proofHtml.asString "graftFacetCodeWitness" &&
+ !hasSubstr proofHtml.asString "bp_code_panel_wrapper"
+
private def renderAuditNode
(manifest : Informal.PreviewManifest.File)
(htmlCache : Informal.PreviewManifest.HtmlCache.File)
diff --git a/tests/VersoBlueprintTests/BlueprintImportedDuplicates/Direct.lean b/tests/VersoBlueprintTests/BlueprintImportedDuplicates/Direct.lean
index cc6e9bbc..3174f07c 100644
--- a/tests/VersoBlueprintTests/BlueprintImportedDuplicates/Direct.lean
+++ b/tests/VersoBlueprintTests/BlueprintImportedDuplicates/Direct.lean
@@ -28,7 +28,7 @@ error: Duplicate imported blueprint author id '«dup.imported.author»'
#guard_msgs in
#docs (Genre.Manual) directImportedDuplicateDoc "Direct Imported Duplicates" :=
:::::::
-{blueprint_summary}
+{blueprint_node "dup.imported.node"}
:::::::
/-- info: true -/
diff --git a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
index ef2e9efb..bbea6394 100644
--- a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
+++ b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
@@ -67,6 +67,12 @@ open Informal.PreviewManifest
let leanCodePreviewKeysDesc? := do
let leanCodePreviewKeysJson ← entryProps.get? "leanCodePreviewKeys"
leanCodePreviewKeysJson.getObjValAs? String "description" |>.toOption
+ let foldCodeBlockDesc? := do
+ let foldCodeBlockJson ← entryProps.get? "foldCodeBlock"
+ foldCodeBlockJson.getObjValAs? String "description" |>.toOption
+ let foldProofBlockDesc? := do
+ let foldProofBlockJson ← entryProps.get? "foldProofBlock"
+ foldProofBlockJson.getObjValAs? String "description" |>.toOption
let sourceLocationDesc? := do
let sourceLocationJson ← entryProps.get? "sourceLocation"
sourceLocationJson.getObjValAs? String "description" |>.toOption
@@ -119,6 +125,8 @@ open Informal.PreviewManifest
!useRefProps.contains "intents" &&
entryProps.contains "leanCodePreviewKeys" &&
entryProps.contains "codeData" &&
+ entryProps.contains "foldProofBlock" &&
+ entryProps.contains "foldCodeBlock" &&
entryProps.contains "externalMarkup" &&
entryProps.contains "sources" &&
!entryProps.contains "source" &&
@@ -137,6 +145,10 @@ open Informal.PreviewManifest
proofUsesDesc? == some "Structured proof use metadata, preserving origin and intent tags." &&
displayCaptionDesc? == some "Structured heading caption for renderers that need to lay out the title." &&
leanCodePreviewKeysDesc? == some "Manifest/cache-backed preview keys for Lean code previews associated with this entry." &&
+ foldProofBlockDesc? ==
+ some "Whether the canonical proof shell is collapsed when this is a proof entry." &&
+ foldCodeBlockDesc? ==
+ some "Whether the associated Lean code panel is collapsed for this canonical traversal entry." &&
(internalSchemaDesc?.getD "").contains "Internal generated-data schema marker" &&
sourceLocationDesc? == some "Source location lookup result for this manifest entry." &&
kindDesc? == some "Kind (definition, proposition, lemma, theorem, corollary)." &&
diff --git a/tests/browser/test_preview_runtime_regressions.py b/tests/browser/test_preview_runtime_regressions.py
index 1986cd13..9e262192 100644
--- a/tests/browser/test_preview_runtime_regressions.py
+++ b/tests/browser/test_preview_runtime_regressions.py
@@ -101,6 +101,36 @@ def test_external_declaration_docstrings_render_markdown(self, server: str, page
expect(fun_doc).to_contain_text("Adds a small preview offset")
expect(fun_doc.locator("code").first).to_contain_text("n")
+ verso_def = page.locator(
+ '[data-decl="PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition"]'
+ ).first
+ expect(verso_def).to_have_count(1)
+ verso_doc = verso_def.locator(".bp_external_decl_body > div.docstring").first
+ expect(verso_doc.locator("strong")).to_contain_text("structural external-panel docstring")
+ expect(verso_doc.locator("li")).to_have_count(2)
+ verso_math = verso_doc.locator("code.bp_math.inline").first
+ expect(verso_math).to_contain_text("6 + 1 = 7")
+ expect(verso_math).to_have_attribute("data-bp-math-rendered", "1")
+ expect(verso_math.locator(".katex")).to_have_count(1)
+ verso_display_math = verso_doc.locator("code.bp_math.display").first
+ expect(verso_display_math).to_contain_text("6 + 2 = 8")
+ expect(verso_display_math).to_have_attribute("data-bp-math-rendered", "1")
+ expect(verso_display_math.locator(".katex-display")).to_have_count(1)
+ expect(verso_def.locator(".bp_external_decl_body > pre.docstring")).to_have_count(0)
+
+ verso_structure = page.locator(
+ '[data-decl="PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure"]'
+ ).first
+ expect(verso_structure).to_have_count(1)
+ expect(verso_structure.locator(".bp_external_decl_body > div.docstring strong")).to_contain_text(
+ "structural container docstring"
+ )
+ field_doc = verso_structure.locator(".subdocs div.docstring").first
+ expect(field_doc.locator("strong")).to_contain_text("structural field docstring")
+ field_math = field_doc.locator("code.bp_math.inline").first
+ expect(field_math).to_contain_text("8 + 1 = 9")
+ expect(field_math).to_have_attribute("data-bp-math-rendered", "1")
+
decl = page.locator(
'[data-decl="PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage.ofCounterexample"]'
).first
diff --git a/tests/harness/preview_runtime_showcase/check_blueprint_code_panels.py b/tests/harness/preview_runtime_showcase/check_blueprint_code_panels.py
index 0c7fc922..2facdb10 100644
--- a/tests/harness/preview_runtime_showcase/check_blueprint_code_panels.py
+++ b/tests/harness/preview_runtime_showcase/check_blueprint_code_panels.py
@@ -285,6 +285,10 @@ def main() -> int:
fail("missing in-module documented external definition showcase declaration")
if "PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedFunction" not in code_panels:
fail("missing in-module documented external function showcase declaration")
+ if "PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition" not in code_panels:
+ fail("missing in-module Verso-docstring external definition showcase declaration")
+ if "PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure" not in code_panels:
+ fail("missing in-module Verso-docstring external structure showcase declaration")
if "PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem" not in code_panels:
fail("missing in-module external theorem showcase declaration")
if "PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedTheorem" not in code_panels:
@@ -368,6 +372,46 @@ def main() -> int:
if docstringed_defs_panel.count('data-kind="def"') < 2:
fail("documented multi-definition panel missing def kind markers")
+ verso_docstring_panel = next(
+ (
+ p
+ for p in external_panels
+ if 'data-decl="PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition"'
+ in p
+ ),
+ None,
+ )
+ if verso_docstring_panel is None:
+ fail("missing Verso-docstring external code panel")
+ if "structural external-panel docstring" not in verso_docstring_panel:
+ fail("Verso-docstring panel missing structural emphasis")
+ if '6 + 1 = 7' not in verso_docstring_panel:
+ fail("Verso-docstring panel missing structural inline mathematics")
+ if '6 + 2 = 8' not in verso_docstring_panel:
+ fail("Verso-docstring panel missing structural display mathematics")
+ if verso_docstring_panel.count("structural panel item") < 2:
+ fail("Verso-docstring panel missing structural list items")
+ if '' in verso_docstring_panel:
+ fail("Verso-docstring panel was flattened to a plain docstring")
+
+ verso_structure_panel = next(
+ (
+ p
+ for p in external_panels
+ if 'data-decl="PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure"'
+ in p
+ ),
+ None,
+ )
+ if verso_structure_panel is None:
+ fail("missing Verso-docstring external structure panel")
+ if "structural container docstring" not in verso_structure_panel:
+ fail("Verso structure panel missing structural declaration emphasis")
+ if "structural field docstring" not in verso_structure_panel:
+ fail("Verso structure panel missing structural field emphasis")
+ if '8 + 1 = 9' not in verso_structure_panel:
+ fail("Verso structure panel missing structural field mathematics")
+
theorem_docstring_panel = next(
(
p
diff --git a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CodePanels.lean b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CodePanels.lean
index 214b0d10..402b768d 100644
--- a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CodePanels.lean
+++ b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CodePanels.lean
@@ -28,6 +28,29 @@ definitions appear in the same code panel.
-/
def previewDocstringedFunction (n : Nat) : Nat := n + 1
+set_option doc.verso true in
+/--
+A *structural external-panel docstring* with inline mathematics
+$`6 + 1 = 7`.
+
+A display equation follows:
+$$`6 + 2 = 8`
+
+* First structural panel item.
+* Second structural panel item.
+-/
+def previewVersoDocstringedDefinition : Nat := 7
+
+set_option doc.verso true in
+/--
+A *structural container docstring* for a field-docstring regression.
+-/
+structure PreviewVersoDocstringedStructure where
+ /--
+ A *structural field docstring* with inline mathematics $`8 + 1 = 9`.
+ -/
+ value : Nat
+
theorem previewExternalTheorem : True := by
trivial
@@ -303,3 +326,11 @@ class PanelInlineMixedFold (α : Type) where
:::definition "panel_no_code"
Statement without associated Lean code.
:::
+
+:::definition "panel_external_verso_docstring" (lean := "PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition")
+External definition panel sample with a structural Verso docstring.
+:::
+
+:::definition "panel_external_verso_structure_docstring" (lean := "PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure")
+External structure panel sample with structural declaration and field docstrings.
+:::