Commit 2025-02-27 14:58 a1b038bb
View on Github →refactor(Cache): rewrite getFileImports
to use search path and return module names and source file location (#21815)
Rewrite getFileImports
to not use getPackageDirs
anymore.
Additionally, getFileImports
now returns module names like Mathlib.Data.Set.Basic
and resolved .lean
file locations instead of non-resolved file names (Mathlib/Data/Set/Basic.lean
) like it used to. This is in preparation for #21238.
This PR should not change any behaviour in how cache
works.