Skip to content

Commit

Permalink
chore: avoid RBTree.ofList in Cache (#3507)
Browse files Browse the repository at this point in the history
Unlike fromList, ofList is not tail recursive and hence susceptible to stack overflow.
  • Loading branch information
Ruben-VandeVelde committed Apr 19, 2023
1 parent c9a607f commit d7f8e10
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Cache/IO.lean
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ def packCache (hashMap : HashMap) (overwrite : Bool) : IO $ Array String := do
/-- Gets the set of all cached files -/
def getLocalCacheSet : IO $ Lean.RBTree String compare := do
let paths ← getFilesWithExtension CACHEDIR "gz"
return .ofList (paths.data.map (·.withoutParent CACHEDIR |>.toString))
return .fromList (paths.data.map (·.withoutParent CACHEDIR |>.toString)) _

def isPathFromMathlib (path : FilePath) : Bool :=
match path.components with
Expand Down

0 comments on commit d7f8e10

Please sign in to comment.