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.