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 #

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

            Build Info to Key #

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

              Recursive Building #

              @[inline, reducible]
              abbrev Lake.IndexBuildFn (m : TypeType v) :

              A build function for any element of the Lake build index.

              Equations
              Instances For
                @[inline, reducible]
                abbrev Lake.IndexT (m : TypeType v) (α : Type) :

                A transformer to equip a monad with a build function for the Lake index.

                Equations
                Instances For
                  @[inline, reducible]
                  abbrev Lake.IndexBuildM (α : Type) :

                  The monad for build functions that are part of the index.

                  Equations
                  Instances For
                    @[inline]

                    Fetch the result associated with the info using the Lake build index.

                    Equations
                    Instances For

                      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.

                      @[inline, reducible]

                      The direct local imports of the Lean module.

                      Equations
                      Instances For
                        @[inline, reducible]

                        The transitive local imports of the Lean module.

                        Equations
                        Instances For
                          @[inline, reducible]

                          The transitive local imports of the Lean module.

                          Equations
                          Instances For
                            @[inline, reducible]

                            Shared library for --load-dynlib.

                            Equations
                            Instances For
                              @[inline, reducible]

                              A Lean library's Lean modules.

                              Equations
                              Instances For
                                @[inline, reducible]

                                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.

                                  @[inline, reducible]

                                  Build info for the module's specified facet.

                                  Equations
                                  Instances For
                                    @[inline, reducible]

                                    The direct local imports of the Lean module.

                                    Equations
                                    Instances For
                                      @[inline, reducible]

                                      The transitive local imports of the Lean module.

                                      Equations
                                      Instances For
                                        @[inline, reducible]

                                        The transitive local imports of the Lean module.

                                        Equations
                                        Instances For
                                          @[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 object file built from c.

                                                    Equations
                                                    Instances For
                                                      @[inline, reducible]

                                                      Shared library for --load-dynlib.

                                                      Equations
                                                      Instances For
                                                        @[inline, reducible]

                                                        Build info for the package's specified facet.

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

                                                              Build info for a custom package target.

                                                              Equations
                                                              Instances For
                                                                @[inline, reducible]

                                                                Build info of the Lean library's Lean binaries.

                                                                Equations
                                                                Instances For
                                                                  @[inline, reducible]

                                                                  A Lean library's Lean modules.

                                                                  Equations
                                                                  Instances For
                                                                    @[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]

                                                                            Build info of the Lean executable.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline, reducible]

                                                                              Build info of the external library's static binary.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline, reducible]

                                                                                Build info of the external library's shared binary.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline, reducible]

                                                                                  Build info of the external library's dynlib.

                                                                                  Equations
                                                                                  Instances For