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

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

instance Lake.instToJsonModuleOutputDescrs : Lean.ToJson ModuleOutputDescrs

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

instance Lake.instFromJsonModuleOutputDescrs : Lean.FromJson ModuleOutputDescrs

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.