structure Lake.ModuleOutputHashes : Type

The content hashes of the output artifacts of a module build.

• olean : Hash
• oleanServer? : Option Hash
• oleanPrivate? : Option Hash
• ilean : Hash
• c : Hash
• bc? : Option Hash

def Lake.ModuleOutputHashes.oleanHashes (hashes : ModuleOutputHashes) : Array Hash

Equations

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

def Lake.ModuleOutputHashes.toJson (hashes : ModuleOutputHashes) : Lean.Json

Equations

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

instance Lake.instToJsonModuleOutputHashes : Lean.ToJson ModuleOutputHashes

Equations

• Lake.instToJsonModuleOutputHashes = { toJson := Lake.ModuleOutputHashes.toJson }

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

Equations

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

instance Lake.instFromJsonModuleOutputHashes : Lean.FromJson ModuleOutputHashes

Equations

• Lake.instFromJsonModuleOutputHashes = { fromJson? := Lake.ModuleOutputHashes.fromJson? }

structure Lake.ModuleOutputArtifacts : Type

The output artifacts of a module build.

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

def Lake.ModuleOutputArtifacts.hashes (arts : ModuleOutputArtifacts) : ModuleOutputHashes

Content hashes of the artifacts.

Equations

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