source
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

Instances For

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

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

Instances For

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

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

Instances For

source
instance Lake.instToJsonModuleOutputDescrs :
Lean.ToJson ModuleOutputDescrs
Equations

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

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

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

Instances For

source
instance Lake.instFromJsonModuleOutputDescrs :
Lean.FromJson ModuleOutputDescrs
Equations

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

source
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

Instances For

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

Instances For