Commit 2024-01-10 11:53 1fb4b03b

View on Github →

refactor: split ImportGraph into its own package. (#9169) Remove ImportGraph from the mathlib repo and add it as a dependency.

Estimated changes

Deleted ImportGraph/Main.lean

deleted def asDotGraph

deleted def graph

deleted def importGraphCLI

deleted def main

Modified Mathlib.lean

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Environment.getModuleFor?

deleted def Lean.Environment.requiredModules

deleted def Lean.Name.requiredModules

Modified Mathlib/Lean/Name.lean

deleted def getModule

Modified Mathlib/Tactic/Common.lean

Deleted Mathlib/Util/Imports.lean

deleted def Lean.Environment.importsOf

deleted def Lean.Environment.minimalRequiredModules

deleted def Lean.Name.findHome

deleted def Lean.NameMap.downstreamOf

deleted def Lean.NameMap.filterGraph

deleted def Lean.NameMap.transitiveFilteredUpstream

deleted def Lean.NameMap.transitiveReduction

deleted def Lean.NameMap.upstreamOf

deleted def redundantImports

Modified lake-manifest.json

Modified lakefile.lean

Deleted test/Imports.lean