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 :
  • Library file path.

  • name : String

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

A dynamic/shared library for linking.

Instances For

    Optional library directory (for -L).

    Instances For

      Module Facets #

      structure Lake.ModuleFacet (α : Type) :
      • name : Lake.Name

        The name of the module facet.

      • data_eq : Lake.ModuleData s.name = α

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

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

      Instances For
        instance Lake.instReprModuleFacet :
        {α : Type} → [inst : Repr α] → Repr (Lake.ModuleFacet α)
        @[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.

        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.

          Instances For
            @[inline, reducible]

            The olean file produced by lean.

            Instances For
              @[inline, reducible]

              The ilean file produced by lean.

              Instances For
                @[inline, reducible]

                The C file built from the Lean file via lean.

                Instances For
                  @[inline, reducible]

                  The object file built from c.

                  Instances For

                    Package Facets #

                    @[inline, reducible]

                    A package's cloud build release.

                    Instances For
                      @[inline, reducible]

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

                      Instances For

                        Target Facets #

                        @[inline, reducible]

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

                        Instances For
                          @[inline, reducible]

                          A Lean library's static artifact.

                          Instances For
                            @[inline, reducible]

                            A Lean library's shared artifact.

                            Instances For
                              @[inline, reducible]

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

                              Instances For
                                @[inline, reducible]

                                A Lean binary executable.

                                Instances For
                                  @[inline, reducible]

                                  A external library's static binary.

                                  Instances For
                                    @[inline, reducible]

                                    A external library's shared binary.

                                    Instances For
                                      @[inline, reducible]

                                      A external library's dynlib.

                                      Instances For