Documentation

def Lake.noBuildCode :

ExitCode

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

Equations

Lake.noBuildCode = 3

def Lake.platformTrace :

Hash

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.pureHash System.Platform.target

@[inline]

def Lake.addPlatformTrace :

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.BuildTrace.ofHash Lake.platformTrace)

@[inline]

def Lake.addLeanTrace :

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} [ComputeHash α Id] (a : α) :

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

Equations

Lake.addPureTrace a = Lake.addTrace (Lake.BuildTrace.ofHash (Lake.pureHash a))

structure Lake.BuildMetadata :

Type

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

depHash : Hash
log : Log

Instances For

Lean.ToJson BuildMetadata

instance Lake.instToJsonBuildMetadata :

Equations

Lake.instToJsonBuildMetadata = { toJson := Lake.toJsonBuildMetadata✝ }

def Lake.BuildMetadata.ofHash (h : Hash) :

BuildMetadata

Equations

Lake.BuildMetadata.ofHash h = { depHash := h, log := ∅ }

Except String BuildMetadata

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

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 }

Lean.FromJson BuildMetadata

instance Lake.instFromJsonBuildMetadata :

Equations

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

def Lake.readTraceFile? (path : System.FilePath) :

LogIO (Option BuildMetadata)

Read persistent trace data from a file.

Equations

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

def Lake.writeTraceFile (path : System.FilePath) (depTrace : BuildTrace) (log : Log) :

IO Unit

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

@[specialize #[]]

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

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

@[specialize #[]]

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.

def Lake.buildUnlessUpToDate?.go (depTrace : BuildTrace) (traceFile : System.FilePath) (build : JobM PUnit) (action : JobAction := JobAction.build) :

JobM Bool

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) :

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.cacheFileHash (file : System.FilePath) :

IO Unit

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.

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

IO Unit

Remove the cached hash of a file (its .hash file).

Equations

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

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 __do_lift ← Lake.fetchFileHash file text let __do_lift_1 ← liftM (Lake.getMTime file) pure { hash := __do_lift, mtime := __do_lift_1 }

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, save the new trace 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 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 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.

@[reducible, inline, deprecated Lake.buildFileUnlessUpToDate' (since := "2024-12-06")]

abbrev Lake.buildFileUnlessUpToDate (file : System.FilePath) (depTrace : BuildTrace) (build : JobM PUnit) (text : Bool := false) :

JobM BuildTrace

Equations

Lake.buildFileUnlessUpToDate file depTrace build text = do Lake.setTrace depTrace Lake.buildFileUnlessUpToDate' file build text Lake.getTrace

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

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

Lake.buildFileAfterDepList file deps build extraDepTrace text = Lake.buildFileAfterDep file (Lake.Job.collectList deps) build extraDepTrace text

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

Lake.buildFileAfterDepArray file deps build extraDepTrace text = Lake.buildFileAfterDep file (Lake.Job.collectArray deps) build extraDepTrace text

Common Builds #

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

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

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

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

@[inline]

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

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

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) :

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 := #[]) :

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) :

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) :

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) :

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) :