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

@@ -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 }
 

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
     }

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
 
 /--

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