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

@[instance_reducible]

instance ImportGraph.Lake.instHashableSemVerCore_importGraph : Hashable Lake.SemVerCore

Equations

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

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

@[instance_reducible]

instance ImportGraph.Lake.instHashableDate_importGraph : Hashable Lake.Date

Equations

• ImportGraph.Lake.instHashableDate_importGraph = { hash := ImportGraph.Lake.instHashableDate_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)

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 }

@[instance_reducible]

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

Equations

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

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.

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 }

def ImportGraph.Lake.IO.getWorkspace (wsDir? : Option System.FilePath := none) : IO Lake.Workspace

Loads the lake workspace from the current directory (or, if specified, from wsDir?) in IO.

Note that in the language server, the current working directory is the workspace root, so this may use the current working directory of elaboration. However, it may not itself be called directly during elaboration, as this causes the language server to crash. Therefore, for use "in" the language server, it must be called across a process boundary via an exe.

Equations

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