chore: bump to nightly-2025-05-20 (#444)

Author: david-christiansen

Manual/Elaboration.lean

@@ -185,7 +185,7 @@ example (b : B) : ⟨b.1, b.2⟩ = b := rfl
 error: type mismatch
   rfl
 has type
-  ?m.736 = ?m.736 : Prop
+  ?m.744 = ?m.744 : Prop
 but is expected to have type
   e1 = e2 : Prop
 -/

Manual/Intro.lean

@@ -99,9 +99,9 @@ declaration uses 'sorry'
 
 Error messages are shown like this:
 ```leanOutput output (severity := error)
-Application type mismatch: In the appplication
+Application type mismatch: In the application
   Nat.succ "two"
-the final argument
+the argument
   "two"
 has type
   String : Type

Manual/Language/InductiveTypes.lean

@@ -264,10 +264,14 @@ inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
   | right : β → Either' α β
 ```
 ```leanOutput Either'
-inductive datatype parameter mismatch
+Mismatched inductive type parameter in
+  Either' α β
+The provided argument
   α
-expected
+is not definitionally equal to the expected parameter
   α✝
+
+Note: The value of parameter 'α✝' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
 ```
 
 Placing the parameters after the colon results in parameters that can be instantiated by the constructors:

Manual/Language/InductiveTypes/Structures.lean

@@ -533,9 +533,9 @@ it is a type error to apply {name}`printEven` directly to {name}`two`:
 #check printEven two
 ```
 ```leanOutput printTwo
-Application type mismatch: In the appplication
+Application type mismatch: In the application
   printEven two
-the final argument
+the argument
   two
 has type
   EvenPrime : Type

Manual/Meta/Basic.lean

@@ -152,111 +152,3 @@ def commandWithoutAsync : (act : CommandElabM α) → CommandElabM α :=
 
 def withoutAsync [Monad m] [MonadWithOptions m] : (act : m α) → m α :=
   withOptions (Elab.async.set · false)
-
-
-/--
-Consistently rewrite all substrings that look like automatic metavariables (e.g "?m.123") so
-that they're ?m.1, ?m.2, etc.
--/
-def normalizeMetavars (str : String) : String := Id.run do
-  let mut out := ""
-  let mut iter := str.iter
-  let mut gensymCounter := 1
-  let mut nums : Std.HashMap String Nat := {}
-  -- States are:
-  -- * none - Not looking at a metavar
-  -- * 0 - Saw the ?
-  -- * 1 - Saw the m
-  -- * 2 - Saw the .
-  -- * 3 - Saw one or more digits
-  let mut state : Option (Fin 4 × String.Iterator) := none
-  while h : iter.hasNext do
-    let c := iter.curr' h
-
-    match state with
-    | none =>
-      if c == '?' then
-        state := some (0, iter)
-      else
-        out := out.push c
-    | some (0, i) =>
-      state := if c == 'm' then some (1, i) else none
-    | some (1, i) =>
-      state := if c == '.' then some (2, i) else none
-    | some (2, i) =>
-      state := if c.isDigit then some (3, i) else none
-    | some (3, i) =>
-      unless c.isDigit do
-        state := none
-        let mvarStr := i.extract iter
-        match nums[mvarStr]? with
-        | none =>
-          nums := nums.insert mvarStr gensymCounter
-          out := out ++ s!"?m.{gensymCounter}"
-          gensymCounter := gensymCounter + 1
-        | some s => out := out ++ s!"?m.{s}"
-        out := out.push c
-
-    iter := iter.next
-  match state with
-  | some (3, i) =>
-    let mvarStr := i.extract iter
-    match nums[mvarStr]? with
-    | none =>
-      nums := nums.insert mvarStr gensymCounter
-      out := out ++ s!"?m.{gensymCounter}"
-      gensymCounter := gensymCounter + 1
-    | some s => out := out ++ s!"?m.{s}"
-  | some (_, i) =>
-    out := out ++ i.extract iter
-  | _ => pure ()
-
-  out
-
-/-- info: "List ?m.1" -/
-#guard_msgs in
-#eval normalizeMetavars "List ?m.9783"
-
-/-- info: "List ?m.1 " -/
-#guard_msgs in
-#eval normalizeMetavars "List ?m.9783 "
-
-/-- info: "x : ?m.1\nxs : List ?m.1\nelem : x ∈ xs\n⊢ xs.length > 0\n" -/
-#guard_msgs in
-#eval normalizeMetavars
-  r##"x : ?m.1034
-xs : List ?m.1034
-elem : x ∈ xs
-⊢ xs.length > 0
-"##
-
-/-- info: "x : ?m.1\nxs : List ?m.1\nelem : x ∈ xs\n⊢ xs.length > 0" -/
-#guard_msgs in
-#eval normalizeMetavars
-  r##"x : ?m.1034
-xs : List ?m.1034
-elem : x ∈ xs
-⊢ xs.length > 0"##
-
-/-- info: "x : ?m.1\nxs : List ?m.2\nelem : x ∈ xs\n⊢ xs.length > 0" -/
-#guard_msgs in
-#eval normalizeMetavars
-  r##"x : ?m.1034
-xs : List ?m.10345
-elem : x ∈ xs
-⊢ xs.length > 0"##
-
-/-- info: "x : ?m.1\nxs : List ?m.2\nelem : x ∈ xs\n⊢ xs.length > 0" -/
-#guard_msgs in
-#eval normalizeMetavars
-  r##"x : ?m.1035
-xs : List ?m.1034
-elem : x ∈ xs
-⊢ xs.length > 0"##
-
-#eval normalizeMetavars
-  r##"x : ?m.1035
-α : Type ?u.1234
-xs : List ?m.1034
-elem : x ∈ xs
-⊢ xs.length > 0"##

Manual/Meta/Syntax.lean

@@ -830,7 +830,7 @@ where
       return bar ++ .nest 2 (← production which stx |>.run' {})
 
 def testGetBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : TermElabM String := do
-  let (tagged, _) ← getBnf config isFirst stxs |>.run {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩}
+  let (tagged, _) ← getBnf config isFirst stxs |>.run (← ``(Manual)) (.const ``Manual []) {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩}
   pure tagged.stripTags
 
 namespace Tests
@@ -897,7 +897,7 @@ info: antiquot ::= ...
 
 end Tests
 
-instance : MonadWithReaderOf Core.Context DocElabM := inferInstanceAs (MonadWithReaderOf Core.Context (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)))
+instance : MonadWithReaderOf Core.Context DocElabM := inferInstanceAs (MonadWithReaderOf Core.Context (ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))))
 
 def withOpenedNamespace (ns : Name) (act : DocElabM α) : DocElabM α :=
   try

Manual/Meta/Tactics.lean

@@ -11,6 +11,7 @@ import Verso.Code.Highlighted
 import Verso.Doc.ArgParse
 import Verso.Doc.Suggestion
 import SubVerso.Highlighting.Code
+import SubVerso.Examples.Messages
 import VersoManual
 
 import Manual.Meta.Basic
@@ -22,6 +23,7 @@ open Lean Elab Term Tactic
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
 open Verso.Genre.Manual.InlineLean.Scopes (runWithOpenDecls runWithVariables)
 open SubVerso.Highlighting
+open SubVerso.Examples.Messages
 
 structure TacticOutputConfig where
   «show» : Bool := true

Manual/NotationsMacros.lean

@@ -273,9 +273,9 @@ example (cmd1 cmd2 : TSyntax `command) : MacroM (TSyntax `command) := `($cmd1 $c
 ```
 The result is two type errors like the following:
 ```leanOutput cmdQuot
-Application type mismatch: In the appplication
+Application type mismatch: In the application
   cmd1.raw
-the final argument
+the argument
   cmd1
 has type
   TSyntax `command : Type

Manual/NotationsMacros/SyntaxDef.lean

@@ -756,44 +756,45 @@ In particular, Indentation-sensitvity is specified by combining {name Lean.Parse
 :::example "Aligned Columns"
 This syntax for saving notes takes a bulleted list of items, each of which must be aligned at the same column.
 ```lean
-syntax "note " ppLine withPosition((colEq "• " str ppLine)+) : term
+syntax "note " ppLine withPosition((colEq "◦ " str ppLine)+) : term
 ```
 
 There is no elaborator or macro associated with this syntax, but the following example is accepted by the parser:
 ```lean (error := true) (name := noteEx1)
 #check
   note
-    • "One"
-    • "Two"
+    ◦ "One"
+    ◦ "Two"
 ```
 ```leanOutput noteEx1
-elaboration function for '«termNote__•__»' has not been implemented
+elaboration function for '«termNote__◦__»' has not been implemented
   note
-    • "One"
-    • "Two"
+    ◦ "One"
+    ◦ "Two"
+
 ```
 
 The syntax does not require that the list is indented with respect to the opening token, which would require an extra `withPosition` and a `colGt`.
 ```lean (error := true) (name := noteEx15)
 #check
   note
-• "One"
-• "Two"
+◦ "One"
+◦ "Two"
 ```
 ```leanOutput noteEx15
-elaboration function for '«termNote__•__»' has not been implemented
+elaboration function for '«termNote__◦__»' has not been implemented
   note
-    • "One"
-    • "Two"
+    ◦ "One"
+    ◦ "Two"
 ```
 
 
 The following examples are not syntactically valid because the columns of the bullet points do not match.
 ```syntaxError noteEx2
 #check
   note
-    • "One"
-   • "Two"
+    ◦ "One"
+   ◦ "Two"
 ```
 ```leanOutput noteEx2
 <example>:4:3-4:4: expected end of input
@@ -802,8 +803,8 @@ The following examples are not syntactically valid because the columns of the bu
 ```syntaxError noteEx2
 #check
   note
-   • "One"
-     • "Two"
+   ◦ "One"
+     ◦ "Two"
 ```
 ```leanOutput noteEx2
 <example>:4:5-4:6: expected end of input

Manual/RecursiveDefs/PartialFixpoint.lean

@@ -175,7 +175,7 @@ The error message on the recursive call is:
 ```leanOutput nonTailPos
 Could not prove 'List.findIndex' to be monotone in its recursive calls:
   Cannot eliminate recursive call `List.findIndex ys p` enclosed in
-    let_fun r := ys✝.findIndex p;
+    have r := ys✝.findIndex p;
     if r = -1 then -1 else r + 1
 ```