Documentation

Lake.Build.Info

Build Info #

This module defines the Lake build info type and related utilities. Build info is what is the data passed to a Lake build function to facilitate the build.

inductive Lake.BuildInfo :

The type of Lake's build info.

Instances For

    Build Info & Keys #

    Build Key Helper Constructors #

    @[reducible, inline]
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              @[reducible, inline]
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For

                    Build Info to Key #

                    @[reducible]

                    The key that identifies the build in the Lake build store.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Instances for deducing data types of BuildInfo keys #

                      Build Info & Facets #

                      Complex Builtin Facet Declarations #

                      Additional builtin facets missing from Build.Facets. These are defined here because they need configuration definitions (e.g., Module), whereas the facets there are needed by the configuration definitions.

                      @[reducible, inline]

                      The direct local imports of the Lean module.

                      Equations
                      Instances For
                        @[reducible, inline]

                        The transitive local imports of the Lean module.

                        Equations
                        Instances For
                          @[reducible, inline]

                          The transitive local imports of the Lean module.

                          Equations
                          Instances For
                            @[reducible, inline]

                            Shared library for --load-dynlib.

                            Equations
                            Instances For
                              @[reducible, inline]

                              A Lean library's Lean modules.

                              Equations
                              Instances For
                                @[reducible, inline]

                                The package's complete array of transitive dependencies.

                                Equations
                                Instances For

                                  Facet Build Info Helper Constructors #

                                  Definitions to easily construct BuildInfo values for module, package, and target facets.

                                  @[reducible, inline]

                                  Build info for the module's specified facet.

                                  Equations
                                  Instances For
                                    @[reducible, inline]

                                    The direct local imports of the Lean module.

                                    Equations
                                    Instances For
                                      @[reducible, inline]

                                      The transitive local imports of the Lean module.

                                      Equations
                                      Instances For
                                        @[reducible, inline]

                                        The transitive local imports of the Lean module.

                                        Equations
                                        Instances For
                                          @[reducible, inline]

                                          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
                                            @[reducible, inline]

                                            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, inline]

                                              The olean file produced by lean.

                                              Equations
                                              Instances For
                                                @[reducible, inline]

                                                The ilean file produced by lean.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]

                                                  The C file built from the Lean file via lean.

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]

                                                    The C file built from the Lean file via lean.

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]

                                                      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, inline]

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

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]

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

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]

                                                            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, inline]

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

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]

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

                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]

                                                                  The object file .bc.o built from bc.

                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]

                                                                    Shared library for --load-dynlib.

                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]

                                                                      Build info for the package's specified facet.

                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]

                                                                        A package's cloud build release. Will cause the whole build to fail if the release cannot be fetched.

                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]

                                                                          A package's optional cloud build release. Will not cause the whole build to fail if the release cannot be fetched.

                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline]

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

                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline]

                                                                              Build info for a custom package target.

                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline]

                                                                                Build info of the Lean library's Lean binaries.

                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline]

                                                                                  A Lean library's Lean modules.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]

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

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline]

                                                                                      A Lean library's static artifact.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline]

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

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline]

                                                                                          A Lean library's shared artifact.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline]

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

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline]

                                                                                              Build info of the Lean executable.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[reducible, inline]

                                                                                                Build info of the external library's static binary.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible, inline]

                                                                                                  Build info of the external library's shared binary.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[reducible, inline]

                                                                                                    Build info of the external library's dynlib.

                                                                                                    Equations
                                                                                                    Instances For