fix: keep Lake workspace axioms out of library imports

ImportGraph/Lake.lean

@@ -5,149 +5,24 @@ Authors: Thomas R. Murrills
 -/
 module
 
+public import ImportGraph.Util.Modules
 public import Lake.Config.Workspace
 
 import Lake.Load.Workspace
 
-/-
-# Extra `Lake` utilities
-
-This file defines a few convenient lake utilities, notably:
+/-!
+# Lake workspace loading
 
-- `for ... in ... do` instances that allow iterating through lake modules:
-  - Given `dir : System.FilePath`, `for (mod, dirEntry) in dir.modules (root := ...) do` iterates
-    in modules under the directory `dir` (descending into subdirectories)
-  - Given `glob : Lake.Glob`, `for (mod, dirEntry) in glob.modulesIn dir do` iterates through all
-    modules in `dir` matching `glob`.
-- `ImportGraph.IO.getWorkspace : IO Lake.Workspace`: a version of
-  `Lake.loadWorkspace : LoggerIO Lake.Workspace` for use in `IO` which constructs the IO
-  environment variables and finds the lean installation.
+Workspace loading is intended for executables. Library consumers needing only module traversal
+and the associated instances should import `ImportGraph.Util.Modules` instead.
 
-Note that this file should generally not be transitively imported, and is not imported via
-`import ImportGraph`. However, it is a dependency of the `import-graph-workspace-summary` exe,
-which is a default target. As such, it will always get built under `lake build`.
+This file must not be imported by modules reachable from `ImportGraph` or `ImportGraph.Tools`;
+see `ImportGraphTest.NoLakeAxioms`. The workspace-summary executable imports it separately.
 -/
 
 open Lean Lake
 
-public section
-
-namespace ImportGraph
-
-namespace System.FilePath
-
-/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
-`for (mod, dirEntry) in mods do`. Usually invoked via `for (mod, dirEntry) in dir.modules do`; see
-`ImportGraph.System.FilePath.modules` for details. -/
-structure Modules where
-  dir : System.FilePath
-  root : Name := .anonymous
-
-/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
-`for (mod, dirEntry) in dir.modules do`, descending into subdirectories (top-down, left-to-right),
-and constructing the module name according to the directory names and `*.lean` filenames.
-
-For example, if `dir` contains `A/B/C.lean`, this iteration visits `(A.B.C, ⟨"A/B", "C.lean"⟩)`.
-
-If `root` is provided, then `root` is prepended to the module names created from paths in the
-directory, e.g. if `dir` contains `A/B/C.lean` and we iterate through
-``for (mod, dirEntry) in dir.modules (root := `Foo)``, this iteration visits
-`(Foo.A.B.C, ⟨"A/B", "C.lean"⟩)`.
-
-By default, no root is inferred. -/
-@[inline] def modules (dir : System.FilePath) (root := Name.anonymous) : Modules := { dir, root }
-
-@[specialize]
-partial def Modules.forInAux [Monad m] [MonadLiftT IO m] {β}
-    (dir : System.FilePath) (pre : Name) (b : β)
-    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m (ForInStep β) := do
-  let mut b := b
-  for entry in ← dir.readDir do
-    if (← liftM (m := IO) <| entry.path.isDir) then
-      match (← Modules.forInAux entry.path (.str pre entry.fileName) b f) with
-      | ForInStep.yield b' => b := b'
-      | ForInStep.done b'  => return ForInStep.done b'
-    else if entry.path.extension.isEqSome "lean" then
-      let mod := .str pre <| (System.FilePath.withExtension entry.fileName "").toString
-      match (← f (mod, entry) b) with
-      | ForInStep.yield b' => b := b'
-      | ForInStep.done b'  => return ForInStep.done b'
-  return ForInStep.yield b
-
-instance [Monad m] [MonadLiftT IO m] : ForIn m Modules (Name × IO.FS.DirEntry) where
-  forIn spec init f := ForInStep.value <$> Modules.forInAux spec.dir spec.root init f
-
-/--
-Splits `path` into the `DirEntry` for its enclosing directory and file name, as `readDir` would
-report it. `path.parent` (rather than `path.withFileName ""`) is used for `root` so that it carries
-no trailing separator and so that `root / fileName` round-trips back to `path` (matching the entries
-produced when iterating through a directory).
--/
-def toDirEntry (path : System.FilePath) : IO.FS.DirEntry where
-  root := path.parent.getD ""
-  fileName := path.fileName.getD ""
-
-end System.FilePath
-
-open ImportGraph
-
-namespace Lake
-
-/-! ## Missing instances -/
-
-deriving instance Hashable for SemVerCore
-deriving instance Hashable for StdVer
-deriving instance Hashable for LeanVer
-deriving instance Hashable for Date
-deriving instance Hashable for ToolchainVer
-
-deriving instance ToJson, FromJson for Lake.Glob
-
-/-! ## `for ... in` instances -/
-
-/-- Allows iteration over the matched modules via `for (mod, dirEntry) in globMods do`. This is
-typically constructed via `glob.modulesIn dir`. -/
-structure Glob.Modules where
-  glob : Glob
-  dir : System.FilePath
-
-/-- Allows iteration over the modules matched by a `Lake.Glob` in `dir` via
-`for (mod, dirEntry) in glob.modulesIn dir do`. -/
-@[inline] def Glob.modulesIn (dir : System.FilePath) (glob : Glob) : Glob.Modules :=
-  { glob, dir }
-
-/--
-Iterates over the module names selected by `glob`, resolving submodule globs against the `.lean`
-files found under `dir`.
-
-Auxiliary to the `ForIn` instance for `Glob.Modules`.
--/
-@[specialize]
-def Glob.Modules.forIn [Monad m] [MonadLiftT IO m] {β}
-    (spec : Glob.Modules) (init : β)
-    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m β := do
-  match spec.glob with
-  | .one n =>
-    -- Like Lake's `Glob.forEachModuleIn`, which yields `n` unconditionally: we must not require
-    -- `n`'s source file to exist, so build its `DirEntry` without touching the filesystem.
-    let modFile := modToFilePath spec.dir n "lean"
-    return (← f (n, modFile.toDirEntry) init).value
-  | .submodules n =>
-    let modDir := modToFilePath spec.dir n ""
-    -- `ForIn.forIn`, not the `forIn` being defined here (which the local name would shadow).
-    ForIn.forIn (modDir.modules (root := n)) init f
-  | .andSubmodules n =>
-    let modFile := modToFilePath spec.dir n "lean"
-    match ← f (n, modFile.toDirEntry) init with
-    | ForInStep.done b => return b
-    | ForInStep.yield b =>
-      let modDir := modToFilePath spec.dir n ""
-      ForIn.forIn (modDir.modules (root := n)) b f
-
-instance [Monad m] [MonadLiftT IO m] : ForIn m Glob.Modules (Name × IO.FS.DirEntry) where
-  forIn := Glob.Modules.forIn
-
-namespace IO
+namespace ImportGraph.Lake.IO
 
 /-- Loads the lake workspace from the current directory (or, if specified, from `wsDir?`) in `IO`.
 

ImportGraph/Util/Modules.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+public import Lake.Config.Glob
+public import Lake.Util.Version
+
+/-!
+# Module traversal utilities
+
+Provides directory and glob iteration, plus the JSON and hashing instances used by workspace
+summaries, without importing Lake workspace configuration or loading.
+-/
+
+open Lean Lake
+
+public section
+
+namespace ImportGraph
+
+namespace System.FilePath
+
+/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
+`for (mod, dirEntry) in mods do`. Usually invoked via `for (mod, dirEntry) in dir.modules do`; see
+`ImportGraph.System.FilePath.modules` for details. -/
+structure Modules where
+  dir : System.FilePath
+  root : Name := .anonymous
+
+/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
+`for (mod, dirEntry) in dir.modules do`, descending into subdirectories (top-down, left-to-right),
+and constructing the module name according to the directory names and `*.lean` filenames.
+
+For example, if `dir` contains `A/B/C.lean`, this iteration visits `(A.B.C, ⟨"A/B", "C.lean"⟩)`.
+
+If `root` is provided, then `root` is prepended to the module names created from paths in the
+directory, e.g. if `dir` contains `A/B/C.lean` and we iterate through
+``for (mod, dirEntry) in dir.modules (root := `Foo)``, this iteration visits
+`(Foo.A.B.C, ⟨"A/B", "C.lean"⟩)`.
+
+By default, no root is inferred. -/
+@[inline] def modules (dir : System.FilePath) (root := Name.anonymous) : Modules := { dir, root }
+
+@[specialize]
+partial def Modules.forInAux [Monad m] [MonadLiftT IO m] {β}
+    (dir : System.FilePath) (pre : Name) (b : β)
+    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m (ForInStep β) := do
+  let mut b := b
+  for entry in ← dir.readDir do
+    if (← liftM (m := IO) <| entry.path.isDir) then
+      match (← Modules.forInAux entry.path (.str pre entry.fileName) b f) with
+      | ForInStep.yield b' => b := b'
+      | ForInStep.done b'  => return ForInStep.done b'
+    else if entry.path.extension.isEqSome "lean" then
+      let mod := .str pre <| (System.FilePath.withExtension entry.fileName "").toString
+      match (← f (mod, entry) b) with
+      | ForInStep.yield b' => b := b'
+      | ForInStep.done b'  => return ForInStep.done b'
+  return ForInStep.yield b
+
+instance [Monad m] [MonadLiftT IO m] : ForIn m Modules (Name × IO.FS.DirEntry) where
+  forIn spec init f := ForInStep.value <$> Modules.forInAux spec.dir spec.root init f
+
+/--
+Splits `path` into the `DirEntry` for its enclosing directory and file name, as `readDir` would
+report it. `path.parent` (rather than `path.withFileName ""`) is used for `root` so that it carries
+no trailing separator and so that `root / fileName` round-trips back to `path` (matching the entries
+produced when iterating through a directory).
+-/
+def toDirEntry (path : System.FilePath) : IO.FS.DirEntry where
+  root := path.parent.getD ""
+  fileName := path.fileName.getD ""
+
+end System.FilePath
+
+open ImportGraph
+
+namespace Lake
+
+/-! ## Missing instances -/
+
+deriving instance Hashable for SemVerCore
+deriving instance Hashable for StdVer
+deriving instance Hashable for LeanVer
+deriving instance Hashable for Date
+deriving instance Hashable for ToolchainVer
+
+deriving instance ToJson, FromJson for Lake.Glob
+
+/-! ## `for ... in` instances -/
+
+/-- Allows iteration over the matched modules via `for (mod, dirEntry) in globMods do`. This is
+typically constructed via `glob.modulesIn dir`. -/
+structure Glob.Modules where
+  glob : Glob
+  dir : System.FilePath
+
+/-- Allows iteration over the modules matched by a `Lake.Glob` in `dir` via
+`for (mod, dirEntry) in glob.modulesIn dir do`. -/
+@[inline] def Glob.modulesIn (dir : System.FilePath) (glob : Glob) : Glob.Modules :=
+  { glob, dir }
+
+/--
+Iterates over the module names selected by `glob`, resolving submodule globs against the `.lean`
+files found under `dir`.
+
+Auxiliary to the `ForIn` instance for `Glob.Modules`.
+-/
+@[specialize]
+def Glob.Modules.forIn [Monad m] [MonadLiftT IO m] {β}
+    (spec : Glob.Modules) (init : β)
+    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m β := do
+  match spec.glob with
+  | .one n =>
+    -- Like Lake's `Glob.forEachModuleIn`, which yields `n` unconditionally: we must not require
+    -- `n`'s source file to exist, so build its `DirEntry` without touching the filesystem.
+    let modFile := modToFilePath spec.dir n "lean"
+    return (← f (n, modFile.toDirEntry) init).value
+  | .submodules n =>
+    let modDir := modToFilePath spec.dir n ""
+    -- `ForIn.forIn`, not the `forIn` being defined here (which the local name would shadow).
+    ForIn.forIn (modDir.modules (root := n)) init f
+  | .andSubmodules n =>
+    let modFile := modToFilePath spec.dir n "lean"
+    match ← f (n, modFile.toDirEntry) init with
+    | ForInStep.done b => return b
+    | ForInStep.yield b =>
+      let modDir := modToFilePath spec.dir n ""
+      ForIn.forIn (modDir.modules (root := n)) b f
+
+instance [Monad m] [MonadLiftT IO m] : ForIn m Glob.Modules (Name × IO.FS.DirEntry) where
+  forIn := Glob.Modules.forIn
+
+end ImportGraph.Lake

ImportGraph/WorkspaceModel/Base.lean

@@ -8,7 +8,7 @@ module
 public import Lake.Config.Glob
 public import Lake.Util.Version
 
-import ImportGraph.Lake
+import ImportGraph.Util.Modules
 
 /-!
 # Basic Lake workspace data

ImportGraph/WorkspaceModel/Build.lean

@@ -10,7 +10,7 @@ public import ImportGraph.WorkspaceModel.Summary
 public import ImportGraph.Shake.Algebra
 
 import Lean.Elab.ParseImportsFast
-import ImportGraph.Lake
+import ImportGraph.Util.Modules
 
 /-!
 # Building a `WorkspaceModel`

ImportGraph/WorkspaceModel/Summary.lean

@@ -9,14 +9,15 @@ public import ImportGraph.WorkspaceModel.Summary.Core
 public import ImportGraph.WorkspaceModel.Summary.Get
 
 /-!
-Importing this file downstream is "safe", and only transitively introduces the following small Lake
-dependencies:
+Importing this file downstream is "safe", and introduces the following small Lake dependencies
+for its public field types:
 ```
 public import Lake.Config.Glob
 public import Lake.Util.Version
 ```
-Both of these files do not transitively import any further Lake dependencies. They are necessary
-for the types `Glob` and `ToolchainVer` in `WorkspaceSummary` field types.
+These provide `Glob` and `ToolchainVer` in `WorkspaceSummary` field types. Cache validation also
+uses `Lake.Build.Trace` for hashing. None of these imports brings in Lake workspace loading or
+the build type-family axioms.
 
 For Lake interaction with `WorkspaceSummary`, import `ImportGraph.WorkspaceModel.Summary.Lake`.
 -/