Merge pull request #37 from leanprover-community/bump/nightly-2024-10-17

chore: adaptations for nightly-2024-10-17

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)

lake-manifest.json

@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "389fb58a2ff92e1ede0db37b1fedcb9a6162df94",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "importGraph",

lakefile.toml

@@ -14,7 +14,7 @@ rev = "main"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "main"
+rev = "nightly-testing"
 
 [[lean_lib]]
 name = "ImportGraph"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc1
+leanprover/lean4:nightly-2024-10-17