Documentation

Lake.Build.ModuleArtifacts

source
structure Lake.ModuleOutputDescrs :
Type

The descriptions of the output artifacts of a module build.

Instances For
    source
    def Lake.ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) :
    Array ArtifactDescr
    Instances For
      source
      def Lake.ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) :
      Lean.Json
      Instances For
        source
        @[implicit_reducible]
        instance Lake.instToJsonModuleOutputDescrs :
        Lean.ToJson ModuleOutputDescrs
        source
        def Lake.ModuleOutputDescrs.fromJson? (val : Lean.Json) :
        Except String ModuleOutputDescrs
        Instances For
          source
          @[implicit_reducible]
          instance Lake.instFromJsonModuleOutputDescrs :
          Lean.FromJson ModuleOutputDescrs
          source
          structure Lake.ModuleOutputArtifacts :
          Type

          The output artifacts of a module build.

          Instances For
            source
            def Lake.ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) :
            ModuleOutputDescrs

            Content hashes of the artifacts.

            Instances For