Common Build Tools

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

General Utilities

instance Lake.instMonadWorkspaceJobM : MonadWorkspace JobM

Equations

• Lake.instMonadWorkspaceJobM = inferInstance

def Lake.platformTrace : BuildTrace

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

• Lake.platformTrace = Lake.BuildTrace.ofHash (Lake.pureHash System.Platform.target) System.Platform.target

@[inline]

def Lake.addPlatformTrace : JobM PUnit

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

• Lake.addPlatformTrace = Lake.addTrace Lake.platformTrace

@[inline]

def Lake.addLeanTrace : JobM PUnit

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

Equations

• Lake.addLeanTrace = do let __do_lift ← Lake.getLeanTrace Lake.addTrace __do_lift

@[inline]

def Lake.addPureTrace {α : Type u_1} [ToString α] [ComputeHash α Id] (a : α) (caption : String := "pure") : JobM PUnit

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

Equations

• Lake.addPureTrace a caption = Lake.addTrace (Lake.BuildTrace.ofHash (Lake.pureHash a) (toString caption ++ toString ": " ++ toString (toString a)))

structure Lake.BuildMetadata : Type

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

• depHash : Hash
• inputs : Array (String × Lean.Json)
• outputs? : Option Lean.Json
• log : Log
• synthetic : Bool

  A trace file that was created from fetching an artifact from the cache.

def Lake.BuildMetadata.toJson (self : BuildMetadata) : Lean.Json

Equations

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

instance Lake.instToJsonBuildMetadata : Lean.ToJson BuildMetadata

Equations

• Lake.instToJsonBuildMetadata = { toJson := Lake.BuildMetadata.toJson }

def Lake.BuildMetadata.ofStub (hash : Hash) : BuildMetadata

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

Equations

• Lake.BuildMetadata.ofStub hash = { depHash := hash, inputs := #[], outputs? := none, log := ∅, synthetic := false }

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

abbrev Lake.BuildMetadata.ofHash (hash : Hash) : BuildMetadata

Equations

• Lake.BuildMetadata.ofHash = Lake.BuildMetadata.ofStub

def Lake.BuildMetadata.fromJsonObject? (obj : JsonObject) : Except String BuildMetadata

Equations

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

def Lake.BuildMetadata.fromJson? (json : Lean.Json) : Except String BuildMetadata

Equations

• One or more equations did not get rendered due to their size.
• Lake.BuildMetadata.fromJson? json = Lake.error (toString "unknown trace format: expected JSON number or object")

instance Lake.instFromJsonBuildMetadata : Lean.FromJson BuildMetadata

Equations

• Lake.instFromJsonBuildMetadata = { fromJson? := Lake.BuildMetadata.fromJson? }

def Lake.BuildMetadata.parse (contents : String) : Except String BuildMetadata

Parse build metadata from a trace file's contents.

Equations

• Lake.BuildMetadata.parse contents = Lean.Json.parse contents >>= Lean.fromJson?

def Lake.BuildMetadata.ofFetch (inputHash : Hash) (outputs : Lean.Json) : BuildMetadata

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

Equations

• Lake.BuildMetadata.ofFetch inputHash outputs = { depHash := inputHash, inputs := #[], outputs? := some outputs, log := ∅, synthetic := true }

@[inline]

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

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

Equations

• Lake.BuildMetadata.ofBuild depTrace outputs log = Lake.BuildMetadata.ofBuildCore✝ depTrace (Lean.toJson outputs) log

inductive Lake.SavedTrace : Type

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

• missing : SavedTrace
• invalid : SavedTrace
• ok (data : BuildMetadata) : SavedTrace

def Lake.readTraceFile (path : System.FilePath) : LogIO SavedTrace

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.

@[inline, deprecated Lake.readTraceFile (since := "2025-06-26")]

def Lake.readTraceFile? (path : System.FilePath) : LogIO (Option BuildMetadata)

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

Equations

• Lake.readTraceFile? path = do let __do_lift ← Lake.readTraceFile path match __do_lift with | Lake.SavedTrace.ok data => pure (some data) | x => liftM none

def Lake.BuildMetadata.writeFile (path : System.FilePath) (data : BuildMetadata) : IO Unit

Write a trace file containing the metadata.

Equations

• Lake.BuildMetadata.writeFile path data = do Lake.createParentDirs path IO.FS.writeFile path (Lean.toJson data).pretty

@[inline]

def Lake.writeFetchTrace (path : System.FilePath) (inputHash : Hash) (outputs : Lean.Json) : IO Unit

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

Equations

• Lake.writeFetchTrace path inputHash outputs = Lake.BuildMetadata.writeFile path (Lake.BuildMetadata.ofFetch inputHash outputs)

@[inline]

def Lake.writeBuildTrace {α : Type u_1} [Lean.ToJson α] (path : System.FilePath) (depTrace : BuildTrace) (outputs : α) (log : Log) : IO Unit

Write a trace file containing metadata about a build.

Equations

• Lake.writeBuildTrace path depTrace outputs log = Lake.BuildMetadata.writeFile path (Lake.BuildMetadata.ofBuild depTrace outputs log)

@[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) : IO Unit

Equations

• @Lake.writeTraceFile = @Lake.writeBuildTrace

inductive Lake.OutputStatus : Type

Indicator of whether a build's output(s) are up-to-date.

• outOfDate : OutputStatus

  Needs rebuild

• mtimeUpToDate : OutputStatus

  Up-to-date by modification time

• hashUpToDate : OutputStatus

  Up-to-date by hash

instance Lake.instDecidableEqOutputStatus : DecidableEq OutputStatus

Equations

• Lake.instDecidableEqOutputStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[inline]

def Lake.OutputStatus.ofHashCheck (upToDate : Bool) : OutputStatus

Constructs an OutputStatus from a hash check.

Equations

• Lake.OutputStatus.ofHashCheck upToDate = if upToDate = true then Lake.OutputStatus.hashUpToDate else Lake.OutputStatus.outOfDate

@[inline]

def Lake.OutputStatus.ofMTimeCheck (upToDate : Bool) : OutputStatus

Constructs an OutputStatus from a modification time check.

Equations

• Lake.OutputStatus.ofMTimeCheck upToDate = if upToDate = true then Lake.OutputStatus.mtimeUpToDate else Lake.OutputStatus.outOfDate

@[inline]

def Lake.OutputStatus.isUpToDate (status : OutputStatus) : Bool

Whether the build should be considered up-to-date for rebuilding.

Equations

• status.isUpToDate = (status != Lake.OutputStatus.outOfDate)

@[inline]

def Lake.OutputStatus.isCacheable (status : OutputStatus) : Bool

Whether the build or rebuild should be considered up-to-date for caching.

Equations

• status.isCacheable = (status != Lake.OutputStatus.mtimeUpToDate)

@[inline]

def Lake.checkHashUpToDate {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (depHash : Option Hash) (oldTrace : MTime := depTrace.mtime) : JobM Bool

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

• Lake.checkHashUpToDate info depTrace depHash oldTrace = (fun (x : Lake.OutputStatus) => x.isUpToDate) <$> Lake.checkHashUpToDate'✝ info depTrace depHash oldTrace

@[specialize #[]]

def Lake.SavedTrace.replayIfUpToDate' {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (savedTrace : SavedTrace) (oldTrace : MTime := depTrace.mtime) : JobM OutputStatus

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

Equations

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

@[inline]

def Lake.SavedTrace.replayIfUpToDate {ι : Type u_1} [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (savedTrace : SavedTrace) (oldTrace : MTime := depTrace.mtime) : JobM Bool

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

Equations

• Lake.SavedTrace.replayIfUpToDate info depTrace savedTrace oldTrace = (fun (x : Lake.OutputStatus) => x.isUpToDate) <$> Lake.SavedTrace.replayIfUpToDate' info depTrace savedTrace oldTrace

def Lake.SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool

Returns if the saved trace exists and its hash matches inputHash.

If up-to-date, replays the saved log from the trace and sets the current build action to replay. Otherwise, if the log is empty and trace is synthetic, or if the trace is not up-to-date, the build action will be set ot fetch.

Equations

• One or more equations did not get rendered due to their size.
• Lake.SavedTrace.replayOrFetchIfUpToDate inputHash self = do let y ← pure PUnit.unit (fun (y : PUnit) => do Lake.updateAction Lake.JobAction.fetch pure false) y

class Lake.ToOutputJson (α : Type u) : Type u

For internal use only.

• toOutputJson (arts : α) : Lean.Json

instance Lake.instToOutputJsonPUnit : ToOutputJson PUnit

Equations

• Lake.instToOutputJsonPUnit = { toOutputJson := fun (x : PUnit) => Lean.Json.null }

instance Lake.instToOutputJsonArtifact : ToOutputJson Artifact

Equations

• Lake.instToOutputJsonArtifact = { toOutputJson := fun (x : Lake.Artifact) => Lean.toJson x.descr }

@[specialize #[]]

def Lake.buildAction {α : Type} [ToOutputJson α] (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), JSON description of 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.

@[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) : JobM Bool

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.

@[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) : JobM PUnit

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

• Lake.buildUnlessUpToDate info depTrace traceFile build action oldTrace = discard (Lake.buildUnlessUpToDate? info depTrace traceFile build action oldTrace)

def Lake.writeFileHash (file : System.FilePath) (hash : Hash) : IO Unit

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

Equations

• Lake.writeFileHash file hash = do Lake.createParentDirs { toString := file.toString ++ ".hash" } IO.FS.writeFile { toString := file.toString ++ ".hash" } hash.toString

def Lake.cacheFileHash (file : System.FilePath) (text : Bool := false) : IO Unit

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

• Lake.cacheFileHash file text = do let hash ← Lake.computeFileHash file text Lake.writeFileHash file hash

def Lake.clearFileHash (file : System.FilePath) : IO Unit

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

Equations

• Lake.clearFileHash file = Lake.removeFileIfExists { toString := file.toString ++ ".hash" }

def Lake.fetchFileHash (file : System.FilePath) (text : Bool := false) : JobM Hash

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.

def Lake.fetchFileTrace (file : System.FilePath) (text : Bool := false) : JobM BuildTrace

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

• Lake.fetchFileTrace file text = do let hash ← Lake.fetchFileHash file text let mtime ← liftM (Lake.getMTime file) pure { caption := file.toString, hash := hash, mtime := mtime }

def Lake.buildFileUnlessUpToDate' (file : System.FilePath) (build : JobM PUnit) (text : Bool := false) : JobM Unit

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.

def Lake.Cache.saveArtifact (cache : Cache) (file : System.FilePath) (ext : String := "art") (text exe useLocalFile : Bool := false) : IO Artifact

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

Additional Options:

• text: the contents of file are hashed as text rather than as a binary blob.
• exe: the cached file will be executable.
• useLocalFile: the resulting artifact will use file's path instead of path to the file in the cache.

Equations

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

@[inline]

def Lake.cacheArtifact {m : Type → Type u_1} [MonadWorkspace m] [MonadLiftT IO m] [Monad m] (file : System.FilePath) (ext : String := "art") (text exe useLocalFile : Bool := false) : m Artifact

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

Additional Options:

• text: the contents of file are hashed as text rather than as a binary blob.
• exe: the cached file will be executable.
• useLocalFile: the resulting artifact will use file's path instead of path to the file in the cache.

Equations

• Lake.cacheArtifact file ext text exe useLocalFile = do let __do_lift ← Lake.getLakeCache liftM (__do_lift.saveArtifact file ext text exe useLocalFile)

class Lake.ResolveOutputs (m : Type v → Type w) (α : Type v) : Type w

For internal use only.

• resolveOutputs? (outputs : Lean.Json) : m (Except String α)

  For internal use only.

@[specialize #[]]

def Lake.getArtifacts? {α : Type} [ResolveOutputs JobM α] (inputHash : Hash) (savedTrace : SavedTrace) (cache : Cache) (pkg : Package) : JobM (Option α)

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

For internal use only.

Equations

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

def Lake.computeArtifact (path : System.FilePath) (ext : String := "art") (text : Bool := false) : JobM Artifact

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.

def Lake.buildArtifactUnlessUpToDate (file : System.FilePath) (build : JobM PUnit) (text : Bool := false) (ext : String := "art") (restore exe : Bool := false) : JobM Artifact

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.

@[inline]

def Lake.buildFileAfterDep {α : Type u_1} (file : System.FilePath) (dep : Job α) (build : α → JobM PUnit) (extraDepTrace : JobM BuildTrace := pure BuildTrace.nil) (text : Bool := false) : SpawnM (Job System.FilePath)

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.

Common Builds

def Lake.inputBinFile (path : System.FilePath) : SpawnM (Job System.FilePath)

A build job for a 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

• Lake.inputBinFile path = Lake.Job.async do let __do_lift ← Lake.computeTrace path Lake.setTrace __do_lift pure path

def Lake.inputTextFile (path : System.FilePath) : SpawnM (Job System.FilePath)

A build job for a 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

• Lake.inputTextFile path = Lake.Job.async do let __do_lift ← Lake.computeTrace { path := path } Lake.setTrace __do_lift pure path

@[inline]

def Lake.inputFile (path : System.FilePath) (text : Bool) : SpawnM (Job System.FilePath)

A build job for a 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

• Lake.inputFile path text = if text = true then Lake.inputTextFile path else Lake.inputBinFile path

def Lake.inputDir (path : System.FilePath) (text : Bool) (filter : System.FilePath → Bool) : SpawnM (Job (Array System.FilePath))

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.

@[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) : SpawnM (Job System.FilePath)

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.

def Lake.buildLeanO (oFile : System.FilePath) (srcJob : Job System.FilePath) (weakArgs traceArgs : Array String := #[]) (leanIncludeDir? : Option System.FilePath := none) : SpawnM (Job System.FilePath)

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.

def Lake.buildStaticLib (libFile : System.FilePath) (oFileJobs : Array (Job System.FilePath)) (thin : Bool := false) : SpawnM (Job System.FilePath)

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.

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) : SpawnM (Job Dynlib)

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.

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) : SpawnM (Job Dynlib)

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.

def Lake.buildLeanExe (exeFile : System.FilePath) (linkObjs : Array (Job System.FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false) : SpawnM (Job System.FilePath)

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.