update

leanprover-community · Feb 17, 2025 · 4299ce8 · 4299ce8
1 parent 62b4ae0
commit 4299ce8
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/ImportGraph/UnusedTransitiveImports.lean b/ImportGraph/UnusedTransitiveImports.lean
@@ -3,7 +3,7 @@ import ImportGraph.Imports
 open Lean
 
 def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do
-  searchPathRef.set compile_time_search_path%
+  initSearchPath (← findSysroot)
   unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024)
     fun env => Prod.fst <$> Core.CoreM.toIO
         (ctx := { fileName := "<CoreM>", fileMap := default }) (s := { env := env }) do f

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a6bd8a6497ac71aa33eb77a777c468b8d5f218e",
+   "rev": "38af7c17fedc637d6cb491d557c82ac6477a8295",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "d835296a6149acb9bd2ff65ec01b728b9cc99a1c",
+   "rev": "5bf2647dfadce4e48961532d6162d46558be6731",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "importGraph",

diff --git a/lakefile.toml b/lakefile.toml
@@ -9,7 +9,7 @@ testRunner = "ImportGraphTest"
 [[require]]
 name = "Cli"
 scope = "leanprover"
-rev = "main"
+rev = "nightly-testing"
 
 [[require]]
 name = "batteries"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-01-30
+leanprover/lean4:nightly-2025-02-17
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2025-01-30
		leanprover/lean4:nightly-2025-02-17