Documentation

Lake.Config.FacetConfig

structure Lake.FacetConfig (name : Lean.Name) :

A facet's declarative configuration.

  • kind : Lean.Name

    The facet kind (i.e., the kind of targets that support this facet).

  • fetchFn : DataType self.kindFetchM (Job (FacetOut name))

    The facet's fetch function.

  • outKind : OptDataKind (FacetOut name)

    The optional data kind of the facet's output.

  • buildable : Bool

    Is this facet compatible with the lake build CLI?

  • format : OutFormatFacetOut nameString

    Format this facet's output (e.g., for lake query).

  • memoize : Bool

    Whether the fetch of this facet should be cached in the Lake build store.

Instances For
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        structure Lake.KFacetConfig (k name : Lean.Name) extends Lake.FacetConfig name :
        Instances For
          @[reducible, inline]
          abbrev Lake.FacetConfig.toKind {name kind : Lean.Name} (self : FacetConfig name) (h : self.kind = kind) :
          KFacetConfig kind name
          Equations
          • self.toKind h = { toFacetConfig := self, kind_eq := h }
          Instances For
            def Lake.FacetConfig.toKind? {name : Lean.Name} (kind : Lean.Name) (self : FacetConfig name) :
            Option (KFacetConfig kind name)
            Equations
            Instances For
              @[inline]
              def Lake.KFacetConfig.run {kind : Lean.Name} {α : Type} {facet : Lean.Name} {β : Type} [FamilyOut DataType kind α] [FamilyOut FacetOut facet β] (self : KFacetConfig kind facet) (info : α) :
              FetchM (Job β)

              Run the facet configuration's fetch function.

              Equations
              Instances For
                @[inline]
                def Lake.mkFacetJobConfig {β : Type} {kind : Lean.Name} {α : Type} {facet : Lean.Name} [FormatQuery β] [outKind : OptDataKind β] [i : FamilyOut DataType kind α] [o : FamilyOut FacetOut facet β] (build : αFetchM (Job β)) (buildable memoize : Bool := true) :
                KFacetConfig kind facet

                A smart constructor for facet configurations that generate jobs for the CLI.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  structure Lake.NamedConfigDecl (β : Lean.NameType u) :

                  A dependently typed configuration based on its registered name.

                  Instances For
                    @[reducible, inline]

                    A module facet's declarative configuration.

                    Equations
                    Instances For
                      @[reducible, inline]

                      A module facet declaration from a configuration file.

                      Equations
                      Instances For
                        @[reducible, inline]

                        A package facet's declarative configuration.

                        Equations
                        Instances For
                          @[reducible, inline]

                          A package facet declaration from a configuration file.

                          Equations
                          Instances For
                            @[reducible, inline]

                            A library facet's declarative configuration.

                            Equations
                            Instances For
                              @[reducible, inline]

                              A library facet declaration from a configuration file.

                              Equations
                              Instances For
                                @[reducible, inline]

                                A library facet's declarative configuration.

                                Equations
                                Instances For
                                  @[reducible, inline]

                                  A Lean executable facet's declarative configuration.

                                  Equations
                                  Instances For
                                    @[reducible, inline]

                                    An external library facet's declarative configuration.

                                    Equations
                                    Instances For