From 4a3401f69a5fd3d247943df1ab7a78e56566bc8a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 23 Jan 2026 15:02:11 +0100 Subject: [PATCH] fix: enable Verso docstrings in `where`-blocks (#12122) This PR adds support for Verso docstrings in `where` clauses. Closes #12066. --- src/Lean/Elab/LetRec.lean | 17 ++++-- src/Lean/Elab/MutualDef.lean | 4 +- src/Lean/Elab/Term/TermElabM.lean | 5 ++ tests/lean/run/versoDocsWhere.lean | 90 ++++++++++++++++++++++++++++++ 4 files changed, 109 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/versoDocsWhere.lean diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 1e8a613859..08a470ce2b 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -20,10 +20,12 @@ structure LetRecDeclView where declName : Name parentName? : Option Name binderIds : Array Syntax + binders : Syntax -- binder syntax for docstring elaboration type : Expr mvar : Expr -- auxiliary metavariable used to lift the 'let rec' valStx : Syntax termination : TerminationHints + docString? : Option (TSyntax ``Parser.Command.docComment × Bool) := none structure LetRecView where decls : Array LetRecDeclView @@ -32,8 +34,9 @@ structure LetRecView where /- group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do let mut decls : Array LetRecDeclView := #[] + let isVerso := doc.verso.get (← getOptions) for attrDeclStx in letRec[1][0].getSepArgs do - let docStr? := attrDeclStx[0].getOptional?.map TSyntax.mk + let docStr? := attrDeclStx[0].getOptional?.map (TSyntax.mk ·, isVerso) let attrOptStx := attrDeclStx[1] let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0] let decl := attrDeclStx[2][0] @@ -49,12 +52,14 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do if decls.any fun decl => decl.declName == declName then withRef declId do throwError "`{.ofConstName declName}` has already been declared" - let binders := decl[1] + let binderStx := decl[1] checkNotAlreadyDeclared declName applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration - addDocString' declName binders docStr? + -- Docstring processing is deferred until the declaration is added to the environment. + -- This is necessary for Verso docstrings to work correctly, as they may reference the + -- declaration being defined. addDeclarationRangesFromSyntax declName decl declId - let binders := binders.getArgs + let binders := binderStx.getArgs let typeStx := expandOptType declId decl[2] let (type, binderIds) ← elabBindersEx binders fun xs => do let type ← elabType typeStx @@ -70,7 +75,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do let termination ← elabTerminationHints ⟨attrDeclStx[3]⟩ decls := decls.push { ref := declId, attrs, shortDeclName, declName, parentName?, - binderIds, type, mvar, valStx, termination + binderIds, binders := binderStx, type, mvar, valStx, termination, docString? := docStr? } else throwUnsupportedSyntax @@ -127,6 +132,8 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array val := value mvarId := view.mvar.mvarId! termination + binders := view.binders + docString? := view.docString? } modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift } diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 34f0863596..8e12b0ae9c 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1092,8 +1092,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo ref := c.ref declName := c.toLift.declName levelParams := [] -- we set it later - binders := mkNullNode -- No docstrings, so we don't need these - modifiers := { modifiers with attrs := c.toLift.attrs } + binders := c.toLift.binders + modifiers := { modifiers with attrs := c.toLift.attrs, docString? := c.toLift.docString? } kind, type, value, termination := c.toLift.termination } diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index f6f80e2030..b0dbe4326c 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -167,6 +167,11 @@ structure LetRecToLift where val : Expr mvarId : MVarId termination : TerminationHints + /-- The binders syntax for the declaration, used for docstring elaboration. -/ + binders : Syntax := .missing + /-- The docstring, if present, and whether it's Verso. Docstring processing is deferred until the + declaration is added to the environment (needed for Verso docstrings to work). -/ + docString? : Option (TSyntax ``Lean.Parser.Command.docComment × Bool) := none deriving Inhabited /-- diff --git a/tests/lean/run/versoDocsWhere.lean b/tests/lean/run/versoDocsWhere.lean new file mode 100644 index 0000000000..0192d3f4db --- /dev/null +++ b/tests/lean/run/versoDocsWhere.lean @@ -0,0 +1,90 @@ +import Lean +/-! +# Verso Docstrings on `where`-clause declarations + +This test checks that Verso docstrings work correctly on declarations in a `where` clause. + +-/ + +section + +open Lean Elab Command + +deriving instance Repr for VersoDocString + +def printVersoDocstring (x : Name) : CommandElabM Unit := do + let docs? ← findInternalDocString? (← getEnv) x + match docs? with + | none => throwError m!"No docstring for {.ofConstName x}" + | some (.inl md) => throwError m!"Only a Markdown docstring for {.ofConstName x}:\n{md}" + | some (.inr v) => IO.println (repr v) + +end + +set_option doc.verso true + +/-- This docstring works. -/ +def foo := bar + where + /-- This docstring should also work. -/ + bar := 37 + +-- Verify the docstrings are present +/-- +info: { text := #[Lean.Doc.Block.para #[Lean.Doc.Inline.text "This docstring works. "]], subsections := #[] } +-/ +#guard_msgs in +#eval printVersoDocstring ``foo + +/-- +info: { text := #[Lean.Doc.Block.para #[Lean.Doc.Inline.text "This docstring should also work. "]], subsections := #[] } +-/ +#guard_msgs in +#eval printVersoDocstring ``foo.bar + + +-- Test with multiple where declarations +/-- Outer function. -/ +def outer := inner1 + inner2 + where + /-- First inner function. -/ + inner1 := 10 + /-- Second inner function is {lean}`outer.inner2`. -/ + inner2 := 20 + +/-- +info: { text := #[Lean.Doc.Block.para #[Lean.Doc.Inline.text "First inner function. "]], subsections := #[] } +-/ +#guard_msgs in +#eval printVersoDocstring ``outer.inner1 + +/-- +info: { text := #[Lean.Doc.Block.para + #[Lean.Doc.Inline.text "Second inner function is ", + Lean.Doc.Inline.other + { name := `Lean.Doc.Data.LeanTerm val := Dynamic.mk `Lean.Doc.Data.LeanTerm _ } + #[Lean.Doc.Inline.code "outer.inner2"], + Lean.Doc.Inline.text ". "]], + subsections := #[] } +-/ +#guard_msgs in +#eval printVersoDocstring ``outer.inner2 + + +/-- Function with type annotation. -/ +def withType := helper + where + /-- What is the type of {name (full := withType.helper)}`helper`?. -/ + helper : Nat := 42 + +/-- +info: { text := #[Lean.Doc.Block.para + #[Lean.Doc.Inline.text "What is the type of ", + Lean.Doc.Inline.other + { name := `Lean.Doc.Data.Const val := Dynamic.mk `Lean.Doc.Data.Const _ } + #[Lean.Doc.Inline.code "helper"], + Lean.Doc.Inline.text "?. "]], + subsections := #[] } +-/ +#guard_msgs in +#eval printVersoDocstring ``withType.helper