# Common Build Tools #

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

## General Utilities #

source
instance Lake.instMonadWorkspaceJobM :
MonadWorkspace JobM
Equations

- Lake.instMonadWorkspaceJobM = inferInstance

source
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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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)))

Instances For

source
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.

Instances For

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

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

Instances For

source
instance Lake.instToJsonBuildMetadata :
Lean.ToJson BuildMetadata
Equations

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

source
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 }

Instances For

source
@[reducible, inline, deprecated Lake.BuildMetadata.ofStub (since := "2025-06-28")]
abbrev Lake.BuildMetadata.ofHash (hash : Hash) :
BuildMetadata
Equations

- Lake.BuildMetadata.ofHash = Lake.BuildMetadata.ofStub

Instances For

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

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

Instances For

source
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")

Instances For

source
instance Lake.instFromJsonBuildMetadata :
Lean.FromJson BuildMetadata
Equations

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

source
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?

Instances For

source
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 }

Instances For

source
@[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

Instances For

source
inductive Lake.SavedTrace :
Type

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

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

Instances For

source
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.

Instances For

source
@[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

Instances For

source
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

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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

Instances For

source
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

Instances For

source
instance Lake.instDecidableEqOutputStatus :
DecidableEq OutputStatus
Equations

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

source
@[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

Instances For

source
@[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

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[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

Instances For

source
@[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.

Instances For

source
@[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

Instances For

source
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

Instances For

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

For internal use only.

- toOutputJson (arts : α) : Lean.Json

Instances

source
instance Lake.instToOutputJsonPUnit :
ToOutputJson PUnit
Equations

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

source
instance Lake.instToOutputJsonArtifact :
ToOutputJson Artifact
Equations

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

source
@[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.

Instances For

source
@[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.

Instances For

source
@[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)

Instances For

source
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

Instances For

source
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

Instances For

source
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" }

Instances For

source
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.

Instances For

source
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 }

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[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)

Instances For

source
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.

Instances

source
@[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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[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.

Instances For

## Common Builds #

source
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

Instances For

source
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

Instances For

source
@[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

Instances For

source
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.

Instances For

source
@[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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For