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.