chore: adaptations for nightly-2025-07-22

Author: mathlib4-bot

Batteries/CodeAction/Attr.lean

@@ -63,7 +63,7 @@ def TacticCodeActions.insert (self : TacticCodeActions)
     { self with onAnyTactic := self.onAnyTactic.push action }
   else
     { self with onTactic := tacticKinds.foldl (init := self.onTactic) fun m a =>
-        m.insert a ((m.findD a #[]).push action) }
+        m.insert a ((m.getD a #[]).push action) }
 
 /-- An extension which collects all the tactic code actions. -/
 initialize tacticSeqCodeActionExt :

Batteries/Data/NameSet.lean

@@ -12,20 +12,12 @@ instance : Singleton Name NameSet where
   singleton := fun n => (∅ : NameSet).insert n
 
 instance : Union NameSet where
-  union := fun s t => s.fold (fun t n => t.insert n) t
+  union := fun s t => s.foldl (fun t n => t.insert n) t
 
 instance : Inter NameSet where
-  inter := fun s t => s.fold (fun r n => if t.contains n then r.insert n else r) {}
+  inter := fun s t => s.foldl (fun r n => if t.contains n then r.insert n else r) {}
 
 instance : SDiff NameSet where
-  sdiff := fun s t => t.fold (fun s n => s.erase n) s
-
-/-- Create a `Lean.NameSet` from a `List`. This operation is `O(n)` in the length of the list. -/
-def ofList (l : List Name) : NameSet :=
-  l.foldl (fun s n => s.insert n) {}
-
-/-- Create a `Lean.NameSet` from an `Array`. This operation is `O(n)` in the size of the array. -/
-def ofArray (a : Array Name) : NameSet :=
-  a.foldl (fun s n => s.insert n) {}
+  sdiff := fun s t => t.foldl (fun s n => s.erase n) s
 
 end Lean.NameSet

Batteries/Data/String/Lemmas.lean

@@ -10,6 +10,10 @@ import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
 import Std.Classes.Ord.String -- Not needed here, but imported to ensure instance names don't clash.
 
+
+-- Commented out temporarily as this is broken on nightly-2025-07-22
+/-
+
 namespace String
 
 -- TODO(kmill): add `@[ext]` attribute to `String.ext` in core.
@@ -1089,3 +1093,5 @@ theorem dropWhile_eq (p : Char → Bool) (s : String) : s.dropWhile p = ⟨s.1.d
     (s.dropWhile p).1 = s.1.dropWhile p := by rw [dropWhile_eq]
 
 end String
+
+-/

Batteries/Tactic/HelpCmd.lean

@@ -49,8 +49,8 @@ syntax withPosition("#help " colGt &"option" (colGt ppSpace Parser.rawIdent)?) :
 
 private def elabHelpOption (id : Option Ident) : CommandElabM Unit := do
   let id := id.map (·.raw.getId.toString false)
-  let mut decls : Lean.RBMap _ _ compare := {}
-  for (name, decl) in show Lean.RBMap .. from ← getOptionDecls do
+  let mut decls : Std.TreeMap _ _ compare := {}
+  for (name, decl) in show NameMap OptionDecl from ← getOptionDecls do
     let name := name.toString false
     if let some id := id then
       if !id.isPrefixOf name then
@@ -96,7 +96,7 @@ syntax withPosition("#help " colGt (&"attr" <|> &"attribute")
 
 private def elabHelpAttr (id : Option Ident) : CommandElabM Unit := do
   let id := id.map (·.raw.getId.toString false)
-  let mut decls : Lean.RBMap _ _ compare := {}
+  let mut decls : Std.TreeMap _ _ compare := {}
   /-
   #adaptation_note
   On nightly-2024-06-21, added the `.toList` here:
@@ -179,7 +179,7 @@ syntax withPosition("#help " colGt &"cats" (colGt ppSpace Parser.rawIdent)?) : c
 
 private def elabHelpCats (id : Option Ident) : CommandElabM Unit := do
   let id := id.map (·.raw.getId.toString false)
-  let mut decls : Lean.RBMap _ _ compare := {}
+  let mut decls : Std.TreeMap _ _ compare := {}
   for (name, cat) in (Parser.parserExtension.getState (← getEnv)).categories do
     let name := name.toString false
     if let some id := id then
@@ -221,8 +221,8 @@ syntax withPosition("#help " colGt &"cat" "+"? colGt ident
 
 private def elabHelpCat (more : Option Syntax) (catStx : Ident) (id : Option String) :
     CommandElabM Unit := do
-  let mut decls : Lean.RBMap _ _ compare := {}
-  let mut rest : Lean.RBMap _ _ compare := {}
+  let mut decls : Std.TreeMap _ _ compare := {}
+  let mut rest : Std.TreeMap _ _ compare := {}
   let catName := catStx.getId.eraseMacroScopes
   let some cat := (Parser.parserExtension.getState (← getEnv)).categories.find? catName
     | throwErrorAt catStx "{catStx} is not a syntax category"
@@ -236,7 +236,7 @@ private def elabHelpCat (more : Option Syntax) (catStx : Ident) (id : Option Str
         if !id.isPrefixOf tk then
           continue
       used := true
-      decls := decls.insert tk ((decls.findD tk #[]).push k)
+      decls := decls.insert tk ((decls.getD tk #[]).push k)
     if !used && id.isNone then
       rest := rest.insert (k.toString false) k
   let mut msg := MessageData.nil

Batteries/Tactic/Lint/Basic.lean

@@ -84,7 +84,7 @@ initialize batteriesLinterExt :
     addImportedFn := fun nss => pure <|
       nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
     addEntryFn
-    exportEntriesFn := fun es => es.fold (fun a _ e => a.push e) #[]
+    exportEntriesFn := fun es => es.foldl (fun a _ e => a.push e) #[]
   }
 
 /--

Batteries/Tactic/PrintDependents.lean

@@ -110,7 +110,7 @@ elab tk:"#print" &"dependents" ids:(ppSpace colGt ident)* : command => do
       | some (ConstantInfo.recInfo v)    => v.type.getUsedConstants
       | some (ConstantInfo.inductInfo v) => v.type.getUsedConstants ++ v.ctors
       | _                                => #[]
-      for c in RBTree.fromArray consts Name.cmp do
+      for c in Std.TreeSet.ofArray consts Name.cmp do
         if state.result.find? c = some true then
           msg := msg ++ m!"{MessageData.ofConst (← mkConstWithLevelParams c)} "
     return msg

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-07-21
+leanprover/lean4:nightly-2025-07-22