diff --git a/ImportGraph/Gexf.lean b/ImportGraph/Gexf.lean index b1d6c0c..f418fc6 100644 --- 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 index 15caa91..ad3597a 100644 --- 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 index a946e60..d4ed67a 100644 --- 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 index f613939..05636e1 100644 --- 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 index 0bef727..44435e7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc1 +leanprover/lean4:nightly-2024-11-14 \ No newline at end of file