Common Build Tools #
This file defines general utilities that abstract common build functionality and provides some common concrete build functions.
General Utilities #
Build trace for the host platform. If an artifact includes this in its trace, it is platform-dependent and will be rebuilt on different host platforms.
Instances For
The build trace file format, which stores information about a (successful) build.
Instances For
Equations
- Lake.instToJsonBuildMetadata = { toJson := Lake.toJsonBuildMetadata✝ }
Equations
- Lake.BuildMetadata.ofHash h = { depHash := h, log := ∅ }
Instances For
Equations
- Lake.BuildMetadata.fromJson? json = do let obj ← Lake.JsonObject.fromJson? json let depHash ← obj.get "depHash" let log ← obj.getD "log" ∅ pure { depHash := depHash, log := log }
Instances For
Equations
- Lake.instFromJsonBuildMetadata = { fromJson? := Lake.BuildMetadata.fromJson? }
Read persistent trace data from a file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Write persistent trace data to a file.
Equations
- Lake.writeTraceFile path depTrace log = do Lake.createParentDirs path let data : Lake.BuildMetadata := { depHash := depTrace.hash, log := log } IO.FS.writeFile path (Lean.toJson data).pretty
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 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
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
Computes the hash of a file and saves it to a .hash
file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Remove the cached hash of a file (its .hash
file).
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 __do_lift ← Lake.fetchFileHash file text let __do_lift_1 ← liftM (Lake.getMTime file) pure { hash := __do_lift, mtime := __do_lift_1 }
Instances For
Builds file
using build
unless it already exists and depTrace
matches
the trace stored in the .trace
file. If built, save the new depTrace
and
cache file
's hash in a .hash
file. Otherwise, try to fetch the hash from
the .hash
file using fetchFileTrace
. Build logs (if any) are saved to
a .log.json
file and replayed from there if the build is skipped.
For example, given file := "foo.c"
, compares depTrace
with that in
foo.c.trace
with the hash cached in foo.c.hash
and the log cached in
foo.c.trace
.
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
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.BuildJob.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.BuildJob.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 ((fun (x : Lake.BuildTrace) => (path, x)) <$> Lake.computeTrace 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 ((fun (x : Lake.BuildTrace) => (path, x)) <$> Lake.computeTrace { path := 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
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 BuildJob
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 leanc
.
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 ar
packaged with Lean.
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 leanc
.
Equations
- One or more equations did not get rendered due to their size.