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.

Estimated changes