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.

Estimated changes