Merge pull request #6 from leanprover-community/batteries

chore: update Std -> Batteries

ImportGraph/Cli.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Cli.Basic
-import Std.Lean.IO.Process
-import Std.Lean.Util.Path
+import Batteries.Lean.IO.Process
+import Batteries.Lean.Util.Path
 import ImportGraph.CurrentModule
 import ImportGraph.Imports
 import ImportGraph.Lean.Name

ImportGraph/Imports.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
-import Std.Lean.NameMap
+import Batteries.Lean.NameMap
 import ImportGraph.RequiredModules
 
 /-!

ImportGraph/Lean/Name.lean

@@ -5,19 +5,18 @@ Authors: Jon Eugster
 -/
 import Lean.Data.Name
 import Lean.CoreM
-import Std.Data.HashMap.Basic
-import Std.Lean.Name
-import Std.Lean.SMap
+import Batteries.Data.HashMap.Basic
+import Batteries.Lean.Name
+import Batteries.Lean.SMap
 import Lean.Meta.Match.MatcherInfo
 
 /-!
 TODO: Some declarations in this file are duplicated from mathlib, but especially `isBlacklisted`
-is deemed to specific for upstreaming to Std.
+is deemed to specific for upstreaming to Batteries.
 -/
 namespace Lean.Name
 
 open Lean Meta Elab
-open Std
 
 namespace ImportGraph
 
@@ -48,11 +47,11 @@ 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 (Std.HashMap Name (Array Name)) := do
-  (← getEnv).constants.foldM (init := Std.HashMap.empty) fun names n _ => do
+def allNamesByModule (p : Name → Bool) : CoreM (Batteries.HashMap Name (Array Name)) := do
+  (← getEnv).constants.foldM (init := Batteries.HashMap.empty) fun names n _ => do
     if p n && !(← isBlackListed n) then
       let some m ← findModuleOf? n | return names
-      -- TODO use `Std.HashMap.modify` when we bump Std4 (or `alter` if that is written).
+      -- TODO use `Batteries.HashMap.modify` when we bump `batteries` (or `alter` if that is written).
       match names.find? m with
       | some others => return names.insert m (others.push n)
       | none => return names.insert m #[n]

lake-manifest.json

@@ -10,11 +10,11 @@
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
-   "name": "std",
+   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,

lakefile.toml

@@ -7,8 +7,8 @@ git = "https://github.com/leanprover/lean4-cli"
 rev = "main"
 
 [[require]]
-name = "std"
-git = "https://github.com/leanprover/std4"
+name = "batteries"
+git = "https://github.com/leanprover-community/batteries"
 rev = "main"
 
 [[lean_lib]]