Common Build Tools #
This file defines general utilities that abstract common build functionality and provides some common concrete build functions.
General Utilities #
Equations
Equations
- Lake.instToJsonPUnit_lake = { toJson := fun (x : PUnit) => Lean.Json.null }
Instances For
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
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.
Instances For
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
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 "" ++ toString caption ++ toString ": " ++ toString (toString a) ++ toString ""))
Instances For
Equations
- Lake.instToJsonBuildMetadata = { toJson := Lake.toJsonBuildMetadata✝ }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.instFromJsonBuildMetadata = { fromJson? := Lake.BuildMetadata.fromJson? }
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
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
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
The state of the trace file data saved on the file system.
- missing : SavedTrace
- invalid : SavedTrace
- ok (data : BuildMetadata) : SavedTrace
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
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
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
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
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
Equations
Instances For
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
Checks whether info
is up-to-date, and replays the log of the trace if available.
Equations
- One or more equations did not get rendered due to their size.
- Lake.SavedTrace.replayIfUpToDate info depTrace Lake.SavedTrace.missing oldTrace = liftM (Lake.BuildTrace.checkAgainstTime info depTrace)
Instances For
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
- One or more equations did not get rendered due to their size.
- Lake.SavedTrace.replayOrFetch traceFile inputHash outputs savedTrace = do Lake.updateAction Lake.JobAction.fetch liftM (Lake.writeFetchTrace traceFile inputHash outputs)
Instances For
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
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
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
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
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
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
- 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
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
Equations
- Lake.buildFileUnlessUpToDate file depTrace build text = do Lake.setTrace depTrace Lake.buildFileUnlessUpToDate' file build text Lake.getTrace
Instances For
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
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
- Lake.cacheArtifact file ext text exe = do let __do_lift ← Lake.getLakeCache liftM (__do_lift.saveArtifact file ext text exe)
Instances For
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
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
The content hash of an artifact which is stored with extension ext
in the Lake cache.
- hash : Hash
Instances For
Equations
- Lake.instToJsonFileOutputHash = { toJson := fun (x : Lake.FileOutputHash ext) => Lean.toJson x.hash }
Equations
- Lake.instFromJsonFileOutputHash = { fromJson? := fun (x : Lean.Json) => Lake.FileOutputHash.mk <$> Lean.fromJson? x }
Equations
- Lake.instResolveArtifactsFileOutputHashArtifactOfMonadLakeEnvOfMonadLiftTBaseIOOfMonad = { resolveArtifacts? := fun (x : Lake.FileOutputHash ext) => Lake.getArtifact? x.hash ext }
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
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
- Lake.buildFileAfterDepList file deps build extraDepTrace text = Lake.buildFileAfterDep file (Lake.Job.collectList deps) build extraDepTrace text
Instances For
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
- Lake.buildFileAfterDepArray file deps build extraDepTrace text = Lake.buildFileAfterDep file (Lake.Job.collectArray deps) build extraDepTrace text
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
- Lake.inputBinFile path = Lake.Job.async do let __do_lift ← Lake.computeTrace path Lake.setTrace __do_lift pure path
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
- Lake.inputTextFile path = Lake.Job.async do let __do_lift ← Lake.computeTrace { path := path } Lake.setTrace __do_lift pure path
Instances For
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
- Lake.inputFile path text = if text = true then Lake.inputTextFile path else Lake.inputBinFile path
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
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
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
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.