Skip to content

Commit

Permalink
use lexicographic sorting
Browse files Browse the repository at this point in the history
Co-authored-by: Moritz Firsching <[email protected]>
  • Loading branch information
joneugster and mo271 committed Aug 7, 2024
1 parent 68cd8ae commit 9fc834c
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion ImportGraph/Imports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,10 @@ def Lean.Environment.minimalRequiredModules (env : Environment) : Array Name :=
let redundant := findRedundantImports env required
required.filter fun n => ¬ redundant.contains n

/-- Lexikographic order of Names for sorting imports -/
def sortImportsLt : Name → Name → Bool
| a, b => a.toString < b.toString

/--
Try to compute a minimal set of imports for this file,
by analyzing the declarations.
Expand All @@ -214,7 +218,7 @@ and is not aware of syntax and tactics,
so the results will likely need to be adjusted by hand.
-/
elab "#min_imports" : command => do
let imports := (← getEnv).minimalRequiredModules.qsort Name.lt
let imports := (← getEnv).minimalRequiredModules.qsort sortImportsLt
|>.toList.map (fun n => "import " ++ n.toString)
logInfo <| Format.joinSep imports "\n"

Expand Down

0 comments on commit 9fc834c

Please sign in to comment.