Skip to content

Commit

Permalink
merge lean-pr-testing-5731
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 17, 2024
2 parents e314ce0 + c2913a0 commit 6b65715
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
6 changes: 3 additions & 3 deletions ImportGraph/Imports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2024-10-17
leanprover/lean4:nightly-2024-10-17

0 comments on commit 6b65715

Please sign in to comment.