chore: bump toolchain to v4.23.0-rc1

examples/textbook/DemoTextbook.lean

@@ -82,7 +82,7 @@ Expected error messages must be indicated explicitly:
 #eval y
 ```
 ```leanOutput yVal
-unknown identifier 'y'
+Unknown identifier `y`
 ```
 
 {include 1 DemoTextbook.Nat}

examples/website/DemoSite/Blog/Conditionals.lean

@@ -234,12 +234,12 @@ Here's some hoverable info:
 example : Nat := "Not a number"
 ```
 ```leanOutput typeErr
-type mismatch
+Type mismatch
   "Not a number"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 ```
 
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
+   "rev": "feac4e0c356b0928657bf3b54fa83ae952f53257",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
+leanprover/lean4:v4.23.0-rc1

src/multi-verso/MultiVerso.lean

@@ -341,7 +341,7 @@ private def RemoteInfo.structBEq (x y : RemoteInfo) : Bool :=
   x1 == x2 &&
   y1 == y2 &&
   doms1.size == doms2.size &&
-  doms1.fold (init := true) fun soFar k v =>
+  doms1.foldl (init := true) fun soFar k v =>
     soFar && (doms2.find? k).isEqSome v
 
 private unsafe def RemoteInfo.fastBEq (x y : RemoteInfo) : Bool :=

src/multi-verso/MultiVerso/Slug.lean

@@ -13,28 +13,95 @@ open Verso.Method
 open Lean (ToJson FromJson)
 open Std (HashSet)
 
+private def validCharString := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_"
+
+
 /-- The characters allowed in slugs. -/
-def Slug.validChars := HashSet.ofList "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_".toList
+def Slug.validChars := HashSet.ofList validCharString.toList
+
+/--
+A slug is well-formed if all its characters are valid.
+-/
+def Slug.WF (str : String) : Prop :=
+  str.toList.all (· ∈ validChars)
+
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let mut iter := validCharString.iter
+  while h : iter.hasNext do
+    let c := iter.curr' h
+    iter := iter.next' h
+    let n := mkIdent <| `Slug ++ (.str .anonymous s!"'{c}'_mem_validChars")
+    let cmd ←
+      `(@[simp, grind] protected theorem $n : ($(quote c) ∈ Slug.validChars) := by simp [Slug.validChars, validCharString])
+    elabCommand cmd
+
 
 private def mangle (c : Char) : String :=
-  match c with
-  | '<' => "_LT_"
-  | '>' => "_GT_"
-  | ';' => "_SEMI_"
-  | '‹' => "_FLQ_"
-  | '›' => "_FRQ_"
-  | '«' => "_FLQQ_"
-  | '»' => "_FLQQ_"
-  | '⟨' => "_LANGLE_"
-  | '⟩' => "_RANGLE_"
-  | '(' => "_LPAR_"
-  | ')' => "_RPAR_"
-  | '[' => "_LSQ_"
-  | ']' => "_RSQ_"
-  | '→' => "_ARR_"
-  | '↦' => "_MAPSTO_"
-  | '⊢' => "_VDASH_"
-  | _ => "___"
+  replacements.lookup c |>.getD "___"
+where
+  replacements : List (Char × String) := [
+    ('<', "_LT_"),
+    ('>', "_GT_"),
+    (';', "_SEMI_"),
+    ('‹', "_FLQ_"),
+    ('›', "_FRQ_"),
+    ('«', "_FLQQ_"),
+    ('»', "_FLQQ_"),
+    ('⟨', "_LANGLE_"),
+    ('⟩', "_RANGLE_"),
+    ('(', "_LPAR_"),
+    (')', "_RPAR_"),
+    ('[', "_LSQ_"),
+    (']', "_RSQ_"),
+    ('→', "_ARR_"),
+    ('↦', "_MAPSTO_"),
+    ('⊢', "_VDASH_")
+  ]
+
+
+@[simp, grind] theorem mangle.replacements_all_wf : (k, v) ∈ mangle.replacements → Slug.WF v := by
+  simp [Slug.WF, replacements]
+  intro
+  repeat (rename_i hk; cases hk; simp [*])
+
+@[simp, grind]
+private theorem mangle.replacements_wf (c : Char) : (c, s) ∈ mangle.replacements → Slug.WF (mangle c) := by
+  unfold mangle
+  generalize h : mangle.replacements = reps
+  have : ∀ k v, (k, v) ∈ reps → Slug.WF v := by
+    rw [← h]
+    grind only [=_ List.contains_iff_mem, mangle.replacements_all_wf]
+  clear h
+  fun_induction List.lookup <;> first | grind | simp
+
+@[simp, grind]
+private theorem mangle_wf (c : Char) : Slug.WF (mangle c) := by
+  unfold mangle
+  by_cases h : ∃ s, (c, s) ∈ mangle.replacements
+  . let ⟨w, p⟩ := h
+    apply mangle.replacements_wf _ p
+  . suffices List.lookup c mangle.replacements = none by
+      rw [this]
+      simp [Slug.WF]
+    generalize h' : mangle.replacements = xs
+    rw [h'] at h
+    clear h'
+    fun_induction List.lookup with try ((first | grind | simp); done)
+    | case2 _ _ _ _ beq =>
+      have := LawfulBEq.eq_of_beq beq
+      exfalso
+      apply h
+      simp [*]
+
+
+@[simp, grind]
+private theorem mangle_mem_valid (c : Char) : c ∈ (mangle c').data → c ∈ Slug.validChars := by
+  intro mem
+  have := mangle_wf c'
+  simp [Slug.WF] at this
+  apply this
+  assumption
 
 /--
 Converts a string to a valid slug, mangling as appropriate.
@@ -50,16 +117,13 @@ def asSlug (str : String) : String :=
         else acc ++ mangle c
   loop str.iter ""
 
-/--
-A slug is well-formed if all its characters are valid.
--/
-def Slug.WF (str : String) : Prop :=
-  str.toList.all (· ∈ validChars)
-
 instance : Decidable (c ∈ Slug.validChars) := inferInstance
 
 instance [DecidablePred p] : Decidable (String.all s (p ·)) :=
-  if h : String.all s (p ·) then isTrue h else isFalse h
+  if h : String.all s (p ·) then
+    isTrue h
+  else
+    isFalse h
 
 @[simp]
 theorem String.empty_all_eq_true : "".all p = true := by
@@ -68,59 +132,53 @@ theorem String.empty_all_eq_true : "".all p = true := by
 @[simp]
 theorem String.Pos.add_0_eq_size {c : Char} : (0 : String.Pos) + c = ⟨c.utf8Size⟩ := by
   simp only [HAdd.hAdd, String.Pos.byteIdx_zero, String.Pos.mk.injEq]
-  show 0 + c.utf8Size = c.utf8Size
-  simp
+  grind
 
 instance : DecidablePred Slug.WF := fun str =>
-  if h : str.toList.all (· ∈ Slug.validChars) then isTrue (by unfold Slug.WF; exact h) else isFalse h
-
-@[simp]
-theorem Slug.wf_mangle : WF (mangle c) := by
-  unfold mangle
-  split <;> dsimp [WF, validChars] <;> simp
+  if h : str.toList.all (· ∈ Slug.validChars) then
+    isTrue h
+  else
+    isFalse h
 
+@[grind]
 theorem Slug.wf_push (c str) : c ∈ validChars → WF str → WF (str.push c) := by
   unfold WF
   cases str
   intro mem wf
+  simp only [String.toList, List.all_eq_true, decide_eq_true_eq] at wf
   simp only [String.toList, String.data_push, List.all_append, List.all_cons, List.all_nil,
     Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-  and_intros <;> simp at wf <;> assumption
+  grind only
 
+@[grind]
 theorem Slug.wf_append (str1 str2) : WF str1 → WF str2 → WF (str1 ++ str2) := by
   unfold WF
   cases str1; cases str2
   intro wf1 wf2
   simp only [String.toList, String.data_append, List.all_append, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
   simp only [String.toList, List.all_eq_true, decide_eq_true_eq] at wf1 wf2
-  and_intros <;> assumption
+  grind only
+
+@[simp]
+theorem Slug.decide_WF_eq_wf (s : String) : (s.toList.all (fun x => decide (x ∈ validChars)) = true) = WF s := by
+  rfl
+
+@[grind, simp]
+theorem Slug.wf_forall : WF s → c ∈ s.data → c ∈ validChars := by
+  intro wf h
+  simp_all [WF]
 
 theorem Slug.asSlug_loop_valid : WF acc → WF (asSlug.loop iter acc) := by
   intro wfAcc
-  induction iter, acc using asSlug.loop.induct <;> unfold asSlug.loop <;> simp [*]
-  case case2 iter acc notEnd c ih =>
+  fun_induction asSlug.loop with try assumption
+  | case2 iter acc notEnd c ih =>
     apply ih
     unfold WF
-    simp only [WF, String.toList, List.all_eq_true, decide_eq_true_eq] at wfAcc
-    split
-    . simp only [String.toList, String.data_push, List.all_append, List.all_cons, List.all_nil,
-      Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-      and_intros <;> assumption
-    . split
-      . simp only [String.toList, ↓Char.isValue, String.data_push, List.all_append, List.all_cons,
-        List.all_nil, Bool.and_true, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq]
-        and_intros
-        . assumption
-        . simp [validChars]
-      . simp only [String.toList, String.data_append, List.all_append, Bool.and_eq_true,
-        List.all_eq_true, decide_eq_true_eq]
-        and_intros
-        . assumption
-        . intro c' mem
-          have : WF (mangle c) := wf_mangle
-          simp only [WF, String.toList, List.all_eq_true, decide_eq_true_eq] at this
-          simp [*]
+    (repeat' split) <;>
+      simp [*] <;>
+      grind only [=_ List.contains_iff_mem, List.contains_eq_mem, mangle_wf, wf_forall, mangle_mem_valid, wf_append, cases Or]
 
+@[grind]
 theorem Slug.asSlug_valid : WF (asSlug str) := by
   unfold asSlug
   apply asSlug_loop_valid

src/verso-blog/VersoBlog.lean

@@ -21,7 +21,6 @@ import Verso.Doc.Suggestion
 import Verso.Hover
 import Verso.WithoutAsync
 open Verso.Output Html
-open Lean (RBMap)
 
 namespace Verso.Genre.Blog
 

src/verso-blog/VersoBlog/Basic.lean

@@ -178,7 +178,7 @@ structure TraverseContext where
   components : Components
 
 structure TraverseState where
-  usedIds : Lean.RBMap (List String) (HashSet String) compare := {}
+  usedIds : Std.HashMap (List String) (HashSet String) := {}
   targets : Lean.NameMap Blog.Info.Target := {}
   blogs : Lean.NameMap Blog.Info.ArchivesMeta := {}
   refs : Lean.NameMap Blog.Info.Ref := {}
@@ -334,7 +334,7 @@ defmethod BlogPost.summary (post : BlogPost) : Array (Block Post) := Id.run do
 
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
   let mut idStr := mangle (toString hint)
-  match state.usedIds.find? path with
+  match state.usedIds[path]? with
   | none => return idStr
   | some used =>
     while used.contains idStr do

src/verso-blog/VersoBlog/Component.lean

@@ -138,8 +138,8 @@ deriving TypeName
 
 open Lean in
 def Components.fromLists (blocks : List (Name × BlockComponent)) (inlines : List (Name × InlineComponent)) : Components where
-  blocks := .fromList (blocks.map fun (x, b) => (x, Dynamic.mk b)) _
-  inlines := .fromList (inlines.map fun (x, b) => (x, Dynamic.mk b)) _
+  blocks := .ofList (blocks.map fun (x, b) => (x, Dynamic.mk b)) _
+  inlines := .ofList (inlines.map fun (x, b) => (x, Dynamic.mk b)) _
 
 open Lean in
 private def nameAndDef [Monad m] [MonadRef m] [MonadQuotation m] (ext : Name × Name) : m Term := do

src/verso-blog/VersoBlog/Component/Ext.lean

@@ -15,7 +15,7 @@ initialize blockComponentExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }
 
 initialize inlineComponentExt :
@@ -25,5 +25,5 @@ initialize inlineComponentExt :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun as (src, tgt) => as.insert src tgt,
     exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
   }

src/verso-blog/VersoBlog/Template.lean

@@ -17,8 +17,7 @@ import Verso.Output.Html
 import Verso.Output.Html.CssVars
 import Verso.Code
 
-open Std (HashSet)
-open Lean (RBMap)
+open Std (HashSet TreeMap)
 
 open Verso Doc Output Html HtmlT
 open Verso.Genre Blog
@@ -52,9 +51,9 @@ instance : Coe Html Template.Params.Val where
    | other => ⟨.mk other, #[]⟩
 
 
-def Params := RBMap String Params.Val compare
+def Params := TreeMap String Params.Val
 
-instance : EmptyCollection Params := inferInstanceAs <| EmptyCollection (RBMap _ _ _)
+instance : EmptyCollection Params := inferInstanceAs <| EmptyCollection (TreeMap _ _ _)
 
 inductive Error where
   | missingParam (param : String)
@@ -258,16 +257,16 @@ namespace Verso.Genre.Blog.Template
 namespace Params
 
 def ofList (params : List (String × Val)) : Params :=
-  Lean.RBMap.ofList params
+  Std.TreeMap.ofList params _
 
 def toList (params : Params) : List (String × Val) :=
-  Lean.RBMap.toList params
+  Std.TreeMap.toList params
 
 def insert (params : Params) (key : String) (val : Val) : Params :=
-  Lean.RBMap.insert params key val
+  Std.TreeMap.insert params key val
 
 def erase (params : Params) (key : String) : Params :=
-  Lean.RBMap.erase params key
+  Std.TreeMap.erase params key
 
 
 end Params
@@ -287,15 +286,15 @@ namespace Template
 
 def param? [TypeName α] (key : String) : TemplateM (Option α) := do
   let ctx ← readThe Context
-  match ctx.params.find? key with
+  match ctx.params.get? key with
   | none => return none
   | some val =>
     if let some v := val.get? (α := α) then return (some v)
     else throw <| .wrongParamType key (TypeName.typeName α)
 
 
 def param [TypeName α] (key : String) : TemplateM α := do
-  match (← read).params.find? key with
+  match (← read).params.get? key with
   | none => throw <| .missingParam key
   | some val =>
     if let some v := val.get? (α := α) then return v

src/verso-manual/VersoManual/Basic.lean

@@ -222,7 +222,7 @@ instance : BEq Domains where
     x.all fun k v => y.find? k |>.isEqSome v
 
 instance : GetElem Domains Name Domain (fun ds d => ds.contents.contains d) where
-  getElem ds d _ok := ds.contents.find! d
+  getElem ds d _ok := ds.contents.get! d
 
 instance : GetElem? Domains Name Domain (fun ds d => ds.contents.contains d) where
   getElem? ds d := ds.contents.find? d