Merge pull request #16 from adomani/patch-1

rename: `#minimize_imports` to `#min_imports`

ImportGraph/Imports.lean

@@ -13,7 +13,7 @@ import ImportGraph.RequiredModules
 Provides the commands
 
 * `#redundant_imports` which lists any transitively redundant imports in the current module.
-* `#minimize_imports` which attempts to construct a minimal set of imports for the declarations
+* `#min_imports` which attempts to construct a minimal set of imports for the declarations
   in the current file.
   (Must be run at the end of the file. Tactics and macros may result in incorrect output.)
 * `#find_home decl` suggests files higher up the import hierarchy to which `decl` could be moved.
@@ -213,11 +213,16 @@ This must be run at the end of the file,
 and is not aware of syntax and tactics,
 so the results will likely need to be adjusted by hand.
 -/
-elab "#minimize_imports" : command => do
+elab "#min_imports" : command => do
   let imports := (← getEnv).minimalRequiredModules.qsort Name.lt
     |>.toList.map (fun n => "import " ++ n.toString)
   logInfo <| Format.joinSep imports "\n"
 
+-- deprecated since 2024-07-06
+elab "#minimize_imports" : command => do
+  logWarning m!"'#minimize_imports' is deprecated: please use '#min_imports'"
+  Elab.Command.elabCommand (← `(command| #min_imports))
+
 /--
 Find locations as high as possible in the import hierarchy
 where the named declaration could live.

test/Imports.lean

@@ -16,13 +16,12 @@ ImportGraph.RequiredModules
 
 /-- info: import ImportGraph.Imports -/
 #guard_msgs in
-#minimize_imports
+#min_imports
 
 /-- info: [ImportGraph.Imports] -/
 #guard_msgs in
 #find_home importTest
 
-
 open Elab Command in
 elab "#my_test" : command => do
   -- functionality of `#redundant_imports`