fix: don't clobber messages

One of the scope preservation combinators was incorrectly clobbering
the message log, which led to errors not being correctly
registered. This has now been fixed, along with the errors in question.

Manual/Classes.lean

@@ -273,7 +273,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
   else
     let j := i / 2
     if Ord.compare xs.contents[i] xs.contents[j] == .lt then
-      Heap.bubbleUp j {xs with contents := xs.contents.swap ⟨i, by omega⟩ ⟨j, by omega⟩}
+      Heap.bubbleUp j {xs with contents := xs.contents.swap i j}
     else xs
 
 def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
@@ -294,13 +294,12 @@ def Heap'.bubbleUp [inst : Ord α] (i : Nat) (xs : @Heap' α inst) : @Heap' α i
   else
     let j := i / 2
     if inst.compare xs.contents[i] xs.contents[j] == .lt then
-      Heap'.bubbleUp j {xs with contents := xs.contents.swap ⟨i, by omega⟩ ⟨j, by omega⟩}
+      Heap'.bubbleUp j {xs with contents := xs.contents.swap i j}
     else xs
 
 def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α :=
   let i := xs.contents.size
   {xs with contents := xs.contents.push x}.bubbleUp i
-end A
 ```
 
 In the improved definitions, {name}`Heap'.bubbleUp` is needlessly explicit; the instance does not need to be explicitly named here because Lean would select the indicated instances nonetheless, but it does bring the correctness invariant front and center for readers.

Manual/Classes/InstanceDecls.lean

@@ -268,8 +268,10 @@ However, because it is an ordinary Lean function, it can recursively refer to it
 instance instDecidableEqStringList : DecidableEq StringList
   | .nil, .nil => .isTrue rfl
   | .cons h1 t1, .cons h2 t2 =>
+    let _ : Decidable (t1 = t2) :=
+      instDecidableEqStringList t1 t2
     if h : h1 = h2 then
-      if h' : instDecidableEqStringList t1 t2 then
+      if h' : t1 = t2 then
         .isTrue (by simp [*])
       else
         .isFalse (by intro hEq; cases hEq; trivial)

Manual/Language.lean

@@ -301,7 +301,7 @@ open Greetings
 
 The section's name must be used to close it.
 
-```lean (error := true) (name := english4)
+```lean (error := true) (name := english4) (keep := false)
 end
 ```
 ```leanOutput english4

Manual/Meta/Lean.lean

@@ -292,7 +292,7 @@ def leanInline : RoleExpander
     let expectedType ← config.type.mapM fun (s : StrLit) => do
       match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with
       | .error e => throwErrorAt term e
-      | .ok stx => withEnableInfoTree false do
+      | .ok stx => withEnableInfoTree false <| runWithOpenDecls <| runWithVariables fun _ => do
         let t ← Elab.Term.elabType stx
         Term.synthesizeSyntheticMVarsNoPostponing
         let t ← instantiateMVars t
@@ -917,14 +917,18 @@ def name : RoleExpander
     let exampleName := name.getString.toName
     let identStx := mkIdentFrom arg (cfg.full.getD exampleName) (canonical := true)
 
-    let resolvedName ←
-      runWithOpenDecls <| runWithVariables fun _ =>
-        withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) do
-          realizeGlobalConstNoOverloadWithInfo identStx
+    try
+      let resolvedName ←
+        runWithOpenDecls <| runWithVariables fun _ =>
+          withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) do
+            realizeGlobalConstNoOverloadWithInfo identStx
 
-    let hl : Highlighted ← constTok resolvedName name.getString
+      let hl : Highlighted ← constTok resolvedName name.getString
 
-    pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])]
+      pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])]
+    catch e =>
+      logErrorAt identStx e.toMessageData
+      pure #[← `(Inline.code $(quote name.getString))]
   | _, more =>
     if h : more.size > 0 then
       throwErrorAt more[0] "Unexpected contents"

Manual/Meta/Lean/Scopes.lean

@@ -46,7 +46,8 @@ context to provide access to variables.
 -/
 def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do
   let scope := (← getScopes).head!
-  Term.withAutoBoundImplicit <|
+  Term.withAutoBoundImplicit do
+    let msgLog ← Core.getMessageLog
     Term.elabBinders scope.varDecls fun xs => do
       -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature
       -- If we don't use this checkpoint here, then auto-bound implicits in the postponed terms will not be handled correctly.
@@ -57,7 +58,7 @@ def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do
       withReader ({ · with sectionFVars := sectionFVars }) do
         -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
         -- So, we use `Core.resetMessageLog`.
-        Core.resetMessageLog
+        Core.setMessageLog msgLog
         let someType := mkSort levelZero
         Term.addAutoBoundImplicits' xs someType fun xs _ =>
           Term.withoutAutoBoundImplicit <| elabFn xs

Manual/Monads.lean

@@ -64,7 +64,6 @@ The {name}`Alternative` type class describes applicative functors that additiona
 ```lean (show := false)
 section
 variable {α : Type u} {β : Type u}
-variable {n : Nat}
 ```
 
 ::::example "Lists with Lengths as Applicative Functors"
@@ -113,7 +112,7 @@ instance : Applicative (LenList n) where
     list := List.replicate n x
     lengthOk := List.length_replicate _ _
   }
-  seq fs xs := fs.zipWith (· ·) (xs ())
+  seq {α β} fs xs := fs.zipWith (· ·) (xs ())
 ```
 
 The well-behaved {name}`Monad` instance takes the diagonal of the results of applying the function:
@@ -128,7 +127,8 @@ def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α :=
   match n with
   | 0 => ⟨[], rfl⟩
   | n' + 1 => {
-    list := square.head.head :: (square.tail.map (·.tail)).diagonal.list,
+    list :=
+      square.head.head :: (square.tail.map (·.tail)).diagonal.list
     lengthOk := by simp
   }
 ```

Manual/Monads/Laws.lean

@@ -24,6 +24,8 @@ set_option linter.unusedVariables false
 tag := "monad-laws"
 %%%
 
+:::keepEnv
+
 ```lean (show := false)
 section Laws
 universe u u' v
@@ -38,7 +40,7 @@ axiom γ : Type u'
 axiom x : f α
 ```
 
-:::keepEnv
+
 ```lean (show := false)
 section F
 variable {f : Type u → Type v} [Functor f] {α β : Type u} {g : α → β} {h : β → γ} {x : f α}
@@ -64,7 +66,7 @@ The {name}`LawfulFunctor` class includes the necessary proofs.
 ```lean (show := false)
 end F
 ```
-:::
+
 
 In addition to proving that the potentially-optimized {name}`SeqLeft.seqLeft` and {name}`SeqRight.seqRight` operations are equivalent to their default implementations, Applicative functors {lean}`f` must satisfy four laws.
 
@@ -75,3 +77,5 @@ The {deftech}[monad laws] specify that {name}`pure` followed by {name}`bind` sho
 {docstring LawfulMonad}
 
 {docstring LawfulMonad.mk'}
+
+:::

Manual/Monads/Lift.lean

@@ -43,6 +43,11 @@ Users should not define new instances of {name}`MonadLiftT`, but it is useful as
 
 {docstring MonadLiftT}
 
+```lean (show := false)
+section
+variable {m : Type → Type u}
+```
+
 :::example "Monad Lifts in Function Signatures"
 The function {name}`IO.withStdin` has the following signature:
 ```signature
@@ -55,6 +60,10 @@ Because it doesn't require its parameter to precisely be in {name}`IO`, it can b
 The instance implicit parameter {lean}`MonadLiftT BaseIO m` allows the reflexive transitive closure of {name}`MonadLift` to be used to assemble the lift.
 :::
 
+```lean (show := false)
+end
+```
+
 
 When a term of type {lean}`n β` is expected, but the provided term has type {lean}`m α`, and the two types are not definitionally equal, Lean attempts to insert lifts and coercions before reporting an error.
 There are the following possibilities:
@@ -113,23 +122,31 @@ fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α
 There are also instances of {name}`MonadLift` for most of the standard library's {tech}[monad transformers], so base monad actions can be used in transformed monads without additional work.
 For example, state monad actions can be lifted across reader and exception transformers, allowing compatible monads to be intermixed freely:
 ````lean (keep := false)
-def incrBy (n : Nat) : StateM Nat Unit := modify (+ n)
+def incrBy (n : Nat) : StateM Nat Unit := modify (· + n)
 
 def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
   if (← read) > 5 then throw "Too much!"
   incrBy (← read)
 ````
 
-Disabling lifting causes the code to fail to work:
-````lean (name := noLift)
+Disabling lifting causes an error:
+````lean (name := noLift) (error := true)
 set_option autoLift false
 
-def incrBy (n : Nat) : StateM Nat Unit := modify (+ n)
+def incrBy (n : Nat) : StateM Nat Unit := modify (. + n)
 
 def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
   if (← read) > 5 then throw "Too much!"
   incrBy (← read)
 ````
+```leanOutput noLift
+type mismatch
+  incrBy __do_lift✝
+has type
+  StateM Nat Unit : Type
+but is expected to have type
+  ReaderT Nat (ExceptT String (StateM Nat)) Unit : Type
+```
 
 ::::
 :::::

Manual/Monads/Syntax.lean

@@ -20,6 +20,8 @@ set_option pp.rawOnError true
 set_option linter.unusedVariables false
 -- set_option trace.SubVerso.Highlighting.Code true
 
+set_option guard_msgs.diff true
+
 #doc (Manual) "Syntax" =>
 
 Lean supports programming with functors, applicative functors, and monads via special syntax:
@@ -589,7 +591,7 @@ p : α → Prop
 inst✝ : DecidablePred p
 xs : Array α
 out✝ : Array Nat := #[]
-col✝ : Std.Range := { start := 0, stop := xs.size, step := 1 }
+col✝ : Std.Range := { start := 0, stop := xs.size, step := 1, step_pos := Nat.zero_lt_one }
 i : Nat
 r✝ : Array Nat
 out : Array Nat := r✝

Manual/Monads/Zoo.lean

@@ -225,7 +225,7 @@ The standard library exports a mix of operations from the `-Of` and undecorated
 ```lean (show := false)
 example : @get = @MonadState.get := by rfl
 example : @set = @MonadStateOf.set := by rfl
-example (f : σ → σ) : @modify σ m inst f = @MonadState.modifyGet σ m inst PUnit fun (s : σ) => (PUnit.unit, f s) := by rfl
+example {inst} (f : σ → σ) : @modify σ m inst f = @MonadState.modifyGet σ m inst PUnit fun (s : σ) => (PUnit.unit, f s) := by rfl
 example : @modifyGet = @MonadState.modifyGet := by rfl
 example : @read = @MonadReader.read := by rfl
 example : @readThe = @MonadReaderOf.read := by rfl

Manual/NotationsMacros.lean

@@ -520,8 +520,8 @@ def ex2 (e) := show m _ from `(2 + $e :num)
 end
 ```
 
-::::keepEnv
-:::example "Expanding Quasiquotation"
+:::::keepEnv
+::::example "Expanding Quasiquotation"
 Printing the definition of {name}`f` demonstrates the expansion of a quasiquotation.
 ```lean (name := expansion)
 open Lean in
@@ -548,8 +548,11 @@ fun {m} [Monad m] [Lean.MonadQuotation m] x n => do
                   (Syntax.ident info "k".toSubstring' (Lean.addMacroScope mainModule `k scp) []))) }.raw
 ```
 
+:::paragraph
 ```lean (show := false)
 section
+open Lean (Term)
+open Lean.Quote
 variable {x : Term} {n : Nat}
 ```
 
@@ -558,13 +561,15 @@ It begins by constructing the source information for the resulting syntax, obtai
 It then obtains the current macro scope and the name of the module being processed, because macro scopes are added with respect to a module to enable independent compilation and avoid the need for a global counter.
 It then constructs a node using helpers such as {name}`Syntax.node1` and {name}`Syntax.node2`, which create a {name}`Syntax.node` with the indicated number of children.
 The macro scope is added to each identifier, and {name Lean.TSyntax.raw}`TSyntax.raw` is used to extract the contents of typed syntax wrappers.
-The antiquotations of {lean}`x` and {lean}`quote (n + 2)` occur directly in the expansion, as parameters to {name}`Syntax.node3`.
+The antiquotations of {lean}`x` and {lean type:="Term"}`quote (n + 2)` occur directly in the expansion, as parameters to {name}`Syntax.node3`.
 
 ```lean (show := false)
 end
 ```
 :::
+
 ::::
+:::::
 
 
 ### Splices
@@ -696,14 +701,14 @@ syntax "⟨| " (term)? " |⟩": term
 
 The `?` splice suffix for a term expects an {lean}`Option Term`:
 ```lean
-def mkStx [Monad m] [MonadQuotation m] (e) : m Term :=
+def mkStx [Monad m] [MonadQuotation m] (e : Option Term) : m Term :=
   `(⟨| $(e)? |⟩)
 ```
 ```lean (name := checkMkStx)
 #check mkStx
 ```
 ```leanOutput checkMkStx
-mkStx {m : Type → Type} [Monad m] [MonadQuotation m] (e : Option (TSyntax `term)) : m Term
+mkStx {m : Type → Type} [Monad m] [MonadQuotation m] (e : Option Term) : m Term
 ```
 
 Supplying {name}`some` results in the optional term being present.
@@ -716,7 +721,7 @@ Supplying {name}`some` results in the optional term being present.
 
 Supplying {name}`none` results in the optional term being absent.
 ```lean (name := noneMkStx)
-#eval do logInfo (← mkStx none))
+#eval do logInfo (← mkStx none)
 ```
 ```leanOutput noneMkStx
 ⟨| |⟩
@@ -970,7 +975,7 @@ open Lean.Macro
 The `arbitrary!` macro is intended to expand to some arbitrarily-determined value of a given type.
 
 ```lean
-syntax (name := arbitrary!) "arbitrary!" term:arg : term
+syntax (name := arbitrary!) "arbitrary! " term:arg : term
 ```
 
 :::keepEnv
@@ -1024,30 +1029,30 @@ macro_rules
 Additionally, if any rule throws the {name Lean.Macro.Exception.unsupportedSyntax}`unsupportedSyntax` exception, no further rules in that command are checked.
 ```lean
 macro_rules
-  | `(arbitrary! Nat) => throwUnsupported
-  | `(arbitrary! Nat) => `(42)
+  | `(arbitrary! (List Nat)) => throwUnsupported
+  | `(arbitrary! (List $_)) => `([])
 
 macro_rules
-  | `(arbitrary! Int) => `(42)
+  | `(arbitrary! (Array Nat)) => `(#[42])
 macro_rules
-  | `(arbitrary! Int) => throwUnsupported
+  | `(arbitrary! (Array $_)) => throwUnsupported
 ```
 
-The case for {lean}`Nat` fails to elaborate, because macro expansion did not translate the {keywordOf arbitrary!}`arbitrary!` syntax into something supported by the elaborator.
+The case for {lean}`List Nat` fails to elaborate, because macro expansion did not translate the {keywordOf arbitrary!}`arbitrary!` syntax into something supported by the elaborator.
 ```lean (name := arb3) (error := true)
-#eval arbitrary! Nat
+#eval arbitrary! (List Nat)
 ```
 ```leanOutput arb3
 elaboration function for 'arbitrary!' has not been implemented
-  arbitrary! Nat
+  arbitrary! (List Nat)
 ```
 
-The case for {lean}`Int` succeeds, because the first set of macro rules are attempted after the second throws the exception.
+The case for {lean}`Array Nat` succeeds, because the first set of macro rules are attempted after the second throws the exception.
 ```lean (name := arb4)
-#eval arbitrary! Int
+#eval arbitrary! (Array Nat)
 ```
 ```leanOutput arb4
-42
+#[42]
 ```
 ::::
 

Manual/RecursiveDefs/Structural.lean

@@ -328,7 +328,7 @@ Wrapping the discriminants in a pair breaks the connection.
 :::example "Structural Recursion Under Pairs"
 
 This function that finds the minimum of the two components of a pair can't be elaborated via structural recursion.
-```lean (error := true) (name := minpair)
+```lean (error := true) (name := minpair) (keep := false)
 def min' (nk : Nat × Nat) : Nat :=
   match nk with
   | (0, _) => 0
@@ -346,7 +346,7 @@ This is because the parameter's type, {name}`Prod`, is not recursive.
 Thus, its constructor has no recursive parameters that can be exposed by pattern matching.
 
 This definition is accepted using {tech}[well-founded recursion], however:
-```lean (keep := false)
+```lean
 def min' (nk : Nat × Nat) : Nat :=
   match nk with
   | (0, _) => 0