From 3fe368e8e7f4b4f25b849bf4915b234f96b73868 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 2 Dec 2025 20:16:35 +0100
Subject: [PATCH] feat: allow Verso docstrings to suppose the existence of
 instances (#11476)

This PR adds a `` {givenInstance}`C` `` documentation role that adds an
instance of `C` to the document's local assumptions.
---
 src/Lean/Elab/DocString.lean         | 22 ++++---
 src/Lean/Elab/DocString/Builtin.lean | 93 +++++++++++++++++++++++++++-
 stage0/src/stdlib_flags.h            |  2 +
 tests/lean/run/versoDocMarkdown.lean | 27 ++++++++
 tests/lean/run/versoDocs.lean        |  6 ++
 5 files changed, 141 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 9b1b2df00c..eb3dc23c53 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@@ -86,6 +86,9 @@ structure State where
   -/
   lctx : LocalContext
   /--
+  -/
+  localInstances : LocalInstances
+  /--
   The options.
 
   The `MonadLift TermElabM DocM` instance runs the lifted action with these options, so elaboration
@@ -129,10 +132,10 @@ instance : MonadStateOf State DocM :=
 
 instance : MonadLift TermElabM DocM where
   monadLift act := private DocM.mk fun _ _ st' => do
-    let {openDecls, lctx, options, ..} := (← st'.get)
+    let {openDecls, lctx, options, localInstances, ..} := (← st'.get)
     let v ←
       withTheReader Core.Context (fun ρ => { ρ with openDecls, options }) <|
-      withTheReader Meta.Context (fun ρ => { ρ with lctx }) <|
+      withTheReader Meta.Context (fun ρ => { ρ with lctx, localInstances }) <|
       act
     return v
 
@@ -144,16 +147,19 @@ private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDoc
   registerEnvExtension (pure none)
 
 private def getModState
-    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
+    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLiftT MetaM m] [MonadLCtx m]
     [MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
   if let some st := modDocstringStateExt.getState (← getEnv) then
     return st
   else
-    let lctx ← getLCtx
-    let openDecls ← getOpenDecls
-    let options ← getOptions
     let scopes := [{header := "", isPublic := true}]
-    let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
+    let openDecls ← getOpenDecls
+    let lctx ← getLCtx
+    let localInstances ← Meta.getLocalInstances
+    let options ← getOptions
+    let scopedExts := #[]
+    let st : ModuleDocstringState :=
+      { scopes, openDecls, lctx, localInstances, options, scopedExts }
     modifyEnv fun env =>
       modDocstringStateExt.setState env st
     return st
@@ -197,7 +203,7 @@ def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
       let options ← getOptions
       let scopes := [{header := "", isPublic := true}]
       let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
-        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
+        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, localInstances, options }
       pure v
     finally
       scopedEnvExtensionsRef.set sc
diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean
index 98f4a2a21e..71ba171c0e 100644
--- a/src/Lean/Elab/DocString/Builtin.lean
+++ b/src/Lean/Elab/DocString/Builtin.lean
@@ -522,7 +522,6 @@ private def givenContents : ParserFn :=
        optionalFn (symbolFn ":" >> termParser.fn)))
     (symbolFn ",")
 
-
 /--
 A metavariable to be discussed in the remainder of the docstring.
 
@@ -612,6 +611,98 @@ def given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : f
         |> Inline.concat
   else return .empty
 
+private def givenInstanceContents : ParserFn :=
+  whitespace >>
+  sepBy1Fn false
+    (nodeFn nullKind
+     (optionalFn (atomicFn (identFn >> symbolFn ":")) >>
+       termParser.fn))
+    (symbolFn ",")
+
+/--
+An instance metavariable to be discussed in the remainder of the docstring.
+
+This is similar to {given}, but the resulting variable is marked for instance synthesis
+(with `BinderInfo.instImplicit`), and the name is optional.
+
+There are two syntaxes that can be used:
+ * `` {givenInstance}`T` `` establishes an unnamed instance of type `T`.
+ * `` {givenInstance}`x : T` `` establishes a named instance `x` of type `T`.
+
+Additionally, the contents of the code literal can be repeated, with comma separators.
+
+If the `show` flag is `false` (default `true`), then the instance is not shown in the docstring.
+-/
+@[builtin_doc_role]
+def givenInstance («show» : flag true) (xs : TSyntaxArray `inline) :
+    DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+
+  let stxs ← parseStrLit givenInstanceContents s
+  let stxs := stxs.getArgs.mapIdx Prod.mk |>.filterMap fun (n, s) =>
+    if n % 2 = 0 then some s else none
+  let mut lctx ← getLCtx
+  let mut localInstances ← Meta.getLocalInstances
+  let mut instCounter := 0
+  for stx in stxs do
+    let nameColonOpt := stx[0][0]
+    let tyStx := stx[1]
+
+    let ty' : Expr ← elabType tyStx
+    let class? ← Meta.isClass? ty'
+    let some className := class?
+      | throwError m!"Expected a type class, but got `{.ofExpr ty'}`"
+
+    -- Generate a fresh name if no name is provided
+    let (userName, hasUserName) ←
+      if nameColonOpt.isMissing then
+        instCounter := instCounter + 1
+        let n ← mkFreshUserName (`inst ++ className)
+        pure (n, false)
+      else
+        pure (nameColonOpt.getId, true)
+
+    let fv ← mkFreshFVarId
+    lctx := lctx.mkLocalDecl fv userName ty' BinderInfo.instImplicit
+    localInstances := localInstances.push { fvar := .fvar fv, className }
+
+    if hasUserName then
+      addTermInfo' nameColonOpt[0] (.fvar fv)
+        (lctx? := some lctx) (isBinder := true) (expectedType? := some ty')
+
+  modify fun st => { st with lctx, localInstances }
+
+  if «show» then
+    let text ← getFileMap
+    let mut outStrs := #[]
+    let mut failed := false
+    for stx in stxs do
+      let nameColonOpt := stx[0][0]
+      let thisStr ←
+        if let some ⟨b', e'⟩ := stx[1].getRange? then
+          -- Has type annotation
+          if nameColonOpt.isMissing then
+            -- No name, just show type
+            pure <| String.Pos.Raw.extract text.source b' e'
+          else
+            -- Has name and type, nameColonOpt is `identFn >> symbolFn ":"`
+            if let some ⟨b, e⟩ := nameColonOpt[0].getRange? then
+              pure <| s!"{b.extract text.source e} : {b'.extract text.source e'}"
+            else
+              failed := true
+              break
+        else
+          failed := true
+          break
+      outStrs := outStrs.push thisStr
+    if failed then
+      return .code s.getString
+    else
+      return outStrs.map Inline.code
+        |>.toList |>.intersperse (Inline.text ", ") |>.toArray
+        |> Inline.concat
+  else return .empty
+
 
 private def firstToken? (stx : Syntax) : Option Syntax :=
   stx.find? fun
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..0b833d9dc4 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/versoDocMarkdown.lean b/tests/lean/run/versoDocMarkdown.lean
index 893759e415..13bf5a480d 100644
--- a/tests/lean/run/versoDocMarkdown.lean
+++ b/tests/lean/run/versoDocMarkdown.lean
@@ -133,6 +133,7 @@ Lean.Doc.assert'
 Lean.Doc.attr
 Lean.Doc.conv
 Lean.Doc.given
+Lean.Doc.givenInstance
 Lean.Doc.kw
 Lean.Doc.kw!
 Lean.Doc.kw?
@@ -190,6 +191,32 @@ Visible:
 -/
 def givenTests (x y : Nat) : Nat := x - y
 
+/--
+{given -show}`α : Type, β : Type, γ : Type` {given -show}`x : α, y : α, z : α`
+Invisible: {givenInstance -show}`Add α` {givenInstance -show}`addInst : Add β`
+
+There is an {lean}`addInst : Add β` and an {lean}`inferInstance : Add α`, and {lean}`x + y + z`.
+
+Visible: {givenInstance}`Add γ`&{givenInstance}`addInst : OfNat γ 5`
+
+Check: {lean}`(5 : γ) + 5`
+
+-/
+def givenInstanceTests (x y : Nat) : Nat := x - y
+
+/--
+info:  ⏎
+Invisible:  ⏎
+
+There is an `addInst : Add β` and an `inferInstance : Add α`, and `x + y + z`\.
+
+Visible: `Add γ`&`addInst : OfNat γ 5`
+
+Check: `(5 : γ) + 5`
+-/
+#guard_msgs in
+#verso_to_markdown givenInstanceTests
+
 /--
 info: Invisible: ⏎
 
diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean
index c2f78fcfba..d59a4ceac9 100644
--- a/tests/lean/run/versoDocs.lean
+++ b/tests/lean/run/versoDocs.lean
@@ -96,6 +96,12 @@ def rot (n : Nat) (xs : Array α) : Array α :=
 #eval rot 5 #[1, 2, 3]
 
 
+/--
+Given {given}`α : Type` and {given}`x : α, y : α` with an instance of {givenInstance}`Add α`,
+{lean}`x + y : α`.
+-/
+def givens := ()
+
 /--
 Given {given}`xs : List α`, finds lists {given}`ys` and {given}`zs` such that {lean}`xs = ys ++ zs`
 and {lean}`∀x ∈ xs, p x` and {lean}`zs.head?.all (¬p ·)`.