From 9d9dd3144c286e416568348bb9536fb1ed18e6f4 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 7 Sep 2026 15:53:17 +0200 Subject: [PATCH 1/3] fix: don't treat the expected messages of `#guard_msgs` as a docstring The doc comment in `#guard_msgs in` holds the messages that the wrapped command is expected to produce. It was attributed to the declaration in that command, which then had two docstring items, and `verso-html` failed with "Duplicate document ID". Only the wrapped command is now searched for docstrings. --- src/verso-literate/VersoLiterateMain.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/verso-literate/VersoLiterateMain.lean b/src/verso-literate/VersoLiterateMain.lean index 17a51764f..a6c705a46 100644 --- a/src/verso-literate/VersoLiterateMain.lean +++ b/src/verso-literate/VersoLiterateMain.lean @@ -144,7 +144,11 @@ def findHighestM [Monad m] (stx : Syntax) (fn : Syntax → Option α) : m (Array Finds the definition sites of each constant in an info tree, and replaces each docstring with a reference to the definition for later substitution. -/ -def findDocstringDefs (stx : Syntax) (t : InfoTree) : TermElabM Syntax := do +partial def findDocstringDefs (stx : Syntax) (t : InfoTree) : TermElabM Syntax := do + -- `#guard_msgs` takes the messages it expects as a doc comment, which documents nothing: it must + -- not be attached to the declaration in the command that `#guard_msgs` wraps. + if stx.isOfKind ``Lean.guardMsgsCmd then + return stx.setArg 4 (← findDocstringDefs stx[4] t) -- Find the definition sites of all constants in this info tree let defSites := t.deepestNodes fun _ i _ => match i with From 1b5f5536efa98b018413fd51fb3ecc6fb2dd6cb3 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 7 Sep 2026 16:59:13 +0200 Subject: [PATCH 2/3] test: a `#guard_msgs` comment is not the guarded declaration's docstring Adds `LitConfig.GuardMsgs` to the literate-config test project, with a theorem that has a docstring and is wrapped in `#guard_msgs in`, and a literate HTML test checking that the theorem's docstring is rendered exactly once and that the expected-messages comment is kept as prose. Without the preceding fix, the comment was attributed to the theorem as a second docstring: the page showed the docstring twice, the expected messages were gone, and `verso-literate-html` failed with "Duplicate document ID". --- src/tests/Tests/LiterateHtml.lean | 18 +++++++++++++++++- test-projects/literate-config/LitConfig.lean | 1 + .../literate-config/LitConfig/GuardMsgs.lean | 11 +++++++++++ 3 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 test-projects/literate-config/LitConfig/GuardMsgs.lean diff --git a/src/tests/Tests/LiterateHtml.lean b/src/tests/Tests/LiterateHtml.lean index 39eb49e01..14f5d600d 100644 --- a/src/tests/Tests/LiterateHtml.lean +++ b/src/tests/Tests/LiterateHtml.lean @@ -305,6 +305,21 @@ private def testUnknownExtensionFallback : IO Unit := do unless hasSubstring html "THIS IS THE FALLBACK" do throw <| IO.userError "HTML missing 'THIS IS THE FALLBACK' marker. The conversion's fallback children were not rendered." +/-- +The doc comment of `#guard_msgs` holds the messages expected from the command that it wraps. It must +not be attributed to the declaration in that command as a second docstring. +-/ +private def testGuardMsgsDocstring (data : TestData) : IO Unit := withTestDir data fun jsonDir htmlDir _ _ => do + runLiterateHtml jsonDir htmlDir + let html ← IO.FS.readFile (htmlDir / "LitConfig" / "GuardMsgs" / "index.html") + let docstring := "A theorem whose proof is left open." + let occurrences := (html.splitOn docstring).length - 1 + unless occurrences == 1 do + throw <| IO.userError s!"Expected the docstring of `guarded` once in the HTML, found it {occurrences} times. \ + The expected-messages comment of `#guard_msgs` was attributed to `guarded` as a docstring." + unless hasSubstring html "declaration uses" do + throw <| IO.userError "The expected-messages comment of `#guard_msgs` is missing from the HTML." + /-- Excluded modules produce no HTML output and are absent from the navbar. -/ private def testExclude (data : TestData) : IO Unit := withTestDir data fun jsonDir htmlDir planFile tomlFile => do IO.FS.writeFile tomlFile "exclude = [\"LitConfig.NoDocstrings\"]\n" @@ -1208,13 +1223,14 @@ private def htmlTests (data : TestData) (projectDir : System.FilePath) : List (S ("all built-in doc roles", testAllBuiltinDocRoles data), ("custom literate handlers", testCustomLiterateHandlers data), ("docstring code block messages", testDocstringCodeBlockMessages data), + ("guard_msgs docstring", testGuardMsgsDocstring data), ("unknown extension fallback", testUnknownExtensionFallback) ] def testLiterateHtml : IO Unit := do IO.println "Running literate HTML tests..." let projectDir := "test-projects/literate-config" - let modules := #["LitConfig", "LitConfig.Core", "LitConfig.Core.Basic", "LitConfig.NoDocstrings", "LitConfig.Builtins", "LitConfig.UserExt"] + let modules := #["LitConfig", "LitConfig.Core", "LitConfig.Core.Basic", "LitConfig.NoDocstrings", "LitConfig.Builtins", "LitConfig.UserExt", "LitConfig.GuardMsgs"] -- First verify test project toolchain matches root toolchain let rootToolchain := (← IO.FS.readFile "lean-toolchain").trimAscii diff --git a/test-projects/literate-config/LitConfig.lean b/test-projects/literate-config/LitConfig.lean index 10705c9f2..819670f8f 100644 --- a/test-projects/literate-config/LitConfig.lean +++ b/test-projects/literate-config/LitConfig.lean @@ -3,6 +3,7 @@ import LitConfig.NoDocstrings import LitConfig.Builtins import LitConfig.UserExt import LitConfig.Gallery +import LitConfig.GuardMsgs import Verso /-! diff --git a/test-projects/literate-config/LitConfig/GuardMsgs.lean b/test-projects/literate-config/LitConfig/GuardMsgs.lean new file mode 100644 index 000000000..a8e4d48ec --- /dev/null +++ b/test-projects/literate-config/LitConfig/GuardMsgs.lean @@ -0,0 +1,11 @@ +/-! +# Guarded Messages + +{lit}`#guard_msgs` takes the messages that it expects as a doc comment. That comment documents +nothing, so the declaration in the guarded command keeps its own docstring, and only that. +-/ + +/-- warning: declaration uses `sorry` -/ +#guard_msgs in +/-- A theorem whose proof is left open. -/ +theorem guarded : 1 + 1 = 2 := sorry From 4db453c51dce6829a078f51c61c263b07da89614 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 28 Sep 2026 12:05:08 +0200 Subject: [PATCH 3/3] chore: rephrase comments and docstrings --- src/tests/Tests/LiterateHtml.lean | 5 +++-- src/verso-literate/VersoLiterateMain.lean | 5 +++-- test-projects/literate-config/LitConfig/GuardMsgs.lean | 4 ++-- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/tests/Tests/LiterateHtml.lean b/src/tests/Tests/LiterateHtml.lean index 14f5d600d..6b531cc3e 100644 --- a/src/tests/Tests/LiterateHtml.lean +++ b/src/tests/Tests/LiterateHtml.lean @@ -306,8 +306,9 @@ private def testUnknownExtensionFallback : IO Unit := do throw <| IO.userError "HTML missing 'THIS IS THE FALLBACK' marker. The conversion's fallback children were not rendered." /-- -The doc comment of `#guard_msgs` holds the messages expected from the command that it wraps. It must -not be attributed to the declaration in that command as a second docstring. +The doc comment on a `#guard_msgs` command is not documentation. Instead, it is a specification of +the expected messages from the wrapped command. It must not be attributed to the declaration in that +command as a second docstring. -/ private def testGuardMsgsDocstring (data : TestData) : IO Unit := withTestDir data fun jsonDir htmlDir _ _ => do runLiterateHtml jsonDir htmlDir diff --git a/src/verso-literate/VersoLiterateMain.lean b/src/verso-literate/VersoLiterateMain.lean index a6c705a46..0f349c96a 100644 --- a/src/verso-literate/VersoLiterateMain.lean +++ b/src/verso-literate/VersoLiterateMain.lean @@ -145,8 +145,9 @@ Finds the definition sites of each constant in an info tree, and replaces each d reference to the definition for later substitution. -/ partial def findDocstringDefs (stx : Syntax) (t : InfoTree) : TermElabM Syntax := do - -- `#guard_msgs` takes the messages it expects as a doc comment, which documents nothing: it must - -- not be attached to the declaration in the command that `#guard_msgs` wraps. + -- `#guard_msgs` takes the messages it expects as a doc comment, but it's not really + -- documentation. It must not be attached to the declaration in the command that `#guard_msgs` + -- wraps. if stx.isOfKind ``Lean.guardMsgsCmd then return stx.setArg 4 (← findDocstringDefs stx[4] t) -- Find the definition sites of all constants in this info tree diff --git a/test-projects/literate-config/LitConfig/GuardMsgs.lean b/test-projects/literate-config/LitConfig/GuardMsgs.lean index a8e4d48ec..c1e408371 100644 --- a/test-projects/literate-config/LitConfig/GuardMsgs.lean +++ b/test-projects/literate-config/LitConfig/GuardMsgs.lean @@ -1,8 +1,8 @@ /-! # Guarded Messages -{lit}`#guard_msgs` takes the messages that it expects as a doc comment. That comment documents -nothing, so the declaration in the guarded command keeps its own docstring, and only that. +{lit}`#guard_msgs` takes the messages that it expects as a doc comment. That comment is not really +documentation, so the declaration in the guarded command keeps its own docstring, and only that. -/ /-- warning: declaration uses `sorry` -/