Merge pull request #23 from leanprover-community/nightly-testing

chore: move to v4.11.0-rc1

ImportGraph/Cli.lean

@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 import Cli.Basic
 import Batteries.Lean.IO.Process
-import Batteries.Lean.Util.Path
 import ImportGraph.CurrentModule
 import ImportGraph.Imports
 import ImportGraph.Lean.Name

ImportGraph/Lean/Name.lean

@@ -5,9 +5,8 @@ Authors: Jon Eugster
 -/
 import Lean.Data.Name
 import Lean.CoreM
-import Batteries.Data.HashMap.Basic
-import Batteries.Lean.SMap
 import Lean.Meta.Match.MatcherInfo
+import Std.Data.HashMap
 
 /-!
 TODO: Some declarations in this file are duplicated from mathlib, but especially `isBlacklisted`
@@ -46,12 +45,12 @@ gathered together into a `HashMap` according to the module they are defined in.
 
 Note: copied from `Mathlib.Lean.Name`
 -/
-def allNamesByModule (p : Name → Bool) : CoreM (Batteries.HashMap Name (Array Name)) := do
-  (← getEnv).constants.foldM (init := Batteries.HashMap.empty) fun names n _ => do
+def allNamesByModule (p : Name → Bool) : CoreM (Std.HashMap Name (Array Name)) := do
+  (← getEnv).constants.foldM (init := Std.HashMap.empty) fun names n _ => do
     if p n && !(← isBlackListed n) then
       let some m ← findModuleOf? n | return names
-      -- TODO use `Batteries.HashMap.modify` when we bump `batteries` (or `alter` if that is written).
-      match names.find? m with
+      -- TODO use `modify`/`alter` when available
+      match names[m]? with
       | some others => return names.insert m (others.push n)
       | none => return names.insert m #[n]
     else

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "rev": "021e272cb5cdcc82b7e1e760fe915ff2f64169ad",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc1