Merge pull request #49 from grunweg/MR-bump-batterires

chore: update for upstreamed NameSet API

ImportGraph/Gexf.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster
 -/
 
-import Lean
+import Lean.Data.Name
+import Lean.AuxRecursor
+import Lean.MonadEnv
+import Lean.Meta.Match.MatcherInfo
 
 open Lean
 

ImportGraph/Imports.lean

@@ -3,7 +3,10 @@ Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-import Lean
+import Lean.Elab.Command
+import Lean.Util.SearchPath
+import Lean.Server.GoTo
+import Lean.Widget.UserWidget
 import ImportGraph.RequiredModules
 
 /-!

ImportGraph/RequiredModules.lean

@@ -3,30 +3,11 @@ Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-import Lean
-
-
-namespace Lean.NameSet
-
-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
-
-instance : Inter NameSet where
-  inter := fun s t => s.fold (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
-
-def ofList (l : List Name) : NameSet :=
-  l.foldl (fun s n => s.insert n) {}
-
-def ofArray (a : Array Name) : NameSet :=
-  a.foldl (fun s n => s.insert n) {}
-
-end Lean.NameSet
+import Lean.CoreM
+import Lean.Data.NameMap
+import Lean.Environment
+import Lean.Util.FoldConsts
+import Batteries.Data.NameSet
 
 namespace Lean
 
@@ -40,6 +21,8 @@ def Environment.getModuleFor? (env : Environment) (declName : Name) : Option Nam
       none
   | some idx => env.header.moduleNames[idx.toNat]!
 
+open Lean
+
 /--
 Return the names of the modules in which constants used in the specified declaration were defined.
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "rev": "66225aab4f6bd1687053b03916105f7cab140507",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.toml

@@ -14,7 +14,7 @@ rev = "main"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "v4.16.0-rc1"
+rev = "main"
 
 [[lean_lib]]
 name = "ImportGraph"