From 4f369e537794bdf931bee9f9bc79dbf74c5a54d3 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Thu, 9 Jan 2025 18:03:01 +0100
Subject: [PATCH 1/2] chore: avoid blanket import Lean

---
 ImportGraph/Gexf.lean            | 5 ++++-
 ImportGraph/Imports.lean         | 5 ++++-
 ImportGraph/RequiredModules.lean | 8 ++++++--
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/ImportGraph/Gexf.lean b/ImportGraph/Gexf.lean
index ee83bc0..357f9a9 100644
--- a/ImportGraph/Gexf.lean
+++ b/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
 
diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean
index fa5902c..61db1e1 100644
--- a/ImportGraph/Imports.lean
+++ b/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
 
 /-!
diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean
index b3a91e1..d4de2e8 100644
--- a/ImportGraph/RequiredModules.lean
+++ b/ImportGraph/RequiredModules.lean
@@ -3,8 +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.CoreM
+import Lean.Data.NameMap
+import Lean.Environment
+import Lean.Util.FoldConsts
 
 namespace Lean.NameSet
 
@@ -40,6 +42,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.
 

From 8537807fb7c1d6b58cb8ccf2af7c7bad13273197 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Thu, 9 Jan 2025 18:05:23 +0100
Subject: [PATCH 2/2] chore: some NameSet API has been upstreamed

---
 ImportGraph/RequiredModules.lean | 23 +----------------------
 lake-manifest.json               |  4 ++--
 lakefile.toml                    |  2 +-
 3 files changed, 4 insertions(+), 25 deletions(-)

diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean
index d4de2e8..868390e 100644
--- a/ImportGraph/RequiredModules.lean
+++ b/ImportGraph/RequiredModules.lean
@@ -7,28 +7,7 @@ import Lean.CoreM
 import Lean.Data.NameMap
 import Lean.Environment
 import Lean.Util.FoldConsts
-
-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 Batteries.Data.NameSet
 
 namespace Lean
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 0d23030..8389c01 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/lakefile.toml b/lakefile.toml
index 3aaa8a5..f613939 100644
--- a/lakefile.toml
+++ b/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"