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.