Commit 2023-11-28 00:02 7cc262f3
View on Github →fix(Cache): correctly handle local copies of Mathlib (#8662)
This parses the lake-manifest to work out where mathlib is.
Previously this assumed it was in .lake/packages, but this is only true of git packages. As a result, it would fail with:
uncaught exception: no such file or directory (error code: 2)
file: .lake/packages/mathlib/lakefile.lean
Tested on a blank project created with lake new test math, with require mathlib from "../mathlib4" in the lakefile.