From ebcdcf2afee0176cd3cf5452641fe5c11fcda827 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 11 Nov 2024 09:22:20 +0100 Subject: [PATCH] chore: move `Core.withImportModules` to `Imports.lean` This way only `main` is defined in UnusedTransitiveImports.lean, and hence it should never be necessary to import `UnusedTransitiveImports`. --- ImportGraph/Imports.lean | 6 ++++++ ImportGraph/UnusedTransitiveImports.lean | 6 ------ 2 files changed, 6 insertions(+), 6 deletions(-) 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 ...`