Merge pull request #42 from leanprover-community/nightly-testing

chore: bump toolchain to v4.14.0-rc1

ImportGraph/CurrentModule.lean

@@ -5,7 +5,7 @@ Authors: Jon Eugster
 -/
 import Lake.Load.Manifest
 
-open Lake
+open Lean (Name)
 
 namespace ImportGraph
 

ImportGraph/Imports.lean

@@ -131,7 +131,7 @@ partial
 def transitiveFilteredUpstream (node : Name) (graph : NameMap (Array Name))
     (filter : Name → Bool) (replacement : Option Name := none):
     List Name :=
-  (graph.find! node).toList.bind fun source =>
+  (graph.find! node).toList.flatMap fun source =>
     ( if filter source then
         -- Add the transitive edges going through the filtered node `source`.
         -- If there is a replacement node, add an additional edge `repl → node`.
@@ -156,12 +156,12 @@ def filterGraph (graph : NameMap (Array Name)) (filter : Name → Bool)
     (replacement : Option Name := none) : NameMap (Array Name) :=
   -- Create a list of all files imported by any of the filtered files
   -- and remove all imports starting with `Mathlib` to avoid loops.
-  let replImports := graph.toList.bind
+  let replImports := graph.toList.flatMap
     (fun ⟨n, i⟩ => if filter n then i.toList else [])
     |>.eraseDups |>.filter (¬ Name.isPrefixOf `Mathlib ·) |>.toArray
   let graph := graph.filterMap (fun node edges => if filter node then none else some <|
     -- If the node `node` is not filtered, modify the `edges` going into `node`.
-    edges.toList.bind (fun source =>
+    edges.toList.flatMap (fun source =>
       if filter source then
         transitiveFilteredUpstream source graph filter (replacement := replacement)
       else [source]) |>.eraseDups.toArray)

ImportGraphTest/Imports.lean

@@ -36,12 +36,7 @@ elab "#unused_transitive_imports" names:ident* : command => do
     if !u.isEmpty then
     logInfo <| s!"Transitively unused imports of {n}:\n{"\n".intercalate (u.map (fun i => s!"  {i}"))}"
 
--- This test case can be removed after nightly-2024-10-24, because these imports have been cleaned up.
--- It should be replaced with another test case!
 /--
-info: Transitively unused imports of Init.Control.StateRef:
-  Init.System.IO
----
 info: Transitively unused imports of Init.System.IO:
   Init.Control.Reader
 -/
@@ -55,14 +50,6 @@ info: Transitively unused imports of ImportGraphTest.Used:
 #guard_msgs in
 #unused_transitive_imports ImportGraphTest.Used ImportGraphTest.Unused Init.Control.Reader
 
--- This is a spurious unused transitive import, because it relies on notation from `Init.Core`.
-/--
-info: Transitively unused imports of Init.Control.Basic:
-  Init.Core
--/
-#guard_msgs in
-#unused_transitive_imports Init.Control.Basic Init.Core
-
 elab "#transitivelyRequiredModules_test" : command => do
   let env ← getEnv
   let unused ← liftCoreM <| env.transitivelyRequiredModules `ImportGraph.RequiredModules

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc1