chore: bump to nightly-2026-03-11 (#799)

Author: david-christiansen

Manual/BuildTools/Lake/Config.lean

@@ -188,7 +188,7 @@ name = "example-package"
       readmeFile := FilePath.mk "README.md",
       reservoir := true,
       enableArtifactCache? := none,
-      restoreAllArtifacts := false,
+      restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
       allowImportAll := false},
   configFile := FilePath.mk "lakefile",
@@ -276,7 +276,7 @@ name = "Sorting"
       readmeFile := FilePath.mk "README.md",
       reservoir := true,
       enableArtifactCache? := none,
-      restoreAllArtifacts := false,
+      restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
       allowImportAll := false},
   configFile := FilePath.mk "lakefile",

Manual/Classes/InstanceSynth.lean

@@ -102,43 +102,43 @@ IF THE LEAN OUTPUT BELOW CHANGES, IT MAY ALSO BE NECESSARY TO UPDATE THE NARRATI
 ```
 ```leanOutput trace (expandTrace := Meta.synthInstance) (expandTrace := Meta.synthInstance.apply) (expandTrace := Meta.synthInstance.resume)
 [Meta.synthInstance] ✅️ Nonempty (Sum Nat Empty)
-  [Meta.synthInstance] new goal Nonempty (Sum Nat Empty)
+  [Meta.synthInstance] ✅️ new goal Nonempty (Sum Nat Empty)
     [Meta.synthInstance.instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad, @Sum.nonemptyLeft, @Sum.nonemptyRight]
   [Meta.synthInstance.apply] ✅️ apply @Sum.nonemptyRight to Nonempty (Sum Nat Empty)
     [Meta.synthInstance.tryResolve] ✅️ Nonempty (Sum Nat Empty) ≟ Nonempty (Sum Nat Empty)
-    [Meta.synthInstance] new goal Nonempty Empty
+    [Meta.synthInstance] ✅️ new goal Nonempty Empty
       [Meta.synthInstance.instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad]
   [Meta.synthInstance.apply] ❌️ apply @instNonemptyOfMonad to Nonempty Empty
     [Meta.synthInstance.tryResolve] ❌️ Nonempty Empty ≟ Nonempty (?m.5 ?m.6)
   [Meta.synthInstance.apply] ✅️ apply @instNonemptyOfInhabited to Nonempty Empty
     [Meta.synthInstance.tryResolve] ✅️ Nonempty Empty ≟ Nonempty Empty
-    [Meta.synthInstance] new goal Inhabited Empty
+    [Meta.synthInstance] ✅️ new goal Inhabited Empty
       [Meta.synthInstance.instances] #[@instInhabitedOfMonad, @Lake.inhabitedOfNilTrace, @instInhabitedOfApplicative_manual]
   [Meta.synthInstance.apply] ❌️ apply @instInhabitedOfApplicative_manual to Inhabited Empty
     [Meta.synthInstance.tryResolve] ❌️ Inhabited Empty ≟ Inhabited (?m.8 ?m.7)
   [Meta.synthInstance.apply] ✅️ apply @Lake.inhabitedOfNilTrace to Inhabited Empty
     [Meta.synthInstance.tryResolve] ✅️ Inhabited Empty ≟ Inhabited Empty
-    [Meta.synthInstance] no instances for Lake.NilTrace Empty
+    [Meta.synthInstance] ✅️ no instances for Lake.NilTrace Empty
       [Meta.synthInstance.instances] #[]
   [Meta.synthInstance.apply] ❌️ apply @instInhabitedOfMonad to Inhabited Empty
     [Meta.synthInstance.tryResolve] ❌️ Inhabited Empty ≟ Inhabited (?m.8 ?m.7)
   [Meta.synthInstance.apply] ✅️ apply @Sum.nonemptyLeft to Nonempty (Sum Nat Empty)
     [Meta.synthInstance.tryResolve] ✅️ Nonempty (Sum Nat Empty) ≟ Nonempty (Sum Nat Empty)
-    [Meta.synthInstance] new goal Nonempty Nat
+    [Meta.synthInstance] ✅️ new goal Nonempty Nat
       [Meta.synthInstance.instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad]
   [Meta.synthInstance.apply] ❌️ apply @instNonemptyOfMonad to Nonempty Nat
     [Meta.synthInstance.tryResolve] ❌️ Nonempty Nat ≟ Nonempty (?m.5 ?m.6)
   [Meta.synthInstance.apply] ✅️ apply @instNonemptyOfInhabited to Nonempty Nat
     [Meta.synthInstance.tryResolve] ✅️ Nonempty Nat ≟ Nonempty Nat
-    [Meta.synthInstance] new goal Inhabited Nat
+    [Meta.synthInstance] ✅️ new goal Inhabited Nat
       [Meta.synthInstance.instances] #[@instInhabitedOfMonad, @Lake.inhabitedOfNilTrace, @instInhabitedOfApplicative_manual, instInhabitedNat]
   [Meta.synthInstance.apply] ✅️ apply instInhabitedNat to Inhabited Nat
     [Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat
     [Meta.synthInstance.answer] ✅️ Inhabited Nat
-  [Meta.synthInstance.resume] propagating Inhabited Nat to subgoal Inhabited Nat of Nonempty Nat
+  [Meta.synthInstance.resume] ✅️ propagating Inhabited Nat to subgoal Inhabited Nat of Nonempty Nat
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.answer] ✅️ Nonempty Nat
-  [Meta.synthInstance.resume] propagating Nonempty Nat to subgoal Nonempty Nat of Nonempty (Sum Nat Empty)
+  [Meta.synthInstance.resume] ✅️ propagating Nonempty Nat to subgoal Nonempty Nat of Nonempty (Sum Nat Empty)
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance.answer] ✅️ Nonempty (Sum Nat Empty)
   [Meta.synthInstance] result @Sum.nonemptyLeft Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)

Manual/Interaction.lean

@@ -151,7 +151,7 @@ Setting {option}`eval.pp` to {lean}`false` disables the use of {name Lean.ToExpr
 #eval fun x => x + 1
 ```
 ```leanOutput funEval
-could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
+Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
   Nat → Nat
 ```
 
@@ -175,7 +175,7 @@ set_option eval.derive.repr false
 #eval Quadrant.nw
 ```
 ```leanOutput quadEval2
-could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
+Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
   Quadrant
 ```
 

Manual/Meta/Tactics.lean

@@ -22,6 +22,24 @@ namespace Manual
 
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
 open Lean Elab Term Tactic
+
+/--
+Sets `linter.unusedVariables` to `false` in all `CommandContextInfo.options` within an info tree.
+
+This prevents the outer unused variable linter from re-processing variables in partial proof states
+and generating spurious warnings. Mirrors `disableUnusedVarLinterInInfoTree` in Verso's
+`InlineLean.lean`.
+-/
+private partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree
+  | .context (.commandCtx ci) child =>
+    .context (.commandCtx { ci with options := Lean.Linter.linter.unusedVariables.set ci.options false })
+      (disableUnusedVarLinterInInfoTree child)
+  | .context pci child =>
+    .context pci (disableUnusedVarLinterInInfoTree child)
+  | .node info children =>
+    .node info (children.map disableUnusedVarLinterInInfoTree)
+  | .hole id => .hole id
+
 open Verso.Genre.Manual.InlineLean.Scopes (runWithOpenDecls runWithVariables)
 open SubVerso.Highlighting
 open SubVerso.Examples.Messages
@@ -183,7 +201,8 @@ where
     ws.apply s1.trimAscii.copy == ws.apply s2.trimAscii.copy
 
   mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : TermElabM InfoTree := do
-    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
+    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx })
+      (trees.map disableUnusedVarLinterInInfoTree)
     let ctx := PartialContextInfo.commandCtx {
       env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace,
       openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen
@@ -374,7 +393,8 @@ def goal : RoleExpander
         pure #[]
 where
   mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do
-    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
+    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx })
+      (trees.map disableUnusedVarLinterInInfoTree)
     let ctx := PartialContextInfo.commandCtx {
       env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace,
       openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen
@@ -538,7 +558,8 @@ def proofState : CodeBlockExpander
 
 where
   mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : DocElabM InfoTree := do
-    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
+    let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx })
+      (trees.map disableUnusedVarLinterInInfoTree)
     let ctx := PartialContextInfo.commandCtx {
       env := ← getEnv, fileMap := ← getFileMap, mctx := {}, currNamespace := ← getCurrNamespace,
       openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen

Manual/NotationsMacros/SyntaxDef.lean

@@ -228,14 +228,14 @@ In the second example, {tech}[macro scopes] inserted by quotation are visible on
   logInfo (repr (removeSourceInfo stx.raw))
 ```
 The contents of the {tech}[pre-resolved identifier] {name}`List.length` are visible here:
-```leanOutput reprStx2
+```leanOutput reprStx2 (allowDiff := 2)
 Lean.Syntax.node
   (Lean.SourceInfo.none)
   `Lean.Parser.Term.app
   #[Lean.Syntax.ident
       (Lean.SourceInfo.none)
       "List.length".toRawSubstring
-      (Lean.Name.mkNum `List.length._@.Manual.NotationsMacros.SyntaxDef._hyg 2)
+      (Lean.Name.mkNum (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkNum `List.length.«_@».Manual.NotationsMacros.SyntaxDef 1704743902) "_hygCtx") "_hyg") 2)
       [Lean.Syntax.Preresolved.decl `List.length []],
     Lean.Syntax.node
       (Lean.SourceInfo.none)
@@ -290,9 +290,9 @@ In the second example, {tech}[macro scopes] inserted by quotation are visible on
   let stx ← `(List.length ["Rose", "Daffodil", "Lily"])
   logInfo (toString stx)
 ```
-```leanOutput toStringStx2
+```leanOutput toStringStx2 (allowDiff := 2)
 (Term.app
- `List.length._@.Manual.NotationsMacros.SyntaxDef._hyg.2
+ `List.length._@.Manual.NotationsMacros.SyntaxDef.3168789510._hygCtx._hyg.2
  [(«term[_]» "[" [(str "\"Rose\"") "," (str "\"Daffodil\"") "," (str "\"Lily\"")] "]")])
 ```
 :::

Manual/Runtime.lean

@@ -368,7 +368,6 @@ For simple examples of how to call foreign code from Lean and vice versa, see [t
 ## The Lean ABI
 
 :::leanSection
-
 ```lean -show
 variable {α₁ αₙ β αᵢ}
 private axiom «α₂→…→αₙ₋₁».{u} : Type u
@@ -402,6 +401,7 @@ In the case of {attr}`extern`, all {tech}[irrelevant] types are removed first.
 tag := "ffi-types"
 %%%
 
+:::leanSection
 ```lean -show
 universe u
 variable (p : Prop)
@@ -422,9 +422,11 @@ In the {tech (key := "application binary interface")}[ABI], Lean types are trans
   It is the same as the {ref "run-time-inductives"}[run-time representation] of these types.
   Its runtime value is either a pointer to an object of a subtype of {c}`lean_object` (see the “Inductive types” section below) or it is the value {c}`lean_box(cidx)` for the {c}`cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
-  ```lean -show
-  variable (u : Unit)
-  ```
+:::
+
+```lean -show
+variable (u : Unit)
+```
 
 :::example "`Unit` in the ABI"
 The runtime value of {lean}`u`​` : `{lean}`Unit` is always `lean_box(0)`.

Manual/Tactics/Conv.lean

@@ -132,11 +132,9 @@ tag := "conv-goals"
 :::conv focus (show := "focus")
 :::
 
-:::conv «conv·._» (show := ". ...")
+:::conv «conv·_» (show := "· ...")
 :::
 
-:::conv «conv·._» (show := "· ...")
-:::
 
 :::conv failIfSuccess (show := "fail_if_success")
 :::

Tutorial/Meta/Theme.lean

@@ -112,7 +112,7 @@ def isFro (path : Path) : Bool := path[0]?.isEqSome "fro"
 Build NavBarConfig for FRO section
 -/
 def buildFroNavBarConfig : TemplateM NavBarConfig := do
-  let leftItems ← getPageItems
+  let pageItems ← getPageItems
   let path ← currentPath
 
   let froPathItems (path : Path) : Array NavBarItem := #[
@@ -128,17 +128,21 @@ def buildFroNavBarConfig : TemplateM NavBarConfig := do
   ]
 
   let rightItems : Array NavBarItem := #[
-    { title := Icon.moon, alt := some "Change Theme", classes := some "change-theme" },
-    { title := Icon.github, alt := some "Github", url := some "https://github.com/leanprover/lean4", blank := true }
+    { title := Icon.moon, alt := some "Change Theme", classes := some "change-theme", align := .right },
+    { title := Icon.github, alt := some "Github", url := some "https://github.com/leanprover/lean4", blank := true, align := .right }
   ]
 
-  let menuItems := #[navFroItem path] ++ froPathItems path
+  let menuItems : Array NavBarItem := (#[navFroItem path] ++ froPathItems path).map fun item =>
+    { item with display := .mobile }
+
+  let items : Array NavBarEntry :=
+    (pageItems.map .item) ++
+    (externalLinks.map .item) ++
+    (menuItems.map .item) ++
+    (rightItems.map .item)
 
   return {
-    leftItems := leftItems
-    rightItems := rightItems
-    menuItems := menuItems
-    externalLinks := externalLinks
+    items := items
     subNavBar := if isFro path then some (SubNavBarConfig.mk (froPathItems path)) else none
   }
 

Tutorial/VCGen.lean

@@ -216,7 +216,36 @@ def nodup (l : List Int) : Bool := Id.run do
 ```
 :::
 
-:::paragraph
+::::paragraph
+:::codeOnly
+```lean
+-- NOTE: This is needed because a recent nightly didn't update the
+-- type of Invariant.withEarlyReturn to use MProd
+abbrev withEarlyReturn {α} {xs : List α} {γ : Type (max u₁ u₂)}
+  (onContinue : List.Cursor xs → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onExcept : ExceptConds ps := ExceptConds.false) :
+    Invariant xs (MProd (Option γ) β) ps :=
+  ⟨fun ⟨xs, x, b⟩ => spred(
+        (⌜x = none⌝ ∧ onContinue xs b)
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suffix = []⌝ ∧ onReturn r b)),
+   onExcept⟩
+-- This test will fail when upstream has been fixed. At that time,
+-- remove the helper and update the proof again.
+/--
+info:
+Std.Do.Invariant.withEarlyReturn.{u₁, u₂} {β : Type (max u₁ u₂)}
+  {ps : PostShape} {α : Type (max u₁ u₂)} {xs : List α}
+  {γ : Type (max u₁ u₂)} (onContinue : xs.Cursor → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onExcept : ExceptConds ps := ExceptConds.false) :
+  Invariant xs (Option γ × β) ps
+-/
+#guard_msgs (whitespace := lax) in
+#check Invariant.withEarlyReturn
+```
+:::
+
 This function is correct if it returns {name}`true` for every list that satisfies {name}`List.Nodup` and {name}`false` for every list that does not.
 Just as it was in {name}`mySum`, the use of {keywordOf Lean.Parser.Term.do}`do`-notation and the {name}`Id` monad is an internal implementation detail of {name}`nodup`.
 Thus, the proof begins by using {name}`Id.of_wp_run_eq` to make the proof state amenable to {tactic}`mvcgen`:
@@ -226,13 +255,13 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
   apply Id.of_wp_run_eq h
   mvcgen
   invariants
-  · Invariant.withEarlyReturn
+  · withEarlyReturn
       (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
       (onContinue := fun xs seen =>
         ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝)
   with grind
 ```
-:::
+::::
 
 
 :::paragraph
@@ -262,7 +291,7 @@ end
 :::
 
 :::paragraph
-Note that the form `mvcgen invariants?` will suggest an initial invariant using {name}`Invariant.withEarlyReturn`, so there is no need to memorize the exact syntax for specifying invariants:
+Note that the form `mvcgen invariants?` will suggest an initial invariant, so there is no need to memorize the exact syntax for specifying invariants:
 ```lean (name := invariants?)
 example (l : List Int) : nodup l ↔ l.Nodup := by
   generalize h : nodup l = r
@@ -274,9 +303,9 @@ This starting point will not allow the proof to succeed—after all, if the inva
 ```leanOutput invariants?
 Try this:
   [apply] invariants
-  ·
-    Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue :=
-      fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
+  · ⇓⟨xs, letMuts⟩ =>
+    ⌜xs.prefix = [] ∧ letMuts = ⟨none, ∅⟩ ∨
+        xs.suffix = [] ∧ (True ↔ l.Nodup) ∧ ∀ (a : Bool), letMuts.fst = some a → (a = true ↔ l.Nodup)⌝
 ```
 :::
 
@@ -891,11 +920,11 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
   wp_pure := by
     intros
     ext
-    simp [wp, ExceptT.run, Id.run, pure, Except.pure, throwThe]
+    simp [wp, ExceptT.run, Id.run, pure, Except.pure]
   wp_bind x f := by
     dsimp only [wp, bind]
     ext
-    cases x <;> simp [ExceptT.run, Id.run, pure, Except.pure, throwThe]
+    cases x <;> simp [ExceptT.run, Id.run, pure, Except.pure]
 ```
 :::
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9f7be0d7cc5706b12097cc3d014d4ee75021768f",
+   "rev": "44daa1f5008ab110e0b781a1138929d3561fa8e3",
    "name": "versowebcomponents",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "936359a56e5f0827c7d378d25916b2f24d4aef4c",
+   "rev": "895de3c71717a6902125254e4b32d9c7565a0463",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8629a535d10cd7edfbf1a2c5cdfbaeee135a62cd",
+   "rev": "650d4104daeb660ff3cc46715602a664504e7785",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",