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.

structure Lake.Dynlib :

A dynamic/shared library for linking.

  • Library file path.

  • name : String

    Library name without platform-specific prefix/suffix (for -l).

Instances For

    Optional library directory (for -L).

    Equations
    Instances For

      Module Facets #

      structure Lake.ModuleFacet (α : Type) :

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

      • name : Lake.Name

        The name of the module facet.

      • data_eq : Lake.ModuleData self.name = α

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

      Instances For
        instance Lake.instReprModuleFacet :
        {α : Type} → [inst : Repr α] → Repr (Lake.ModuleFacet α)
        Equations
        • Lake.instReprModuleFacet = { reprPrec := Lake.reprModuleFacet✝ }
        Equations
        • =
        Equations
        • Lake.instCoeDepNameModuleFacet = { coe := { name := facet, data_eq := } }
        @[inline, 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
          @[inline, 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
            @[inline, reducible]

            The olean file produced by lean.

            Equations
            Instances For
              @[inline, reducible]

              The ilean file produced by lean.

              Equations
              Instances For
                @[inline, reducible]

                The C file built from the Lean file via lean.

                Equations
                Instances For
                  @[inline, reducible]

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

                  Equations
                  Instances For
                    @[inline, reducible]

                    The object file .c.o built from c.

                    Equations
                    Instances For
                      @[inline, reducible]

                      The object file .bc.o built from bc.

                      Equations
                      Instances For
                        @[inline, reducible]

                        The object file built from c/bc.

                        Equations
                        Instances For

                          Package Facets #

                          @[inline, reducible]

                          A package's cloud build release.

                          Equations
                          Instances For
                            @[inline, reducible]

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

                            Equations
                            Instances For

                              Target Facets #

                              @[inline, reducible]

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

                              Equations
                              Instances For
                                @[inline, reducible]

                                A Lean library's static artifact.

                                Equations
                                Instances For
                                  @[inline, reducible]

                                  A Lean library's shared artifact.

                                  Equations
                                  Instances For
                                    @[inline, reducible]

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

                                    Equations
                                    Instances For
                                      @[inline, reducible]

                                      A Lean binary executable.

                                      Equations
                                      Instances For
                                        @[inline, reducible]

                                        A external library's static binary.

                                        Equations
                                        Instances For
                                          @[inline, reducible]

                                          A external library's shared binary.

                                          Equations
                                          Instances For
                                            @[inline, reducible]

                                            A external library's dynlib.

                                            Equations
                                            Instances For