bump toolchain; remove deleted imports

leanprover-community · Nov 14, 2024 · 0fc755a · 0fc755a
1 parent 5ee6767
commit 0fc755a
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 7 deletions.
diff --git a/ImportGraph/Gexf.lean b/ImportGraph/Gexf.lean
@@ -5,7 +5,6 @@ Authors: Jon Eugster
 -/
 
 import Lean
-import Batteries.Lean.NameMap
 import Batteries.Tactic.OpenPrivate
 
 open Lean

diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Lean
-import Batteries.Lean.NameMap
 import ImportGraph.RequiredModules
 
 /-!

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "2ed85f320805f9d3a455ced3b181562ed146bc20",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "importGraph",

diff --git a/lakefile.toml b/lakefile.toml
@@ -14,7 +14,7 @@ rev = "main"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "main"
+rev = "nightly-testing"
 
 [[lean_lib]]
 name = "ImportGraph"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:nightly-2024-11-14
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc1
		leanprover/lean4:nightly-2024-11-14