Documentation

Lake.Build.Common

Common Build Tools #

This file defines general utilities that abstract common build functionality and provides some common concrete build functions.

General Utilities #

Exit code to return if --no-build is set and a build is required.

Equations
Instances For

    Build trace for the host platform. If an artifact includes this trace, it is platform-dependent and will be rebuilt on different host platforms.

    Equations
    Instances For
      @[inline]

      Mixes the platform into the current job's trace. If an artifact includes this trace, it is platform-dependent and will be rebuilt on different host platforms.

      Equations
      Instances For
        @[inline]

        Mixes Lean's trace into the current job's trace.

        Equations
        Instances For
          @[inline]
          def Lake.addPureTrace {α : Type u_1} [ToString α] [ComputeHash α Id] (a : α) (caption : String := "pure") :

          Mixes the trace of a pure value into the current job's trace.

          Equations
          Instances For

            The build trace file format, which stores information about a (successful) build.

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

                Construct build metadata from a trace stub. That is, the old version of the trace file format that just contained a hash.

                Equations
                Instances For
                  @[reducible, inline, deprecated Lake.BuildMetadata.ofStub (since := "2025-06-28")]
                  Equations
                  Instances For

                    Parse build metadata from a trace file's contents.

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

                      Construct build metadata from a cached input-to-output mapping.

                      Equations
                      Instances For
                        @[inline]
                        def Lake.BuildMetadata.ofBuild {α : Type u_1} [Lean.ToJson α] (depTrace : BuildTrace) (outputs : α) (log : Log) :

                        Construct trace file contents from a build's trace, outputs, and log.

                        Equations
                        Instances For

                          The state of the trace file data saved on the file system.

                          Instances For

                            Try to read data from a trace file. Logs if the read failed or the contents where invalid.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[inline, deprecated Lake.readTraceFile (since := "2025-06-26")]

                              Tries to read data from a trace file. On failure, returns none. Logs if the read failed or the contents where invalid.

                              Equations
                              Instances For

                                Write a trace file containing the metadata.

                                Equations
                                Instances For
                                  @[inline]
                                  def Lake.writeFetchTrace (path : System.FilePath) (inputHash : Hash) (outputs : Lean.Json) :

                                  Write a trace file containing metadata on an artifact fetched from a cache.

                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lake.writeBuildTrace {α : Type u_1} [Lean.ToJson α] (path : System.FilePath) (depTrace : BuildTrace) (outputs : α) (log : Log) :

                                    Write a trace file containing metadata about a build.

                                    Equations
                                    Instances For
                                      @[reducible, inline, deprecated Lake.writeBuildTrace (since := "2025-06-28")]
                                      abbrev Lake.writeTraceFile {α : Type u_1} [Lean.ToJson α] (path : System.FilePath) (depTrace : BuildTrace) (outputs : α) (log : Log) :
                                      Equations
                                      Instances For
                                        @[specialize #[]]
                                        def Lake.checkHashUpToDate {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (depHash : Option Hash) (oldTrace : MTime := depTrace.mtime) :

                                        Checks if the info is up-to-date by comparing depTrace with depHash. If old mode is enabled (e.g., --old), uses the oldTrace modification time as the point of comparison instead.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[specialize #[]]
                                          def Lake.SavedTrace.replayIfUpToDate {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (savedTrace : SavedTrace) (oldTrace : MTime := depTrace.mtime) :

                                          Checks whether info is up-to-date, and replays the log of the trace if available.

                                          Equations
                                          Instances For
                                            def Lake.SavedTrace.replayOrFetch (traceFile : System.FilePath) (inputHash : Hash) (outputs : Lean.Json) (savedTrace : SavedTrace) :

                                            Replays the saved log from the trace if it exists and is not synthetic. Otherwise, writes a new synthetic trace file recording the fetch of the artifact from the cache.

                                            Equations
                                            Instances For
                                              @[specialize #[]]
                                              def Lake.buildAction {α : Type} [Lean.ToJson α] (depTrace : BuildTrace) (traceFile : System.FilePath) (build : JobM α) (action : JobAction := JobAction.build) :
                                              JobM α

                                              Runs build as a build action of kind action.

                                              The build's input trace (depTrace), output hashes (the result of build), and log are saved to traceFile, if the build completes without a fatal error (i.e., it does not throw).

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[inline]
                                                def Lake.buildUnlessUpToDate? {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (traceFile : System.FilePath) (build : JobM PUnit) (action : JobAction := JobAction.build) (oldTrace : MTime := depTrace.mtime) :

                                                Checks whether info is up-to-date, and runs build to recreate it if not. If rebuilt, saves the new depTrace and build log to traceFile. Returns whether info was already up-to-date.

                                                Up-to-date Checking

                                                If traceFile exists, checks that the hash in depTrace matches that of the traceFile. If not, and old mode is enabled (e.g., --old), falls back to the oldTrace modification time as the point of comparison. If up-to-date, replay the build log stored in traceFile.

                                                If traceFile does not exist, checks that info has a newer modification time then depTrace / oldTrace. No log will be replayed.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[inline]
                                                  def Lake.buildUnlessUpToDate {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (traceFile : System.FilePath) (build : JobM PUnit) (action : JobAction := JobAction.build) (oldTrace : MTime := depTrace.mtime) :

                                                  Checks whether info is up-to-date, and runs build to recreate it if not. If rebuilt, saves the new depTrace and build log to traceFile.

                                                  See buildUnlessUpToDate? for more details on how Lake determines whether info is up-to-date.

                                                  Equations
                                                  Instances For

                                                    Saves the hash of a file and to its .hash file.

                                                    Equations
                                                    Instances For

                                                      Computes the hash of a file and saves it to a .hash file.

                                                      If text := true, file is hashed as a text file rather than a binary file.

                                                      Equations
                                                      Instances For

                                                        Remove the cached hash of a file (its .hash file) if it exists.

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

                                                          Fetches the hash of a file that may already be cached in a .hash file. If hash files are not trusted (e.g., with --rehash) or the .hash file does not exist, it will be created with a newly computed hash.

                                                          If text := true, file is hashed as a text file rather than a binary file.

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

                                                            Fetches the trace of a file that may have already have its hash cached in a .hash file. If no such .hash file exists, recomputes and creates it.

                                                            If text := true, file is hashed as text file rather than a binary file.

                                                            Equations
                                                            Instances For

                                                              Builds file using build unless it already exists and the current job's trace matches the trace stored in the .trace file. If built, saves the new trace and caches file's hash in a .hash file. Otherwise, tries to fetch the hash from the .hash file using fetchFileTrace. Build logs (if any) are saved to the trace file and replayed from there if the build is skipped.

                                                              For example, given file := "foo.c", compares getTrace with that in foo.c.trace. If built, the hash is cached in foo.c.hash and the new trace is saved to foo.c.trace (including the build log).

                                                              If text := true, file is hashed as a text file rather than a binary file.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[reducible, inline, deprecated Lake.buildFileUnlessUpToDate' (since := "2024-12-06")]
                                                                abbrev Lake.buildFileUnlessUpToDate (file : System.FilePath) (depTrace : BuildTrace) (build : JobM PUnit) (text : Bool := false) :
                                                                Equations
                                                                Instances For
                                                                  def Lake.Cache.saveArtifact (cache : Cache) (file : System.FilePath) (ext : String := "art") (text exe : Bool := false) :

                                                                  Copies file to the Lake cache with the file extension ext, and saves its hash in its .hash file.

                                                                  If text := true, file contents are hashed as a text file rather than a binary file.

                                                                  If the Lake cache is disabled, the behavior of this function is undefined.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[inline]
                                                                    def Lake.cacheArtifact {m : TypeType u_1} [MonadLakeEnv m] [MonadLiftT IO m] [Monad m] (file : System.FilePath) (ext : String := "art") (text exe : Bool := false) :

                                                                    Copies file to the Lake cache with the file extension ext, and saves its hash in its .hash file.

                                                                    If text := true, file contents are hashed as a text file rather than a binary file.

                                                                    If the Lake cache is disabled, the behavior of this function is undefined.

                                                                    Equations
                                                                    Instances For
                                                                      def Lake.computeArtifactTrace (buildFile art : System.FilePath) (contentHash : Hash) :

                                                                      Computes the trace of a cached artifact. buildFile is where the uncached artifact would be located.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        class Lake.ResolveArtifacts (m : Type v → Type w) (α : Type u) (β : outParam (Type v)) :
                                                                        Type (max u w)
                                                                        • resolveArtifacts? (contentHashes : α) : m (Option β)
                                                                        Instances
                                                                          @[specialize #[]]
                                                                          def Lake.resolveArtifactsUsing? {β : Type} (α : Type u) [Lean.FromJson α] [ResolveArtifacts JobM α β] (inputHash : Hash) (traceFile : System.FilePath) (savedTrace : SavedTrace) (cache : CacheRef) :

                                                                          Retrieve artifacts from the Lake cache using the the content hashes stored as α in either the saved trace file or in the cached input-to-content mapping.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            structure Lake.FileOutputHash (ext : String) :

                                                                            The content hash of an artifact which is stored with extension ext in the Lake cache.

                                                                            Instances For

                                                                              Construct an artifact from a path outside the Lake artifact cache.

                                                                              If text := true, file is hashed as a text file rather than a binary file.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                def Lake.buildArtifactUnlessUpToDate (file : System.FilePath) (build : JobM PUnit) (text : Bool := false) (ext : String := "art") (restore exe : Bool := false) :

                                                                                Uses the current job's trace to search Lake's local artifact cache for an artifact with a matching extension (ext) and content hash. If one is found, use it. Otherwise, builds file using build and saves it to the cache. If Lake's local artifact cache is not enabled, falls back to buildFileUnlessUpToDate'.

                                                                                If text := true, file is hashed as a text file rather than a binary file.

                                                                                If restore := true, if file is missing but the artifact is in the cache, it will be copied to the file. This function will also return file rather than the path to the cached artifact.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  def Lake.buildArtifactUnlessUpToDate.doBuild (file : System.FilePath) (build : JobM PUnit) (text : Bool := false) (depTrace : BuildTrace) (traceFile : System.FilePath) :
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Lake.buildFileAfterDep {α : Type u_1} (file : System.FilePath) (dep : Job α) (build : αJobM PUnit) (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) (text : Bool := false) :

                                                                                    Build file using build after dep completes if the dependency's trace (and/or extraDepTrace) has changed.

                                                                                    If text := true, file is handled as a text file rather than a binary file.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      @[reducible, inline, deprecated Lake.buildFileAfterDep (since := "2024-12-06")]
                                                                                      abbrev Lake.buildFileAfterDepList {α : Type u_1} (file : System.FilePath) (deps : List (Job α)) (build : List αJobM PUnit) (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) (text : Bool := false) :

                                                                                      Build file using build after deps have built if any of their traces change.

                                                                                      If text := true, file is handled as a text file rather than a binary file.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline, deprecated Lake.buildFileAfterDep (since := "2024-12-06")]
                                                                                        def Lake.buildFileAfterDepArray {α : Type u_1} (file : System.FilePath) (deps : Array (Job α)) (build : Array αJobM PUnit) (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) (text : Bool := false) :

                                                                                        Build file using build after deps have built if any of their traces change.

                                                                                        If text := true, file is handled as a text file rather than a binary file.

                                                                                        Equations
                                                                                        Instances For

                                                                                          Common Builds #

                                                                                          A build job for binary file that is expected to already exist (e.g., a data blob).

                                                                                          Any byte difference in a binary file will trigger a rebuild of its dependents.

                                                                                          Equations
                                                                                          Instances For

                                                                                            A build job for text file that is expected to already exist (e.g., a source file).

                                                                                            Text file traces have normalized line endings to avoid unnecessary rebuilds across platforms.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]

                                                                                              A build job for file that is expected to already exist (e.g., a data blob or source file).

                                                                                              If text := true, the file is handled as a text file rather than a binary file. Any byte difference in a binary file will trigger a rebuild of its dependents. In contrast, text file traces have normalized line endings to avoid unnecessary rebuilds across platforms.

                                                                                              Equations
                                                                                              Instances For

                                                                                                A build job for a directory of files that are expected to already exist. Returns an array of the files in the directory that match the filter.

                                                                                                If text := true, the files are handled as text files rather than a binary files. Any byte difference in a binary file will trigger a rebuild of its dependents. In contrast, text file traces have normalized line endings to avoid unnecessary rebuilds across platforms.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Lake.buildO (oFile : System.FilePath) (srcJob : Job System.FilePath) (weakArgs traceArgs : Array String := #[]) (compiler : System.FilePath := { toString := "cc" }) (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) :

                                                                                                  Build an object file from a source file job using compiler. The invocation is:

                                                                                                  compiler -c -o oFile srcFile weakArgs... traceArgs...
                                                                                                  

                                                                                                  The traceArgs are included as part of the dependency trace hash, whereas the weakArgs are not. Thus, system-dependent options like -I or -L should be weakArgs to avoid build artifact incompatibility between systems (i.e., a change in the file path should not cause a rebuild).

                                                                                                  You can add more components to the trace via extraDepTrace, which will be computed in the resulting Job before building.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    def Lake.buildLeanO (oFile : System.FilePath) (srcJob : Job System.FilePath) (weakArgs traceArgs : Array String := #[]) (leanIncludeDir? : Option System.FilePath := none) :

                                                                                                    Build an object file from a source fie job (i.e, a lean -c output) using the Lean toolchain's C compiler.

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

                                                                                                      Build a static library from object file jobs using the Lean toolchain's ar.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        def Lake.buildSharedLib (libName : String) (libFile : System.FilePath) (linkObjs : Array (Job System.FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (linker : String := "c++") (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) (plugin : Bool := false) (linkDeps : Bool := System.Platform.isWindows) :

                                                                                                        Build a shared library by linking the results of linkJobs using the Lean toolchain's C compiler.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          def Lake.buildLeanSharedLib (libName : String) (libFile : System.FilePath) (linkObjs : Array (Job System.FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (plugin : Bool := false) (linkDeps : Bool := System.Platform.isWindows) :

                                                                                                          Build a shared library by linking the results of linkJobs using linker.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            def Lake.buildLeanExe (exeFile : System.FilePath) (linkObjs : Array (Job System.FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false) :

                                                                                                            Build an executable by linking the results of linkJobs using the Lean toolchain's linker.

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