diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean index 15caa91..ba2f6d6 100644 --- a/ImportGraph/Imports.lean +++ b/ImportGraph/Imports.lean @@ -185,6 +185,12 @@ def unusedTransitiveImports (amongst : List Name) (verbose : Bool := false) : Co let unused := (transitiveImports.find? n).getD {} \ (transitivelyRequired.find? n |>.getD {}) amongst.filter (fun m => unused.contains m)) +def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do + searchPathRef.set compile_time_search_path% + unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024) + fun env => Prod.fst <$> Core.CoreM.toIO + (ctx := { fileName := "", fileMap := default }) (s := { env := env }) do f + /-- Return the redundant imports (i.e. those transitively implied by another import) of a specified module (or the current module if `none` is specified). diff --git a/ImportGraph/UnusedTransitiveImports.lean b/ImportGraph/UnusedTransitiveImports.lean index 4743757..bb91739 100644 --- a/ImportGraph/UnusedTransitiveImports.lean +++ b/ImportGraph/UnusedTransitiveImports.lean @@ -2,12 +2,6 @@ import ImportGraph.Imports open Lean -def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do - searchPathRef.set compile_time_search_path% - unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024) - fun env => Prod.fst <$> Core.CoreM.toIO - (ctx := { fileName := "", fileMap := default }) (s := { env := env }) do f - /-- `lake exe unused_transitive_imports m1 m2 ...`