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.

structure ImportGraph.System.FilePath.Modules : Type

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.

• dir : System.FilePath
• root : Lean.Name

@[inline]

def ImportGraph.System.FilePath.modules (dir : System.FilePath) (root : Lean.Name := Lean.Name.anonymous) : Modules

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.

Equations

• ImportGraph.System.FilePath.modules dir root = { dir := dir, root := root }

@[specialize #[]]

partial def ImportGraph.System.FilePath.Modules.forInAux {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] {β : Type} (dir : System.FilePath) (pre : Lean.Name) (b : β) (f : Lean.Name × IO.FS.DirEntry → β → m (ForInStep β)) : m (ForInStep β)

@[instance_reducible]

instance ImportGraph.System.FilePath.instForInModulesProdNameDirEntryOfMonadOfMonadLiftTIO {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] : ForIn m Modules (Lean.Name × IO.FS.DirEntry)

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.System.FilePath.toDirEntry (path : System.FilePath) : IO.FS.DirEntry

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).

Equations

• ImportGraph.System.FilePath.toDirEntry path = { root := path.parent.getD { toString := "" }, fileName := path.fileName.getD "" }

Missing instances

def ImportGraph.Lake.instHashableSemVerCore_importGraph.hash : Lake.SemVerCore → UInt64

Equations

• ImportGraph.Lake.instHashableSemVerCore_importGraph.hash { major := a, minor := a_1, patch := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

@[instance_reducible]

instance ImportGraph.Lake.instHashableSemVerCore_importGraph : Hashable Lake.SemVerCore

Equations

• ImportGraph.Lake.instHashableSemVerCore_importGraph = { hash := ImportGraph.Lake.instHashableSemVerCore_importGraph.hash }

@[instance_reducible]

instance ImportGraph.Lake.instHashableStdVer_importGraph : Hashable Lake.StdVer

Equations

• ImportGraph.Lake.instHashableStdVer_importGraph = { hash := ImportGraph.Lake.instHashableStdVer_importGraph.hash }

def ImportGraph.Lake.instHashableStdVer_importGraph.hash : Lake.StdVer → UInt64

Equations

• ImportGraph.Lake.instHashableStdVer_importGraph.hash { toSemVerCore := a, specialDescr := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance ImportGraph.Lake.instHashableLeanVer_importGraph : Hashable Lake.LeanVer

Equations

• ImportGraph.Lake.instHashableLeanVer_importGraph = { hash := ImportGraph.Lake.instHashableStdVer_importGraph.hash }

def ImportGraph.Lake.instHashableDate_importGraph.hash : Lake.Date → UInt64

Equations

• ImportGraph.Lake.instHashableDate_importGraph.hash { year := a, month := a_1, day := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

@[instance_reducible]

instance ImportGraph.Lake.instHashableDate_importGraph : Hashable Lake.Date

Equations

• ImportGraph.Lake.instHashableDate_importGraph = { hash := ImportGraph.Lake.instHashableDate_importGraph.hash }

def ImportGraph.Lake.instHashableToolchainVer_importGraph.hash : Lake.ToolchainVer → UInt64

Equations

• ImportGraph.Lake.instHashableToolchainVer_importGraph.hash (Lake.ToolchainVer.release a) = mixHash 0 (hash a)
• ImportGraph.Lake.instHashableToolchainVer_importGraph.hash (Lake.ToolchainVer.nightly a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)
• ImportGraph.Lake.instHashableToolchainVer_importGraph.hash (Lake.ToolchainVer.pr a) = mixHash 2 (hash a)
• ImportGraph.Lake.instHashableToolchainVer_importGraph.hash (Lake.ToolchainVer.other a) = mixHash 3 (hash a)

@[instance_reducible]

instance ImportGraph.Lake.instHashableToolchainVer_importGraph : Hashable Lake.ToolchainVer

Equations

• ImportGraph.Lake.instHashableToolchainVer_importGraph = { hash := ImportGraph.Lake.instHashableToolchainVer_importGraph.hash }

def ImportGraph.Lake.instToJsonGlob_importGraph.toJson : Lake.Glob → Lean.Json

Equations

• ImportGraph.Lake.instToJsonGlob_importGraph.toJson (Lake.Glob.one a) = Lean.Json.mkObj [("one", Lean.toJson a)]
• ImportGraph.Lake.instToJsonGlob_importGraph.toJson (Lake.Glob.submodules a) = Lean.Json.mkObj [("submodules", Lean.toJson a)]
• ImportGraph.Lake.instToJsonGlob_importGraph.toJson (Lake.Glob.andSubmodules a) = Lean.Json.mkObj [("andSubmodules", Lean.toJson a)]

@[instance_reducible]

instance ImportGraph.Lake.instToJsonGlob_importGraph : Lean.ToJson Lake.Glob

Equations

• ImportGraph.Lake.instToJsonGlob_importGraph = { toJson := ImportGraph.Lake.instToJsonGlob_importGraph.toJson }

def ImportGraph.Lake.instFromJsonGlob_importGraph.fromJson : Lean.Json → Except String Lake.Glob

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonGlob_importGraph : Lean.FromJson Lake.Glob

Equations

• ImportGraph.Lake.instFromJsonGlob_importGraph = { fromJson? := ImportGraph.Lake.instFromJsonGlob_importGraph.fromJson }

for ... in instances

structure ImportGraph.Lake.Glob.Modules : Type

Allows iteration over the matched modules via for (mod, dirEntry) in globMods do. This is typically constructed via glob.modulesIn dir.

• glob : Lake.Glob
• dir : System.FilePath

@[inline]

def ImportGraph.Lake.Glob.modulesIn (dir : System.FilePath) (glob : Lake.Glob) : Modules

Allows iteration over the modules matched by a Lake.Glob in dir via for (mod, dirEntry) in glob.modulesIn dir do.

Equations

• ImportGraph.Lake.Glob.modulesIn dir glob = { glob := glob, dir := dir }

@[specialize #[]]

def ImportGraph.Lake.Glob.Modules.forIn {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] {β : Type} (spec : Modules) (init : β) (f : Lean.Name × IO.FS.DirEntry → β → m (ForInStep β)) : m β

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.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lake.instForInModulesProdNameDirEntryOfMonadOfMonadLiftTIO {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] : ForIn m Glob.Modules (Lean.Name × IO.FS.DirEntry)

Equations

• ImportGraph.Lake.instForInModulesProdNameDirEntryOfMonadOfMonadLiftTIO = { forIn := fun {β : Type} => ImportGraph.Lake.Glob.Modules.forIn }