Commit 2025-02-11 21:00 b920ed92

View on Github →

refactor(Cache): use the Lean search path instead of lake-manifest to determine Mathlib root. (#21666) Instead of manually parsing the lake manifest, use the search path from the env variable LEAN_SRC_PATH (using initSrcSearchPath) to find where the file Mathlib.lean is located.

Estimated changes