Documentation

Lake.Build.Facets

Simple Builtin Facet Declarations #

This module contains the definitions of most of the builtin facets. The others are defined Build.Info. The facets there require configuration definitions (e.g., Module), and some of the facets here are used in said definitions.

Instances For

    Module Facets #

    structure Lake.ModuleFacet (α : Type) :

    A module facet name along with proof of its data type.

    • name : Lean.Name

      The name of the module facet.

    • data_eq : FacetOut self.name = α

      Proof that module's facet build result is of type α.

    Instances For
      instance Lake.instReprModuleFacet {α✝ : Type} [Repr α✝] :
      Equations
        @[reducible]

        The facet which builds all of a module's dependencies (i.e., transitive local imports and --load-dynlib shared libraries). Returns the list of shared libraries to load along with their search path.

        Equations
          Instances For
            @[simp]
            @[reducible]

            The core build facet of a Lean file. Elaborates the Lean file via lean and produces all the Lean artifacts of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

            Equations
              Instances For
                @[reducible]

                The olean file produced by lean.

                Equations
                  Instances For
                    @[reducible]

                    The ilean file produced by lean.

                    Equations
                      Instances For
                        @[reducible]

                        The C file built from the Lean file via lean.

                        Equations
                          Instances For
                            @[reducible]

                            The LLVM BC file built from the Lean file via lean.

                            Equations
                              Instances For
                                @[reducible]

                                The object file .c.o built from c. On Windows, this is c.o.noexport, on other systems it is c.o.export).

                                Equations
                                  Instances For
                                    @[reducible]

                                    The object file .c.o.export built from c (with -DLEAN_EXPORTING).

                                    Equations
                                      Instances For
                                        @[reducible]

                                        The object file .c.o.noexport built from c (without -DLEAN_EXPORTING).

                                        Equations
                                          Instances For
                                            @[reducible]

                                            The object file .bc.o built from bc.

                                            Equations
                                              Instances For
                                                @[reducible]

                                                The object file built from c/bc. On Windows with the C backend, no Lean symbols are exported. On every other configuration, symbols are exported.

                                                Equations
                                                  Instances For
                                                    @[reducible]

                                                    The object file built from c/bc (with Lean symbols exported).

                                                    Equations
                                                      Instances For
                                                        @[reducible]

                                                        The object file built from c/bc (without Lean symbols exported).

                                                        Equations
                                                          Instances For

                                                            Package Facets #

                                                            @[simp]
                                                            @[reducible]

                                                            A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.

                                                            Equations
                                                              Instances For
                                                                @[simp]
                                                                @[reducible]

                                                                A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.

                                                                Equations
                                                                  Instances For
                                                                    @[reducible]

                                                                    A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

                                                                    Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        @[reducible]

                                                                        A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

                                                                        Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            @[simp]
                                                                            axiom Lake.FacetOut.package.optRelease :
                                                                            FacetOut `package.optRelease = Bool
                                                                            @[reducible]

                                                                            A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.

                                                                            Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                @[reducible]

                                                                                A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

                                                                                Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    @[reducible]

                                                                                    A package's extraDepTargets mixed with its transitive dependencies'.

                                                                                    Equations
                                                                                      Instances For

                                                                                        Target Facets #

                                                                                        @[simp]
                                                                                        @[reducible]

                                                                                        The library's default facets (as specified by its defaultFacets configuration). .

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[reducible]

                                                                                            A Lean library's Lean artifacts (i.e., olean, ilean, c).

                                                                                            Equations
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                @[reducible]

                                                                                                A Lean library's static artifact.

                                                                                                Equations
                                                                                                  Instances For
                                                                                                    @[reducible]

                                                                                                    A Lean library's static artifact (with exported symbols).

                                                                                                    Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.

                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        @[reducible]

                                                                                                        A Lean library's shared artifact.

                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            @[reducible]

                                                                                                            A Lean library's extraDepTargets mixed with its package's.

                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                @[reducible]

                                                                                                                The executable's default facet (i.e., an alias for exe)

                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    @[reducible]

                                                                                                                    A Lean binary executable.

                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        @[reducible]

                                                                                                                        The external library's default facet (i.e., an alias for static)

                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            @[reducible]

                                                                                                                            A external library's static binary.

                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                @[reducible]

                                                                                                                                A external library's shared binary.

                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    @[simp]
                                                                                                                                    @[reducible]

                                                                                                                                    A external library's dynlib.

                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible]

                                                                                                                                        The default facet for an input file. Produces the file path.

                                                                                                                                        Equations
                                                                                                                                          Instances For
                                                                                                                                            @[reducible]

                                                                                                                                            The default facet for an input directory. Produces the matching files in the directory.

                                                                                                                                            Equations
                                                                                                                                              Instances For