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

                    Build Info to Key #

                    @[inline, reducible]

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

                    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.

                      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.

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

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

                          Instances For
                            @[inline]

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

                            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.

                              Instances For
                                @[inline, reducible]

                                The transitive local imports of the Lean module.

                                Instances For
                                  @[inline, reducible]

                                  The transitive local imports of the Lean module.

                                  Instances For
                                    @[inline, reducible]

                                    Shared library for --load-dynlib.

                                    Instances For
                                      @[inline, reducible]

                                      A Lean library's Lean modules.

                                      Instances For
                                        @[inline, reducible]

                                        The package's complete array of transitive dependencies.

                                        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.

                                          Instances For
                                            @[inline, reducible]

                                            The direct local imports of the Lean module.

                                            Instances For
                                              @[inline, reducible]

                                              The transitive local imports of the Lean module.

                                              Instances For
                                                @[inline, reducible]

                                                The transitive local imports of the Lean module.

                                                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.

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

                                                              Shared library for --load-dynlib.

                                                              Instances For
                                                                @[inline, reducible]

                                                                Build info for the package's specified facet.

                                                                Instances For
                                                                  @[inline, reducible]

                                                                  A package's cloud build release.

                                                                  Instances For
                                                                    @[inline, reducible]

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

                                                                    Instances For
                                                                      @[inline, reducible]

                                                                      Build info for a custom package target.

                                                                      Instances For
                                                                        @[inline, reducible]

                                                                        Build info of the Lean library's Lean binaries.

                                                                        Instances For
                                                                          @[inline, reducible]

                                                                          A Lean library's Lean modules.

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

                                                                                    Build info of the Lean executable.

                                                                                    Instances For
                                                                                      @[inline, reducible]

                                                                                      Build info of the external library's static binary.

                                                                                      Instances For
                                                                                        @[inline, reducible]

                                                                                        Build info of the external library's shared binary.

                                                                                        Instances For
                                                                                          @[inline, reducible]

                                                                                          Build info of the external library's dynlib.

                                                                                          Instances For