Common Build Tools

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

General Utilities

def Lake.platformTrace : Lake.Hash

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.

Equations

• Lake.platformTrace = Lake.pureHash System.Platform.target

@[specialize #[]]

def Lake.BuildTrace.checkUpToDate {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : Lake.FilePath) : Lake.JobM Bool

Check if the info is up-to-date by comparing depTrace with traceFile.

Equations

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

@[inline]

def Lake.buildUnlessUpToDate? {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : Lake.FilePath) (build : Lake.JobM PUnit) : Lake.JobM Bool

Build info unless it already exists and depTrace matches that of the traceFile. If rebuilt, save the new depTrace to the tracefile. Returns whether info was already up-to-date.

Equations

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

@[inline]

def Lake.buildUnlessUpToDate {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : Lake.FilePath) (build : Lake.JobM PUnit) : Lake.JobM PUnit

Build info unless it already exists and depTrace matches that of the traceFile. If rebuilt, save the new depTrace to the tracefile.

Equations

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

def Lake.fetchFileTrace (file : Lake.FilePath) : Lake.JobM Lake.BuildTrace

Fetch the trace of a file that may have its hash already cached in a .hash file.

Equations

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

def Lake.cacheFileHash (file : Lake.FilePath) : IO Lake.Hash

Compute the hash of a file and save it to a .hash file.

Equations

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

def Lake.replayBuildLog (logFile : Lake.FilePath) : Lake.LogIO PUnit

Replays the JSON log in logFile (if it exists). If the log file is malformed, logs a warning.

Equations

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

def Lake.cacheBuildLog (logFile : Lake.FilePath) (build : Lake.JobM PUnit) : Lake.JobM PUnit

Saves the log produce by build as JSON to logFile.

Equations

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

def Lake.buildFileUnlessUpToDate (file : Lake.FilePath) (depTrace : Lake.BuildTrace) (build : Lake.JobM PUnit) : Lake.JobM Lake.BuildTrace

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 cache in foo.c.hash and the log cache in foo.c.log.json.

Equations

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

@[inline]

def Lake.buildFileAfterDep {α : Type u_1} (file : Lake.FilePath) (dep : Lake.BuildJob α) (build : α → Lake.JobM PUnit) (extraDepTrace : optParam (Lake.JobM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build file using build after dep completes if the dependency's trace (and/or extraDepTrace) has changed.

Equations

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

@[inline]

def Lake.buildFileAfterDepList {α : Type} (file : Lake.FilePath) (deps : List (Lake.BuildJob α)) (build : List α → Lake.JobM PUnit) (extraDepTrace : optParam (Lake.JobM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build file using build after deps have built if any of their traces change.

Equations

• Lake.buildFileAfterDepList file deps build extraDepTrace = do let __do_lift ← liftM (Lake.BuildJob.collectList deps) Lake.buildFileAfterDep file __do_lift build extraDepTrace

@[inline]

def Lake.buildFileAfterDepArray {α : Type} (file : Lake.FilePath) (deps : Array (Lake.BuildJob α)) (build : Array α → Lake.JobM PUnit) (extraDepTrace : optParam (Lake.JobM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build file using build after deps have built if any of their traces change.

Equations

• Lake.buildFileAfterDepArray file deps build extraDepTrace = do let __do_lift ← liftM (Lake.BuildJob.collectArray deps) Lake.buildFileAfterDep file __do_lift build extraDepTrace

Common Builds

def Lake.inputFile (path : Lake.FilePath) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

A build job for file that is expected to already exist (e.g., a source file).

Equations

• Lake.inputFile path = Lake.Job.async ((fun (x : Lake.BuildTrace) => (path, x)) <$> Lake.computeTrace path)

@[inline]

def Lake.buildO (oFile : Lake.FilePath) (srcJob : Lake.BuildJob Lake.FilePath) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) (compiler : optParam Lake.FilePath { toString := "cc" }) (extraDepTrace : optParam (Lake.JobM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) : Lake.SpawnM (Lake.BuildJob Lake.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 BuildJob before building.

Equations

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

@[inline]

def Lake.buildLeanO (oFile : Lake.FilePath) (srcJob : Lake.BuildJob Lake.FilePath) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

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.

def Lake.buildStaticLib (libFile : Lake.FilePath) (oFileJobs : Array (Lake.BuildJob Lake.FilePath)) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

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.

def Lake.buildLeanSharedLib (libFile : Lake.FilePath) (linkJobs : Array (Lake.BuildJob Lake.FilePath)) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build a shared library by linking the results of linkJobs using leanc.

Equations

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

def Lake.buildLeanExe (exeFile : Lake.FilePath) (linkJobs : Array (Lake.BuildJob Lake.FilePath)) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build an executable by linking the results of linkJobs using leanc.

Equations

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

def Lake.buildLeanSharedLibOfStatic (staticLibJob : Lake.BuildJob Lake.FilePath) (weakArgs : optParam (Array String) #[]) (traceArgs : optParam (Array String) #[]) : Lake.SpawnM (Lake.BuildJob Lake.FilePath)

Build a shared library from a static library using leanc.

Equations

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

def Lake.computeDynlibOfShared (sharedLibTarget : Lake.BuildJob Lake.FilePath) : Lake.SpawnM (Lake.BuildJob Lake.Dynlib)

Construct a Dynlib object for a shared library target.

Equations

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