Documentation

Lake.Build.Data

Build Data Subtypes #

opaque Lake.DataType (kind : Lean.Name) :

The open type family which maps a Lake data kind to its associated type. For example, LeanLib.facetKind maps to LeanLib.

It is an open type, meaning additional mappings can be add lazily as needed (via data_type).

class Lake.DataKind (α : Type u) :

A Name descriptor of a data type.

Instances
    class Lake.OptDataKind (α : Type u) :

    Tries to synthesize a Name descriptor of a data type. Otherwise uses Name.anonymous to indicate none was found.

    Instances
      @[instance 100]
      Equations
        @[inline]
        Equations
          Instances For
            theorem Lake.OptDataKind.eq_data_type {α : Type u_1} {self : OptDataKind α} (h : ¬self.isAnonymous = true) :
            α = DataType (name α)
            Equations
              Equations
                @[reducible, inline, deprecated Lake.DataType (since := "2025-03-26")]
                abbrev Lake.TargetData (kind : Lean.Name) :
                Type u_1
                Equations
                  Instances For
                    opaque Lake.FacetOut (facet : Lean.Name) :

                    The open type family which maps a Lake facet to its output type. For example, a FilePath for the module.olean facet.

                    It is an open type, meaning additional mappings can be add lazily as needed (via facet_data).

                    @[reducible, inline]
                    abbrev Lake.FacetData (kind facet : Lean.Name) :

                    The open type family which maps a Lake facet kind and name to its output type. For example, a FilePath for the module olean facet.

                    It is an open type, meaning additional mappings can be add lazily as needed (via facet_data).

                    Equations
                      Instances For
                        instance Lake.instFamilyDefNameFacetDataOfFacetOutHAppend {kind facet : Lean.Name} {α : Type} [h : FamilyDef FacetOut (kind ++ facet) α] :
                        FamilyDef (FacetData kind) facet α
                        instance Lake.instFamilyDefNameFacetOutHAppendOfFacetData {kind facet : Lean.Name} {α : Type} [h : FamilyDef (FacetData kind) facet α] :
                        FamilyDef FacetOut (kind ++ facet) α
                        @[reducible, inline]
                        abbrev Lake.ModuleData (facet : Lean.Name) :

                        The open type family which maps a module facet's name to its output type. For example, a FilePath for the module olean facet.

                        It is an open type, meaning additional mappings can be add lazily as needed (via module_data).

                        Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Lake.PackageData (facet : Lean.Name) :

                            The open type family which maps a package facet's name to output type. For example, an Arrry Package of direct dependencies for the deps facet.

                            It is an open type, meaning additional mappings can be add lazily as needed (via package_data).

                            Equations
                              Instances For
                                @[reducible, inline]
                                abbrev Lake.LibraryData (facet : Lean.Name) :

                                The open type family which maps a Lean library facet's name to its output type. For example, the FilePath pf the generated static library for the static facet.

                                It is an open type, meaning additional mappings can be add lazily as needed (via library_data).

                                Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Lake.LeanLibData (facet : Lean.Name) :

                                    The open type family which maps a Lean library facet's name to its output type. For example, the FilePath pf the generated static library for the static facet.

                                    It is an open type, meaning additional mappings can be add lazily as needed (via library_data).

                                    Equations
                                      Instances For

                                        The open type family which maps a custom package target (package × target name) to its output type.

                                        It is an open type, meaning additional mappings can be add lazily as needed (via custom_data).

                                        @[reducible, inline]
                                        abbrev Lake.CustomData (package target : Lean.Name) :

                                        The open type family which maps a custom package targetto its output type.

                                        It is an open type, meaning additional mappings can be add lazily as needed (via custom_data).

                                        Equations
                                          Instances For

                                            Build Data #

                                            @[reducible, inline]

                                            A mapping between a build key and its associated build data in the store. It is a simple type function composed of the separate open type families for modules facets, package facets, Lake target facets, and custom targets.

                                            Equations
                                              Instances For

                                                Macros for Declaring Build Data #

                                                Macro for declaring new DatayType.

                                                Equations
                                                  Instances For

                                                    Internal macro for declaring new facet within Lake.

                                                    Equations
                                                      Instances For

                                                        Macro for declaring new FacetData.

                                                        Equations
                                                          Instances For

                                                            Macro for declaring new PackageData.

                                                            Equations
                                                              Instances For

                                                                Macro for declaring new ModuleData.

                                                                Equations
                                                                  Instances For

                                                                    Macro for declaring new LibraryData.

                                                                    Equations
                                                                      Instances For

                                                                        Macro for declaring new TargetData.

                                                                        Equations
                                                                          Instances For

                                                                            Macro for declaring new CustomData.

                                                                            Equations
                                                                              Instances For