Commit 2025-02-24 14:14 42e56d74

View on Github →

refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817)

Estimated changes

Modified Cache/Hashing.lean

Modified Cache/IO.lean

deleted def Cache.IO.getPackageDir

added def Cache.IO.getSrcDir

Modified Cache/Lean.lean

added def Lean.Name.fromComponents

added def Lean.SearchPath.findWithExtBase