Documentation

Lake.Config.FacetConfig

structure Lake.FacetConfig (DataFam : Lake.NameType) (ι : Type) (name : Lake.Name) :

A facet's declarative configuration.

Instances For
    instance Lake.instInhabitedFacetConfig :
    {a : Lake.NameType} → {a_1 : Type} → {a_2 : Lake.Name} → Inhabited (Lake.FacetConfig a a_1 a_2)
    Equations
    • Lake.instInhabitedFacetConfig = { default := { build := default, getJob? := default } }
    @[inline, reducible]
    abbrev Lake.FacetConfig.name {DataFam : Lake.NameType} {ι : Type} {name : Lake.Name} :
    Lake.FacetConfig DataFam ι nameLake.Name
    Equations
    Instances For
      @[inline]
      def Lake.mkFacetConfig {ι : Type} {α : Type} {Fam : Lake.NameType} {facet : Lake.Name} (build : ιLake.IndexBuildM α) [h : Lake.FamilyOut Fam facet α] :
      Lake.FacetConfig Fam ι facet

      A smart constructor for facet configurations that are not known to generate targets.

      Equations
      Instances For
        @[inline]
        def Lake.mkFacetJobConfigSmall {ι : Type} {α : Type} {Fam : Lake.NameType} {facet : Lake.Name} (build : ιLake.IndexBuildM (Lake.BuildJob α)) [h : Lake.FamilyOut Fam facet (Lake.BuildJob α)] :
        Lake.FacetConfig Fam ι facet

        A smart constructor for facet configurations that generate jobs for the CLI. This is for small jobs that do not the increase the progress counter.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]
          def Lake.mkFacetJobConfig {ι : Type} {α : Type} {Fam : Lake.NameType} {facet : Lake.Name} (build : ιLake.IndexBuildM (Lake.BuildJob α)) [Lake.FamilyOut Fam facet (Lake.BuildJob α)] :
          Lake.FacetConfig Fam ι 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 (β : Lake.NameType u) :

            A dependently typed configuration based on its registered name.

            Instances For
              @[inline, reducible]

              A module facet's declarative configuration.

              Equations
              Instances For
                @[inline, reducible]

                A module facet declaration from a configuration file.

                Equations
                Instances For
                  @[inline, reducible]

                  A package facet's declarative configuration.

                  Equations
                  Instances For
                    @[inline, reducible]

                    A package facet declaration from a configuration file.

                    Equations
                    Instances For
                      @[inline, reducible]

                      A library facet's declarative configuration.

                      Equations
                      Instances For
                        @[inline, reducible]

                        A library facet declaration from a configuration file.

                        Equations
                        Instances For