feat: Verso and Shake (#10657)

This PR ensures Shake does not remove any imports required by Verso
docstrings

src/Lean/Elab/DocString.lean

@@ -1604,10 +1604,12 @@ private def warnUnusedRefs : DocM Unit := do
 /-- Elaborates a sequence of blocks into a document. -/
 public def elabBlocks (blocks : TSyntaxArray `block) :
     DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
-  let (v, _) ← elabBlocks' 0 |>.run blocks
-  let res ← fixupBlocks v
-  warnUnusedRefs
-  return res
+  -- Users should not need to make import needed for embedded terms public
+  withoutExporting do
+    let (v, _) ← elabBlocks' 0 |>.run blocks
+    let res ← fixupBlocks v
+    warnUnusedRefs
+    return res
 
 /-- Elaborates a sequence of blocks into a module doc snippet. -/
 public def elabModSnippet

src/Lean/Elab/DocString/Builtin.lean

@@ -35,6 +35,16 @@ set_option linter.missingDocs true
 
 public section
 
+/--
+As elaboration results are not added to the environment as part of constants, manually record
+references so that `shake` keeps their imports.
+-/
+private def elabExtraTerm (stx : Syntax) (expectedType? : Option Expr := none) : TermElabM Expr := do
+  let e ← elabTermAndSynthesize stx expectedType?
+  for c in e.getUsedConstants do
+    recordExtraModUseFromDecl (isMeta := false) c
+  return e
+
 /-- Create an identifier while directly copying info -/
 private def mkIdentFrom' (src : Syntax) (val : Name) : Ident :=
   ⟨Syntax.ident src.getHeadInfo (toString val).toSubstring val []⟩
@@ -578,7 +588,7 @@ def given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : f
     let val : Option Expr ← do
       let valStx := stx[1][1]
       if valStx.isMissing then pure none
-      else some <$> elabTerm valStx (some ty')
+      else some <$> elabExtraTerm valStx (some ty')
     let fv ← mkFreshFVarId
     lctx :=
       if let some v := val then
@@ -955,7 +965,7 @@ def leanRole (type : Option StrLit := none) (xs : TSyntaxArray `inline) : DocM (
         if let some t := type then
           logErrorAt t m!"Ignoring `{s.getString}` in favor of type provided after colon"
         some <$> elabType stx[1][1]
-    withoutErrToSorry <| discard <| elabTerm stx[0] ty?
+    withoutErrToSorry <| discard <| elabExtraTerm stx[0] ty?
   let trees := (← getInfoTrees)
   if h : trees.size > 0 then
     let tree := trees[trees.size - 1]
@@ -978,7 +988,7 @@ def leanTerm (code : StrLit) : DocM (Block ElabInline ElabBlock) := do
         pure none
       else -- type after colon
         some <$> elabType stx[1][1]
-    withoutErrToSorry <| discard <| elabTerm stx[0] ty?
+    withoutErrToSorry <| discard <| elabExtraTerm stx[0] ty?
   -- The last info tree is the one we want
   let trees := (← getInfoTrees)
   if h : trees.size > 0 then
@@ -1086,8 +1096,8 @@ def assert' (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
       pure none
     else -- type after colon
       some <$> elabType stx[3][1]
-  let lhs ← elabTerm stx[0] ty?
-  let rhs ← elabTerm stx[2] ty?
+  let lhs ← elabExtraTerm stx[0] ty?
+  let rhs ← elabExtraTerm stx[2] ty?
   unless ← Meta.withTransparency .all <| Meta.isDefEq lhs rhs do
     throwErrorAt stx m!"Expected {lhs} = {rhs}, which is {← Meta.whnf lhs} = {← Meta.whnf rhs}, reducing to {← Meta.reduceAll lhs} = {← Meta.reduceAll rhs} but they are not equal."
   pure (.code s.getString)
@@ -1208,7 +1218,7 @@ def suggestLean (code : StrLit) : DocM (Array CodeSuggestion) := do
         withoutErrToSorry <|
         if stx[1][1].isMissing then pure none
         else some <$> elabType stx[1][1]
-      let tm ← withoutErrToSorry <| elabTerm stx[0] ty?
+      let tm ← withoutErrToSorry <| elabExtraTerm stx[0] ty?
     return #[.mk ``lean none none]
 
   catch | _ => return #[]
@@ -1227,7 +1237,7 @@ def suggestLeanTermBlock (code : StrLit) : DocM (Array CodeBlockSuggestion) := d
         withoutErrToSorry <|
         if stx[1][1].isMissing then pure none
         else some <$> elabType stx[1][1]
-      discard <| withoutErrToSorry <| elabTerm stx[0] ty?
+      discard <| withoutErrToSorry <| elabExtraTerm stx[0] ty?
     return #[.mk ``leanTerm none none]
   catch | _ => return #[]
 

tests/lean/run/versoDocs.lean

@@ -123,7 +123,8 @@ To prove that a relation {name}`P` holds universally for the natural numbers (th
 
 : Inductive step
 
-  {lean}`P` relates non-zero {given}`m` to {given}`n` if it relates {lean}`n % m` to {lean}`m`.
+  {lean}`P` relates non-zero {given (type :="Nat")}`m` to {given}`n` if it relates {lean}`n % m` to
+  {lean}`m`.
 
 This follows the computational behavior of {name}`gcd`.
 -/