From df16f3a38c3d21a911436afb4c4250aaa9c55d13 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 16 Oct 2024 20:56:58 +1100
Subject: [PATCH 1/2] fixes for leanprover/lean4#5731

---
 ImportGraph/Imports.lean | 6 +++---
 lean-toolchain           | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean
index 14705b3..85193dc 100644
--- a/ImportGraph/Imports.lean
+++ b/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)
diff --git a/lean-toolchain b/lean-toolchain
index b1b73fe..dc4bb32 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc1
\ No newline at end of file
+leanprover/lean4-pr-releases:pr-release-5731
\ No newline at end of file

From c2913a0d46da4699971b7a6d45190e562584e0ba Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 16 Oct 2024 20:59:23 +1100
Subject: [PATCH 2/2] .

---
 lake-manifest.json | 4 ++--
 lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 6631554..cfd9030 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "b4cb0a5212271f661c27f52ef0923be1ec3ddd0b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "lean-pr-testing-5731",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "importGraph",
diff --git a/lakefile.toml b/lakefile.toml
index 5d47ad9..8ebb43e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,7 +14,7 @@ rev = "main"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "main"
+rev = "lean-pr-testing-5731"
 
 [[lean_lib]]
 name = "ImportGraph"