structure Lake.ModuleOutputDescrs : Type

The descriptions of the output artifacts of a module build.

• olean : ArtifactDescr
• oleanServer? : Option ArtifactDescr
• oleanPrivate? : Option ArtifactDescr
• ilean : ArtifactDescr
• ir? : Option ArtifactDescr
• c : ArtifactDescr
• bc? : Option ArtifactDescr

def Lake.ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) : Array ArtifactDescr

Equations

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

def Lake.ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Lean.Json

Equations

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

instance Lake.instToJsonModuleOutputDescrs : Lean.ToJson ModuleOutputDescrs

Equations

• Lake.instToJsonModuleOutputDescrs = { toJson := Lake.ModuleOutputDescrs.toJson }

def Lake.ModuleOutputDescrs.fromJson? (val : Lean.Json) : Except String ModuleOutputDescrs

Equations

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

instance Lake.instFromJsonModuleOutputDescrs : Lean.FromJson ModuleOutputDescrs

Equations

• Lake.instFromJsonModuleOutputDescrs = { fromJson? := Lake.ModuleOutputDescrs.fromJson? }

structure Lake.ModuleOutputArtifacts : Type

The output artifacts of a module build.

• olean : Artifact
• oleanServer? : Option Artifact
• oleanPrivate? : Option Artifact
• ilean : Artifact
• ir? : Option Artifact
• c : Artifact
• bc? : Option Artifact

def Lake.ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleOutputDescrs

Content hashes of the artifacts.

Equations

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