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, deprecated Lake.Module.key (since := "2025-03-28")]
      Equations
      Instances For
        @[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline, deprecated Lake.Package.key (since := "2025-03-28")]
            Equations
            Instances For
              @[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]
              Equations
              Instances For
                @[reducible, inline]
                abbrev Lake.Package.targetKey (target : Lean.Name) (self : Package) :
                Equations
                Instances For
                  @[reducible, inline, deprecated Lake.Package.targetKey (since := "2025-03-28")]
                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Lake.ConfigTarget.key {kind : Lean.Name} (self : ConfigTarget kind) :
                    Equations
                    Instances For
                      @[reducible, inline, deprecated Lake.ConfigTarget.key (since := "2025-03-28")]
                      Equations
                      Instances For
                        @[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]
                        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
                            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]

                              The direct local imports of the Lean module.

                              Equations
                              Instances For
                                @[reducible]

                                The transitive local imports of the Lean module.

                                Equations
                                Instances For
                                  @[simp]
                                  @[simp]
                                  @[reducible]

                                  The transitive local imports of the Lean module.

                                  Equations
                                  Instances For
                                    @[simp]
                                    @[reducible]

                                    Shared library for --load-dynlib.

                                    Equations
                                    Instances For
                                      @[reducible]

                                      A Lean library's Lean modules.

                                      Equations
                                      Instances For
                                        @[reducible]

                                        The package's array of dependencies.

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

                                            Module Infos #

                                            @[reducible, inline]
                                            abbrev Lake.Module.facetCore (facet : Lean.Name) (self : Module) :

                                            Build info for applying the specified facet to the module. It is the user's obiligation to ensure the facet in question is a module facet.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Lake.Module.facet (facet : Lean.Name) (self : Module) :

                                              Build info for a module facet.

                                              Equations
                                              Instances For
                                                @[reducible, inline, deprecated Lake.Module.facetCore (since := "2025-03-04")]
                                                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]
                                                                abbrev Lake.Module.c (self : Module) :

                                                                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]
                                                                    abbrev Lake.Module.o (self : Module) :

                                                                    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

                                                                                    Package Infos #

                                                                                    @[reducible, inline]
                                                                                    abbrev Lake.Package.target (target : Lean.Name) (self : Package) :

                                                                                    Build info for a package target (e.g., a library, executable, or custom target).

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline]
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline]
                                                                                        abbrev Lake.Package.facet (facet : Lean.Name) (self : Package) :

                                                                                        Build info for a package facet.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline, deprecated Lake.Package.facetCore (since := "2025-03-04")]
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline]

                                                                                            A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline]

                                                                                              A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[reducible, inline]

                                                                                                A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible, inline]

                                                                                                  A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[reducible, inline]

                                                                                                    A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[reducible, inline]

                                                                                                      A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible, inline, deprecated Lake.Package.gitHubRelease (since := "2024-09-27")]
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[reducible, inline, deprecated Lake.Package.optGitHubRelease (since := "2024-09-27")]
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[reducible, inline]

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

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[reducible, inline]

                                                                                                              The package's array of dependencies.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[reducible, inline]

                                                                                                                The package's complete array of transitive dependencies.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Lean Library Infos #

                                                                                                                  @[reducible, inline]
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[reducible, inline]
                                                                                                                    abbrev Lake.LeanLib.facet (facet : Lean.Name) (self : LeanLib) :

                                                                                                                    Build info for a facet of a Lean library.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[reducible, inline, deprecated Lake.LeanLib.facetCore (since := "2025-03-04")]
                                                                                                                      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).

                                                                                                                              Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.

                                                                                                                              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

                                                                                                                                    Lean Executable Infos #

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

                                                                                                                                      Build info of the Lean executable.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible, inline, deprecated Lake.LeanExe.exe (since := "2025-03-04")]
                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          External Library Infos #

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

                                                                                                                                            Build info of the external library's static binary.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline, deprecated Lake.ExternLib.static (since := "2025-03-04")]
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[reducible, inline]

                                                                                                                                                Build info of the external library's shared binary.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[reducible, inline, deprecated Lake.ExternLib.shared (since := "2025-03-04")]
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[reducible, inline]

                                                                                                                                                    Build info of the external library's dynlib.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[reducible, inline, deprecated Lake.ExternLib.dynlib (since := "2025-03-04")]
                                                                                                                                                      Equations
                                                                                                                                                      Instances For

                                                                                                                                                        Input File & Directory Infos #

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

                                                                                                                                                          Build info of the input file's default facet.

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

                                                                                                                                                              Build info of the input directory's default facet.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For