max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lake cache (& remote cache support) (#10188)

Browse source 
This PR adds support for remote artifact caches (e.g., Reservoir) to
Lake. As part of this support, a new suite of `lake cache` CLI commands
has been introduced to help manage Lake's cache. Also, the existing
local cache support has been overhauled for better interplay with the
new remote support.

**Cache CLI**

Artifacts are uploaded to a remote cache via `lake cache put`. This
command takes a JSON Lines input-to-outputs file which describes the
output artifacts for a build (indexed by its input hash). This file can
be produced by a run of `lake build` with the new `-o` option. Lake will
write the input-to-outputs mappings of thee root package artifacts
traversed by the build to the file specified via `-o`. This file can
then be passed to `lake cache put` to upload both it and the built
artifacts from the local cache to the remote cache.

The remote cache service can be customized using the following
environment variables:

* `LAKE_CACHE_KEY`: This is the authorization key for the remote cache.
Lake uploads artifacts via `curl` using the AWS Signature Version 4
protocol, so this should be the S3 `<key>:<secret>` pair expected by
`curl`.

* `LAKE_CACHE_ARTIFACT_ENDPOINT`: This is the base URL to upload (or
download) artifacts to a given remote cache. Artifacts will be stored at
`<endpoint>/<scope/<content-hash>.art`.

* `LAKE_CACHE_REVISION_ENDPOINT`: This is the base URL to upload (or
download) input-to-output mappings to a given remote cache. Mappings are
indexed by the Git revision of the package, and are stored at
`<endpoint>/<scope/<rev>.jsonl`.

The `<scope>` is provided through the `--scope` option to `lake cache
put`. This option is used to prevent one package from overwriting the
artifacts/mappings of another. Lake artifact hashes and Git revisions
hashes are not cryptographically secure, so it is not safe for a service
to store untrusted files across packages in a single flat store.

Once artifacts are available in a remote cache, the `lake cache get`
command can be used to retrieve them. By default, it will fetch
artifacts for the root package's dependencies from Reservoir using its
API. But, like `cache put`, it can be configured to use a custom
endpoint with the above environment variables and an explicit `--scope`.
When so configured, `cache get` will instead download artifacts for the
root package. Lake only downloads artifacts for a single package in this
case, because it cannot deduce the necessary package scopes without
Reservoir.

**Significant local cache changes**

* Lake now always has a cache directory. If Lake cannot find a good
candidate directory on the system for the cache, it will instead store
the cache at `.lake/cache` within the workspace.

* If the local cache is disabled, Lake will not save built artifacts to
the cache. However, Lake will, nonetheless, always attempt to lookup
build artifacts in the cache. If found, the cached artifact will be
copied to the the build location ("restored").

* Input-to-outputs mappings in the local cache are no longer stored in a
single file for a package, but rather in individual files per input (in
the `outputs` subdirectory of the cache).

* Outputs in a trace file, outputs file, or mappings file are now an
`ArtifactDescr`, which is currently composed of both the content hash
and the file extension.

* Trace files now contain a date-based `schemaVersion` to help make
version to version migration easier. Hashes in JSON and in artifacts
names now use a 16-digit hexadecimal encoding (instead of a variable
decimal encoding).

* `buildArtifactUnlessUpToDate` now returns an `Artifact` instead of a
`FilePath`.

**NOTE:** The Lake local cache is still disabled by default. This means
that built artifacts, by default, will not be placed in the cache
directory, and thus will not be available for `lake cache put` to
upload. Users must first explicitly enable the cache by either setting
the `LAKE_ARTIFACT_CACHE` environment variable to a truthy value or by
setting the `enableArtifactCache` package configuration option to
`true`.
This commit is contained in:
Mac Malone 2025-09-25 21:13:43 -04:00 • committed by GitHub
parent 2231d9b488
commit 28fb4bb1b2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
42 changed files with 1621 additions and 506 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

317
src/lake/Lake/Build/Common.lean
View file

@ -9,8 +9,8 @@ prelude
public import Lean.Data.Json
public import Lake.Build.Job.Monad
public import Lake.Config.Monad
public import Lake.Util.JsonObject
import Lake.Util.IO
import Lake.Util.JsonObject
import Lake.Build.Target.Fetch
public import Lake.Build.Actions
@ -27,8 +27,6 @@ namespace Lake
public instance : MonadWorkspace JobM := inferInstance
public scoped instance : ToJson PUnit := ⟨fun _ => Json.null⟩
open System.Platform in
/--
Build trace for the host platform.
@ -65,22 +63,24 @@ public structure BuildMetadata where
log : Log
/-- A trace file that was created from fetching an artifact from the cache. -/
synthetic : Bool
deriving ToJson
public protected def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
let obj ← JsonObject.fromJson? json
let depHash ← obj.get "depHash"
let inputs ← obj.getD "inputs" {}
let outputs? ← obj.getD "outputs" none
let log ← obj.getD "log" {}
let synthetic ← obj.getD "synthetic" false
return {depHash, inputs, outputs?, log, synthetic}
/-- The current version of the trace file format. -/
def BuildMetadata.schemaVersion : String := "2025-09-10"
public instance : FromJson BuildMetadata := ⟨BuildMetadata.fromJson?⟩
public protected def BuildMetadata.toJson (self : BuildMetadata) : Json :=
({} : JsonObject)
|>.insert "schemaVersion" schemaVersion
|>.insert "depHash" self.depHash
|>.insert "inputs" self.inputs
|>.insert "outputs" self.outputs?
|>.insert "log" self.log
|>.insert "synthetic" self.synthetic
public instance : ToJson BuildMetadata := ⟨BuildMetadata.toJson⟩
/--
Construct build metadata from a trace stub.
That is, the old version of the trace file format that just contained a hash.
That is, the very old version of the trace file format that just contained a hash.
-/
public def BuildMetadata.ofStub (hash : Hash) : BuildMetadata :=
{depHash := hash, inputs := #[], outputs? := none, log := {}, synthetic := false}
@ -88,12 +88,44 @@ public def BuildMetadata.ofStub (hash : Hash) : BuildMetadata :=
@[deprecated ofStub (since := "2025-06-28")]
public abbrev BuildMetadata.ofHash := @ofStub
public def BuildMetadata.fromJsonObject? (obj : JsonObject) : Except String BuildMetadata := do
let depHash ←
if obj.getJson? "schemaVersion" |>.isNone then
Hash.ofDecimal? (← obj.get "depHash") |>.getDM do
error "invalid trace: expected string 'depHash' of decimal digits"
else
obj.get "depHash"
let inputs ← obj.getD "inputs" {}
let outputs? ← obj.getD "outputs" none
let log ← obj.getD "log" {}
let synthetic ← obj.getD "synthetic" false
return {depHash, inputs, outputs?, log, synthetic}
public protected def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
match json with
| .num n =>
match Hash.ofJsonNumber? n with
| .ok hash =>
return .ofStub hash
| .error reason =>
error s!"invalid trace stub: {reason}"
| .obj (o : JsonObject) =>
match BuildMetadata.fromJsonObject? o with
| .ok data =>
return data
| .error e =>
if let some (.str ver) := o.getJson? "schemaVersion" then
if ver == BuildMetadata.schemaVersion then
error s!"invalid trace: {e}"
error s!"unknown trace format: {e}"
| _ =>
error s!"unknown trace format: expected JSON number or object"
public instance : FromJson BuildMetadata := ⟨BuildMetadata.fromJson?⟩
/-- Parse build metadata from a trace file's contents. -/
public def BuildMetadata.parse (contents : String) : Except String BuildMetadata :=
if let some hash := Hash.ofString? contents.trim then
return .ofStub hash
else
Json.parse contents >>= fromJson?
public def BuildMetadata.parse (contents : String) : Except String BuildMetadata := do
Json.parse contents >>= fromJson?
/-- Construct build metadata from a cached input-to-output mapping. -/
public def BuildMetadata.ofFetch (inputHash : Hash) (outputs : Json) : BuildMetadata :=
@ -135,11 +167,16 @@ Logs if the read failed or the contents where invalid.
public def readTraceFile (path : FilePath) : LogIO SavedTrace := do
match (← IO.FS.readFile path |>.toBaseIO) with
| .ok contents =>
match BuildMetadata.parse contents with
| .ok data => return .ok data
| .error e => logVerbose s!"{path}: invalid trace file: {e}"; return .invalid
| .error (.noFileOrDirectory ..) => return .missing
| .error e => logWarning s!"{path}: read failed: {e}"; return .invalid
match Json.parse contents >>= BuildMetadata.fromJson? with
| .ok data =>
return .ok data
| .error e =>
logWarning s!"{path}: {e}"
return .invalid
| .error (.noFileOrDirectory ..) =>
return .missing
| .error e =>
error s!"{path}: read failed: {e}"
/--
Tries to read data from a trace file. On failure, returns `none`.
@ -183,7 +220,17 @@ as the point of comparison instead.
else
return false
/-- Checks whether `info` is up-to-date, and replays the log of the trace if available. -/
/-- Returns whether the hash does not match the trace's dependency hash. -/
public def SavedTrace.isDifferentFrom (hash : Hash) (self : SavedTrace) : Bool :=
match self with
| .ok data =>
hash != data.depHash
| _ =>
true
/--
Checks whether `info` is up-to-date with the trace.
If so, replays the log of the trace if available. -/
@[specialize] public def SavedTrace.replayIfUpToDate
[CheckExists ι] [GetMTime ι]
(info : ι) (depTrace : BuildTrace) (savedTrace : SavedTrace)
@ -219,29 +266,38 @@ public def SavedTrace.replayOrFetch
updateAction .fetch
writeFetchTrace traceFile inputHash outputs
/-- **For internal use only.** -/
public class ToOutputJson (α : Type u) where
toOutputJson (arts : α) : Json
public instance : ToOutputJson PUnit := ⟨fun _ => Json.null⟩
public instance : ToOutputJson Artifact := ⟨(toJson ·.descr)⟩
open ToOutputJson in
/--
Runs `build` as a build action of kind `action`.
The build's input trace (`depTrace`), output hashes (the result of `build`),
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`).
-/
@[specialize] public def buildAction
[ToJson α] (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM α)
[ToOutputJson α]
(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM α)
(action : JobAction := .build)
: JobM α := do
if (← getNoBuild) then
updateAction .build
error "target is out-of-date and needs to be rebuilt"
error s!"target is out-of-date and needs to be rebuilt"
else
updateAction action
let startTime ← IO.monoMsNow
try
let iniPos ← getLogPos
let outputs ← build -- fatal errors will abort here
let a ← build -- fatal errors will abort here
let log := (← getLog).takeFrom iniPos
writeBuildTrace traceFile depTrace outputs log
return outputs
writeBuildTrace traceFile depTrace (toOutputJson a) log
return a
finally
let endTime ← IO.monoMsNow
let elapsed := endTime - startTime
@ -306,11 +362,7 @@ public def cacheFileHash (file : FilePath) (text := false) : IO Unit := do
/-- Remove the cached hash of a file (its `.hash` file) if it exists. -/
public def clearFileHash (file : FilePath) : IO Unit := do
try
IO.FS.removeFile <| file.toString ++ ".hash"
catch
| .noFileOrDirectory .. => pure ()
| e => throw e
removeFileIfExists <| file.toString ++ ".hash"
/--
Fetches the hash of a file that may already be cached in a `.hash` file.
@ -362,8 +414,6 @@ public def buildFileUnlessUpToDate'
clearFileHash file
setTrace (← fetchFileTrace file text)
/--
Copies `file` to the Lake cache with the file extension `ext`, and
saves its hash in its `.hash` file.
@ -379,16 +429,18 @@ public def Cache.saveArtifact
let contents ← IO.FS.readFile file
let normalized := contents.crlfToLf
let hash := Hash.ofString normalized
let path := cache.artifactPath hash ext
let descr := artifactWithExt hash ext
let path := cache.artifactDir / descr.toFilePath
createParentDirs path
IO.FS.writeFile path normalized
writeFileHash file hash
let mtime := (← getMTime path |>.toBaseIO).toOption.getD 0
return {name := file.toString, path, mtime, hash}
return {descr, name := file.toString, path, mtime}
else
let contents ← IO.FS.readBinFile file
let hash := Hash.ofByteArray contents
let path := cache.artifactPath hash ext
let descr := artifactWithExt hash ext
let path := cache.artifactDir / descr.toFilePath
createParentDirs path
IO.FS.writeBinFile path contents
if exe then
@ -396,80 +448,81 @@ public def Cache.saveArtifact
IO.setAccessRights path ⟨r, r, r⟩ -- 777
writeFileHash file hash
let mtime := (← getMTime path |>.toBaseIO).toOption.getD 0
return {name := file.toString, path, mtime, hash}
return {descr, name := file.toString, path, mtime}
@[inline, inherit_doc Cache.saveArtifact]
public def cacheArtifact
[MonadLakeEnv m] [MonadLiftT IO m] [Monad m]
[MonadWorkspace m] [MonadLiftT IO m] [Monad m]
(file : FilePath) (ext := "art") (text := false) (exe := false)
: m Artifact := do (← getLakeCache).saveArtifact file ext text exe
/--
Computes the trace of a cached artifact.
`buildFile` is where the uncached artifact would be located.
-/
public def computeArtifactTrace
(buildFile : FilePath) (art : FilePath) (contentHash : Hash)
: BaseIO BuildTrace := do
let mtime := (← getMTime art |>.toBaseIO).toOption.getD 0
return {caption := buildFile.toString, mtime, hash := contentHash}
/-- **For internal use only.** -/
public class ResolveOutputs (m : Type v → Type w) (α : Type v) where
resolveOutputs? (outputs : Json) : m (Option α)
public class ResolveArtifacts (m : Type v → Type w) (α : Type u) (β : outParam $ Type v) where
resolveArtifacts? (contentHashes : α) : m (Option β)
open ResolveArtifacts in
open ResolveOutputs in
/--
Retrieve artifacts from the Lake cache using the the content hashes stored as `α`
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.**
-/
@[specialize] public def resolveArtifactsUsing?
(α : Type u) [FromJson α] [ResolveArtifacts JobM α β]
(inputHash : Hash) (traceFile : FilePath) (savedTrace : SavedTrace) (cache : CacheRef)
: JobM (Option β) := do
if let some out ← cache.get? inputHash then
if let .ok (hashes : α) := fromJson? out then
if let some arts ← resolveArtifacts? hashes then
savedTrace.replayOrFetch traceFile inputHash out
return some arts
else
logWarning s!"\
input '{inputHash.toString.take 7}' found in package artifact cache, \
but some output(s) were not"
return none
@[specialize] public nonrec def getArtifacts?
[ResolveOutputs JobM α]
(inputHash : Hash) (traceFile : FilePath) (savedTrace : SavedTrace)
(cache : Cache) (pkg : Package)
: JobM (Option α) := do
let updateCache ← pkg.isArtifactCacheEnabled
if let some out ← cache.readOutputs? pkg.cacheScope inputHash then
if let some arts ← resolveOutputs? out then
savedTrace.replayOrFetch traceFile inputHash out
return some arts
else
logWarning s!"\
input '{inputHash.toString.take 7}' found in package artifact cache, \
but output(s) were in an unexpected format"
but some output(s) were not"
if let .ok data := savedTrace then
if data.depHash == inputHash then
if let some out := data.outputs? then
if let .ok (hashes : α) := fromJson? out then
if let some arts ← resolveArtifacts? hashes then
cache.insert inputHash out
savedTrace.replayOrFetch traceFile inputHash out
return some arts
if let some arts ← resolveOutputs? out then
if updateCache then
cache.writeOutputs pkg.cacheScope inputHash out
savedTrace.replayOrFetch traceFile inputHash out
return some arts
return none
/-- The content hash of an artifact which is stored with extension `ext` in the Lake cache. -/
public structure FileOutputHash (ext : String) where
hash : Hash
@[inline] def resolveArtifactsCore?
[FromJson α] [MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m]
(f : α → m (Option β)) (out : Json)
: m (Option β) := do
match fromJson? out with
| .ok (a : α) => f a
| .error e => error e
public instance : ToJson (FileOutputHash ext) := ⟨(toJson ·.hash)⟩
public instance : FromJson (FileOutputHash ext) := ⟨(.mk <$> fromJson? ·)⟩
@[inline] def resolveArtifact
[MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m] (output : Json)
: m (Option Artifact) := resolveArtifactsCore? (do (← getLakeCache).getArtifact? ·) output
public instance
[MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m]
: ResolveArtifacts m (FileOutputHash ext) Artifact := ⟨(getArtifact? ·.hash ext)⟩
@[inline] def resolveOutput?
[MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m] (output : Json)
: m (Option Artifact) := do
match fromJson? output with
| .ok descr => getArtifact? descr
| .error e => error s!"unexpected output: {e}"
instance
[MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m]
: ResolveOutputs m Artifact := ⟨resolveOutput?⟩
/--
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.
-/
public def fetchLocalArtifact (path : FilePath) (text := false) : JobM Artifact := do
public def computeArtifact (path : FilePath) (ext := "art") (text := false) : JobM Artifact := do
let hash ← fetchFileHash path text
let mtime := (← getMTime path |>.toBaseIO).toOption.getD 0
return {name := path.toString, path, mtime, hash}
return {descr := artifactWithExt hash ext, name := path.toString, path, mtime}
/--
Uses the current job's trace to search Lake's local artifact cache for an artifact
@ -486,45 +539,70 @@ than the path to the cached artifact.
public def buildArtifactUnlessUpToDate
(file : FilePath) (build : JobM PUnit)
(text := false) (ext := "art") (restore := false) (exe := false)
: JobM FilePath := do
: JobM Artifact := do
let depTrace ← getTrace
let traceFile := FilePath.mk <| file.toString ++ ".trace"
let savedTrace ← readTraceFile traceFile
if let some pkg ← getCurrPackage? then
let cache ← getLakeCache
let inputHash := depTrace.hash
if let some cache := pkg.cacheRef? then
let art? ← resolveArtifactsUsing? (FileOutputHash ext) inputHash traceFile savedTrace cache
if let some art := art? then
if restore && !(← file.pathExists) then
let fetchArt? restore := do
let some (art : Artifact) ← getArtifacts? inputHash traceFile savedTrace cache pkg
| return none
if restore then
if savedTrace.isDifferentFrom inputHash || !(← file.pathExists) then
logVerbose s!"restored artifact from cache to: {file}"
createParentDirs file
copyFile art.path file
if exe then
let r := ⟨true, true, true⟩
IO.setAccessRights file ⟨r, r, r⟩ -- 777
writeFileHash file art.hash
return some (art.useLocalFile file)
else
return some art
if (← pkg.isArtifactCacheEnabled) then
if let some art ← fetchArt? restore then
setTrace art.trace
return if restore then file else art.path
unless (← savedTrace.replayIfUpToDate file depTrace) do
discard <| doBuild depTrace traceFile
let art ← cacheArtifact file ext text exe
cache.insert inputHash art.hash
if let some outputsRef := pkg.outputsRef? then
outputsRef.insert inputHash art.hash
return art
else
unless (← savedTrace.replayIfUpToDate file depTrace) do
discard <| doBuild depTrace traceFile
let art ← cacheArtifact file ext text exe
cache.writeOutputs pkg.cacheScope inputHash art.descr
if let some outputsRef := pkg.outputsRef? then
outputsRef.insert inputHash art.descr
setTrace art.trace
return if restore then art.useLocalFile file else art
else
let art ← id do
if (← savedTrace.replayIfUpToDate file depTrace) then
computeArtifact file ext
else if let some art ← fetchArt? (restore := true) then
return art
else
doBuild depTrace traceFile
if let some outputsRef := pkg.outputsRef? then
outputsRef.insert inputHash art.descr
setTrace art.trace
return if restore then file else art.path
if (← savedTrace.replayIfUpToDate file depTrace) then
let contentHash ← fetchFileHash file text
setTrace (← computeArtifactTrace file file contentHash)
return file
return art
else
let contentHash ← doBuild depTrace traceFile
writeFileHash file contentHash
setTrace (← computeArtifactTrace file file contentHash)
return file
let art ←
if (← savedTrace.replayIfUpToDate file depTrace) then
computeArtifact file ext text
else
doBuild depTrace traceFile
setTrace art.trace
return art
where
doBuild depTrace traceFile :=
inline <| buildAction depTrace traceFile do
build
clearFileHash file
computeFileHash file text
removeFileIfExists traceFile
computeArtifact file ext
/--
Build `file` using `build` after `dep` completes if the dependency's
@ -538,7 +616,8 @@ If `text := true`, `file` is handled as a text file rather than a binary file.
: SpawnM (Job FilePath) :=
dep.mapM fun depInfo => do
addTrace (← extraDepTrace)
buildArtifactUnlessUpToDate file (build depInfo) text
let art ← buildArtifactUnlessUpToDate file (build depInfo) text
return art.path
/-! ## Common Builds -/
@ -591,7 +670,7 @@ public def inputDir
let ps := ps.qsort (toString · < toString ·)
return ps
job.bindM fun ps =>
Job.collectArray <$> ps.mapM (inputFile · text)
Job.collectArray (traceCaption := path.toString) <$> ps.mapM (inputFile · text)
/--
Build an object file from a source file job using `compiler`. The invocation is:
@ -617,8 +696,9 @@ which will be computed in the resulting `Job` before building.
addPlatformTrace -- object files are platform-dependent artifacts
addPureTrace traceArgs "traceArgs"
addTrace (← extraDepTrace)
buildArtifactUnlessUpToDate oFile (ext := "o") do
let art ← buildArtifactUnlessUpToDate oFile (ext := "o") do
compileO oFile srcFile (weakArgs ++ traceArgs) compiler
return art.path
/--
Build an object file from a source fie job (i.e, a `lean -c` output)
@ -633,19 +713,21 @@ public def buildLeanO
addLeanTrace
addPureTrace traceArgs "traceArgs"
addPlatformTrace -- object files are platform-dependent artifacts
buildArtifactUnlessUpToDate oFile (ext := "o") do
let art ← buildArtifactUnlessUpToDate oFile (ext := "o") do
let lean ← getLeanInstall
let includeDir := leanIncludeDir?.getD lean.includeDir
let args := #["-I", includeDir.toString] ++ lean.ccFlags ++ weakArgs ++ traceArgs
compileO oFile srcFile args lean.cc
return art.path
/-- Build a static library from object file jobs using the Lean toolchain's `ar`. -/
public def buildStaticLib
(libFile : FilePath) (oFileJobs : Array (Job FilePath)) (thin := false)
: SpawnM (Job FilePath) :=
(Job.collectArray oFileJobs "objs").mapM fun oFiles => do
buildArtifactUnlessUpToDate libFile (ext := "a") (restore := true) do
let art ← buildArtifactUnlessUpToDate libFile (ext := "a") (restore := true) do
compileStaticLib libFile oFiles (← getLeanAr) thin
return art.path
private def mkLinkObjArgs
(objs : Array FilePath) (libs : Array Dynlib) : Array String
@ -700,11 +782,11 @@ public def buildSharedLib
addTrace (← extraDepTrace)
-- Lean plugins are required to have a specific name
-- and thus need to copied from the cache with that name
let libFile ← buildArtifactUnlessUpToDate libFile (ext := sharedLibExt) (restore := true) do
let art ← buildArtifactUnlessUpToDate libFile (ext := sharedLibExt) (restore := true) do
let libs ← if linkDeps then mkLinkOrder libs else pure #[]
let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs
compileSharedLib libFile args linker
return {name := libName, path := libFile, deps := libs, plugin}
return {name := libName, path := art.path, deps := libs, plugin}
/--
Build a shared library by linking the results of `linkJobs`
@ -723,13 +805,13 @@ public def buildLeanSharedLib
addPlatformTrace -- shared libraries are platform-dependent artifacts
-- Lean plugins are required to have a specific name
-- and thus need to copied from the cache with that name
let libFile ← buildArtifactUnlessUpToDate libFile (ext := sharedLibExt) (restore := true) do
let art ← buildArtifactUnlessUpToDate libFile (ext := sharedLibExt) (restore := true) do
let lean ← getLeanInstall
let libs ← if linkDeps then mkLinkOrder libs else pure #[]
let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
#["-L", lean.leanLibDir.toString] ++ lean.ccLinkSharedFlags
compileSharedLib libFile args lean.cc
return {name := libName, path := libFile, deps := libs, plugin}
return {name := libName, path := art.path, deps := libs, plugin}
/--
Build an executable by linking the results of `linkJobs`
@ -745,9 +827,10 @@ public def buildLeanExe
addLeanTrace
addPureTrace traceArgs "traceArgs"
addPlatformTrace -- executables are platform-dependent artifacts
buildArtifactUnlessUpToDate exeFile (ext := FilePath.exeExtension) (exe := true) (restore := true) do
let art ← buildArtifactUnlessUpToDate exeFile (ext := FilePath.exeExtension) (exe := true) (restore := true) do
let lean ← getLeanInstall
let libs ← mkLinkOrder libs
let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
#["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
compileExe exeFile args lean.cc
return art.path

2
src/lake/Lake/Build/Context.lean
View file

@ -42,6 +42,8 @@ public structure BuildConfig where
ansiMode : AnsiMode := .auto
/-- Whether to print a message when the build finishes successfully (if not quiet). -/
showSuccess : Bool := false
/-- File to save input-to-output mappings from the build of the worksoace's root -/
outputsFile? : Option FilePath := none
/--
Whether the build should show progress information.

161
src/lake/Lake/Build/Module.lean
View file

@ -511,6 +511,16 @@ public def Module.setupFacetConfig : ModuleFacetConfig setupFacet :=
public def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
mkFacetJobConfig fun mod => (·.toOpaque) <$> mod.setup.fetch
/-- Remove all existing artifacts produced by the Lean build of the module. -/
public def Module.clearOutputArtifacts (mod : Module) : IO PUnit := do
removeFileIfExists mod.oleanFile
removeFileIfExists mod.oleanServerFile
removeFileIfExists mod.oleanPrivateFile
removeFileIfExists mod.ileanFile
removeFileIfExists mod.irFile
removeFileIfExists mod.cFile
removeFileIfExists mod.bcFile
/-- Remove any cached file hashes of the module build outputs (in `.hash` files). -/
public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
clearFileHash mod.oleanFile
@ -535,31 +545,34 @@ public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
if Lean.Internal.hasLLVMBackend () then
cacheFileHash mod.bcFile
private def ModuleOutputHashes.getArtifactsFrom?
(cache : Cache) (hashes : ModuleOutputHashes)
private def ModuleOutputDescrs.getArtifactsFrom?
(cache : Cache) (descrs : ModuleOutputDescrs)
: BaseIO (Option ModuleOutputArtifacts) := OptionT.run do
let mut arts : ModuleOutputArtifacts := {
olean := ← cache.getArtifact? hashes.olean "olean"
ilean := ← cache.getArtifact? hashes.ilean "ilean"
c :=← cache.getArtifact? hashes.c "c"
olean := ← cache.getArtifact? descrs.olean
ilean := ← cache.getArtifact? descrs.ilean
c :=← cache.getArtifact? descrs.c
}
if let some hash := hashes.oleanServer? then
arts := {arts with oleanServer? := some (← cache.getArtifact? hash "olean.server")}
if let some hash := hashes.oleanPrivate? then
arts := {arts with oleanPrivate? := some (← cache.getArtifact? hash "olean.private")}
if let some hash := hashes.ir? then
arts := {arts with ir? := some (← cache.getArtifact? hash "ir")}
if let some hash := descrs.oleanServer? then
arts := {arts with oleanServer? := some (← cache.getArtifact? hash)}
if let some hash := descrs.oleanPrivate? then
arts := {arts with oleanPrivate? := some (← cache.getArtifact? hash)}
if let some hash := descrs.ir? then
arts := {arts with ir? := some (← cache.getArtifact? hash)}
if Lean.Internal.hasLLVMBackend () then
arts := {arts with bc? := some (← cache.getArtifact? (← hashes.bc?) "bc")}
arts := {arts with bc? := some (← cache.getArtifact? (← descrs.bc?))}
return arts
@[inline] private def ModuleOutputHashes.getArtifacts?
[MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m] (hashes : ModuleOutputHashes)
: m (Option ModuleOutputArtifacts) := do hashes.getArtifactsFrom? (← getLakeCache)
@[inline] def resolveModuleOutputs?
[MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m] (outputs : Json)
: m (Option ModuleOutputArtifacts) := do
match fromJson? outputs with
| .ok (descrs : ModuleOutputDescrs) => descrs.getArtifactsFrom? (← getLakeCache)
| .error e => error e
private instance
[MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m]
: ResolveArtifacts m ModuleOutputHashes ModuleOutputArtifacts := ⟨ ModuleOutputHashes.getArtifacts?⟩
instance
[MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m]
: ResolveOutputs m ModuleOutputArtifacts := ⟨resolveModuleOutputs?⟩
/-- Save module build artifacts to the local Lake cache. Requires the artifact cache to be enabled. -/
private def Module.cacheOutputArtifacts (mod : Module) : JobM ModuleOutputArtifacts := do
@ -578,22 +591,38 @@ where
@[inline] cacheIfExists? art ext := do
cacheIf? (← art.pathExists) art ext
private def restoreModuleArtifact (file : FilePath) (art : Artifact) : JobM Artifact := do
unless (← file.pathExists) do
logVerbose s!"restored artifact from cache to: {file}"
createParentDirs file
copyFile art.path file
writeFileHash file art.hash
return art.useLocalFile file
/--
Some module build artifacts must be located in the build directory (e.g., ILeans).
This copies the required artifacts from the local Lake cache to the build directory and
updates the data structure with the new paths.
-/
private def Module.restoreArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
private def Module.restoreNeededArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
return {cached with
ilean := ← restore mod.ileanFile cached.ilean
ilean := ← restoreModuleArtifact mod.ileanFile cached.ilean
}
private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
return {cached with
olean := ← restoreModuleArtifact mod.oleanFile cached.olean
oleanServer? := ← restoreSome mod.oleanServerFile cached.oleanServer?
oleanPrivate? := ← restoreSome mod.oleanPrivateFile cached.oleanPrivate?
ilean := ← restoreModuleArtifact mod.ileanFile cached.ilean
ir? := ← restoreSome mod.oleanFile cached.ir?
c := ← restoreModuleArtifact mod.cFile cached.c
bc? := ← restoreSome mod.oleanFile cached.bc?
}
where
restore file art := do
unless (← file.pathExists) do
logVerbose s!"restored artifact from cache to: {file}"
copyFile art.path file
writeFileHash file art.hash
return art.useLocalFile file
@[inline] restoreSome file art? :=
art?.mapM (restoreModuleArtifact file)
private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : Bool) : ModuleArtifacts where
lean? := srcFile
@ -605,31 +634,27 @@ private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : B
c? := mod.cFile
bc? := if Lean.Internal.hasLLVMBackend () then some mod.bcFile else none
private def Module.computeOutputHashes (mod : Module) (isModule : Bool) : FetchM ModuleOutputHashes :=
private def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
return {
olean := ← computeFileHash mod.oleanFile
oleanServer? := ← if isModule then some <$> computeFileHash mod.oleanServerFile else pure none
oleanPrivate? := ← if isModule then some <$> computeFileHash mod.oleanPrivateFile else pure none
ilean := ← computeFileHash mod.ileanFile
ir? := ← if isModule then some <$> computeFileHash mod.irFile else pure none
c := ← computeFileHash mod.cFile
bc? := ← if Lean.Internal.hasLLVMBackend () then some <$> computeFileHash mod.bcFile else pure none
olean := ← compute mod.oleanFile "olean"
oleanServer? := ← computeIf isModule mod.oleanServerFile "olean.server"
oleanPrivate? := ← computeIf isModule mod.oleanPrivateFile "olean.private"
ilean := ← compute mod.ileanFile "ilean"
ir? := ← computeIf isModule mod.irFile "ir"
c := ← compute mod.cFile "c"
bc? := ← computeIf (Lean.Internal.hasLLVMBackend ()) mod.bcFile "bc"
}
where
@[inline] compute file ext := do
computeArtifact file ext
computeIf c file ext := do
if c then return some (← compute file ext) else return none
private def Module.fetchLocalArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
return {
olean := ← fetchLocalArtifact mod.oleanFile
oleanServer? := ← if isModule then some <$> fetchLocalArtifact mod.oleanServerFile else pure none
oleanPrivate? := ← if isModule then some <$> fetchLocalArtifact mod.oleanPrivateFile else pure none
ilean := ← fetchLocalArtifact mod.ileanFile
ir? := ← if isModule then some <$> fetchLocalArtifact mod.irFile else pure none
c := ← fetchLocalArtifact mod.cFile
bc? := ← if Lean.Internal.hasLLVMBackend () then some <$> fetchLocalArtifact mod.bcFile else pure none
}
instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
private def Module.buildLean
(mod : Module) (depTrace : BuildTrace) (srcFile : FilePath) (setup : ModuleSetup)
: JobM ModuleOutputHashes := buildAction depTrace mod.traceFile do
: JobM ModuleOutputArtifacts := buildAction depTrace mod.traceFile do
let args := mod.weakLeanArgs ++ mod.leanArgs
let relSrcFile := relPathFrom mod.pkg.dir srcFile
let directImports := (← (← mod.input.fetch).await).imports
@ -639,7 +664,7 @@ private def Module.buildLean
compileLeanModule srcFile relSrcFile setup mod.setupFile arts args
(← getLeanPath) (← getLean)
mod.clearOutputHashes
mod.computeOutputHashes setup.isModule
mod.computeArtifacts setup.isModule
private def traceOptions (opts : LeanOptions) (caption := "opts") : BuildTrace :=
opts.values.foldl (init := .nil caption) fun t n v =>
@ -671,18 +696,38 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
let depTrace ← getTrace
let inputHash := depTrace.hash
let savedTrace ← readTraceFile mod.traceFile
if let some ref := mod.pkg.cacheRef? then
if let some arts ← resolveArtifactsUsing? ModuleOutputHashes inputHash mod.traceFile savedTrace ref then
return ← mod.restoreArtifacts arts
let upToDate ← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace
unless upToDate do
discard <| mod.buildLean depTrace srcFile setup
if let some ref := mod.pkg.cacheRef? then
let arts ← mod.cacheOutputArtifacts
ref.insert inputHash arts.hashes
return arts
else
mod.fetchLocalArtifacts setup.isModule
let cache ← getLakeCache
let fetchArtsFromCache? restoreAll := do
let arts? ← getArtifacts? inputHash mod.traceFile savedTrace cache mod.pkg
if let some arts := arts? then
if savedTrace.isDifferentFrom inputHash then
mod.clearOutputArtifacts
if restoreAll then
some <$> mod.restoreAllArtifacts arts
else
some <$> mod.restoreNeededArtifacts arts
else
return none
let arts ← id do
if (← mod.pkg.isArtifactCacheEnabled) then
if let some arts ← fetchArtsFromCache? false then
return arts
else
unless (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) do
discard <| mod.buildLean depTrace srcFile setup
let arts ← mod.cacheOutputArtifacts
cache.writeOutputs mod.pkg.cacheScope inputHash arts.descrs
return arts
else
if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
mod.computeArtifacts setup.isModule
else if let some arts ← fetchArtsFromCache? true then
return arts
else
mod.buildLean depTrace srcFile setup
if let some ref := mod.pkg.outputsRef? then
ref.insert inputHash arts.descrs
return arts
/-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
public def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=

70
src/lake/Lake/Build/ModuleArtifacts.lean
View file

@ -14,42 +14,42 @@ open Lean (Json ToJson FromJson)
namespace Lake
/-- The content hashes of the output artifacts of a module build. -/
public structure ModuleOutputHashes where
olean : Hash := .nil
oleanServer? : Option Hash := none
oleanPrivate? : Option Hash := none
ilean : Hash := .nil
ir? : Option Hash := none
c : Hash := .nil
bc? : Option Hash := none
/-- The descriptions of the output artifacts of a module build. -/
public structure ModuleOutputDescrs where
olean : ArtifactDescr
oleanServer? : Option ArtifactDescr := none
oleanPrivate? : Option ArtifactDescr := none
ilean : ArtifactDescr
ir? : Option ArtifactDescr := none
c : ArtifactDescr
bc? : Option ArtifactDescr := none
public def ModuleOutputHashes.oleanHashes (hashes : ModuleOutputHashes) : Array Hash := Id.run do
let mut oleanHashes := #[hashes.olean]
if let some hash := hashes.oleanServer? then
oleanHashes := oleanHashes.push hash
if let some hash := hashes.oleanPrivate? then
oleanHashes := oleanHashes.push hash
return oleanHashes
public def ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) : Array ArtifactDescr := Id.run do
let mut descrs := #[self.olean]
if let some hash := self.oleanServer? then
descrs := descrs.push hash
if let some hash := self.oleanPrivate? then
descrs := descrs.push hash
return descrs
public protected def ModuleOutputHashes.toJson (hashes : ModuleOutputHashes) : Json := Id.run do
public protected def ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Json := Id.run do
let mut obj : JsonObject := {}
obj := obj.insert "o" hashes.oleanHashes
obj := obj.insert "i" hashes.ilean
if let some ir := hashes.ir? then
obj := obj.insert "o" self.oleanParts
obj := obj.insert "i" self.ilean
if let some ir := self.ir? then
obj := obj.insert "r" ir
obj := obj.insert "c" hashes.c
if let some bc := hashes.bc? then
obj := obj.insert "c" self.c
if let some bc := self.bc? then
obj := obj.insert "b" bc
return obj
public instance : ToJson ModuleOutputHashes := ⟨ModuleOutputHashes.toJson⟩
public instance : ToJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.toJson⟩
public protected def ModuleOutputHashes.fromJson? (val : Json) : Except String ModuleOutputHashes := do
public protected def ModuleOutputDescrs.fromJson? (val : Json) : Except String ModuleOutputDescrs := do
let obj ← JsonObject.fromJson? val
let oleanHashes : Array Hash ← obj.get "o"
let oleanHashes : Array ArtifactDescr ← obj.get "o"
let some olean := oleanHashes[0]?
| throw "expected a least one 'o' (OLean) hash"
| throw "expected a least one 'o' (.olean) hash"
return {
olean := olean
oleanServer? := oleanHashes[1]?
@ -60,7 +60,7 @@ public protected def ModuleOutputHashes.fromJson? (val : Json) : Except String M
bc? := ← obj.get? "b"
}
public instance : FromJson ModuleOutputHashes := ⟨ModuleOutputHashes.fromJson?⟩
public instance : FromJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.fromJson?⟩
/-- The output artifacts of a module build. -/
public structure ModuleOutputArtifacts where
@ -73,11 +73,11 @@ public structure ModuleOutputArtifacts where
bc? : Option Artifact := none
/-- Content hashes of the artifacts. -/
public def ModuleOutputArtifacts.hashes (arts : ModuleOutputArtifacts) : ModuleOutputHashes where
olean := arts.olean.hash
oleanServer? := arts.oleanServer?.map (·.hash)
oleanPrivate? := arts.oleanPrivate?.map (·.hash)
ilean := arts.ilean.hash
ir? := arts.ir?.map (·.hash)
c := arts.c.hash
bc? := arts.bc?.map (·.hash)
public def ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleOutputDescrs where
olean := arts.olean.descr
oleanServer? := arts.oleanServer?.map (·.descr)
oleanPrivate? := arts.oleanPrivate?.map (·.descr)
ilean := arts.ilean.descr
ir? := arts.ir?.map (·.descr)
c := arts.c.descr
bc? := arts.bc?.map (·.descr)

1
src/lake/Lake/Build/Package.lean
View file

@ -11,6 +11,7 @@ public import Lake.Config.FacetConfig
public import Lake.Build.Job.Monad
public import Lake.Build.Infos
import Lake.Util.Git
import Lake.Util.Url
import Lake.Util.Proc
import Lake.Build.Actions
import Lake.Build.Common

37
src/lake/Lake/Build/Run.lean
View file

@ -222,14 +222,6 @@ public def monitorJobs
didBuild := s.didBuild
}
/-- Save input mappings to the local Lake artifact cache (if enabled). -/
public def Workspace.saveInputs (ws : Workspace) : LogIO Unit := do
unless ws.lakeCache.isDisabled do
ws.packages.forM fun pkg => do
if let some ref := pkg.cacheRef? then
let inputsFile := pkg.inputsFileIn ws.lakeCache
(← ref.get).save inputsFile
/-- Exit code to return if `--no-build` is set and a build is required. -/
public def noBuildCode : ExitCode := 3
@ -260,16 +252,25 @@ public def Workspace.runFetchM
let showTime := isVerbose || !useAnsi
let {failures, numJobs, didBuild} ← monitorJobs #[job] ctx.registeredJobs
out failLv outLv minAction showOptional useAnsi showProgress showTime
-- Save input mappings to cache
match (← ws.saveInputs.run {}) with
| .ok _ log =>
if !log.isEmpty && isVerbose then
print! out "There were issues saving input mappings to the local artifact cache:\n"
log.replay (logger := .stream out outLv useAnsi)
| .error _ log =>
print! out "Failed to save input mappings to the local artifact cache.\n"
if isVerbose then
log.replay (logger := .stream out outLv useAnsi)
-- Save input-to-output mappings
if let some outputsFile := cfg.outputsFile? then
let logger := .stream out outLv useAnsi
unless ws.isRootArtifactCacheEnabled do
logger.logEntry <| .warning s!"{ws.root.name}: \
the artifact cache is not enabled for this package, so the artifacts described \
by the mappings produced by `-o` will not necessarily be available in the cache."
if let some ref := ws.root.outputsRef? then
match (← (← ref.get).writeFile outputsFile {}) with
| .ok _ log =>
if !log.isEmpty && isVerbose then
print! out "There were issues saving input-to-output mappings from the build:\n"
log.replay (logger := logger)
| .error _ log =>
print! out "Failed to save input-to-output mappings from the build.\n"
if isVerbose then
log.replay (logger := logger)
else
print! out "Workspace missing input-to-output mappings from build. (This is likely a bug in Lake.)\n"
-- Report
let isNoBuild := cfg.noBuild
if failures.isEmpty then

69
src/lake/Lake/Build/Trace.lean
View file

@ -8,6 +8,8 @@ module
prelude
public import Init.System.IO
public import Lean.Data.Json
import Init.Data.Nat.Fold
import Lake.Util.String
import Lake.Util.IO
/-! # Lake Traces
@ -101,27 +103,60 @@ namespace Hash
public instance : Hashable Hash := ⟨Hash.val⟩
@[inline] public def ofNat (n : Nat) :=
mk n.toUInt64
public def ofString? (s : String) : Option Hash :=
(inline s.toNat?).map ofNat
public def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
public def nil : Hash :=
mk <| 1723 -- same as Name.anonymous
public instance : NilTrace Hash := ⟨nil⟩
@[inline] public def ofNat (n : Nat) :=
mk n.toUInt64
/-- Parse a hash from a JSON number. -/
public def ofJsonNumber? (n : JsonNumber) : Except String Hash :=
if n.exponent = 0 && 0 ≤ n.mantissa then
if h : n.mantissa.toNat < UInt64.size then
return ⟨.ofNatLT n.mantissa.toNat h⟩
else
throw "number too big"
else
throw "number is not a natural"
/-- Parse a hash from a string of hexadecimal digits. Does no validation. -/
public def ofHex (s : String) : Hash :=
mk <| s.utf8ByteSize.fold (init := 0) fun i h n =>
let c := s.getUtf8Byte ⟨i⟩ h
if c ≤ 57 then n*16 + (c - 48).toUInt64
else if 97 ≤ c then n*16 + (c - 87).toUInt64 -- c - 'a' + 10 = (c - 87)
else n*16 + (c - 55).toUInt64 -- c - 'A' + 10 = (c - 55)
-- sanity check
example : ofHex "0123456789" = ⟨0x0123456789⟩ ∧
ofHex "abcdeF" = ⟨0xabcdef⟩ ∧ ofHex "ABCDEF" = ⟨0xABCDEF⟩ := by native_decide
/-- Parse a hash from a 16-digit string of hexadecimal digits. -/
public def ofHex? (s : String) : Option Hash :=
if s.utf8ByteSize = 16 && isHex s then ofHex s else none
/-- Returns the hash as 16-digit lowercase hex string. -/
public def hex (self : Hash) : String :=
lpad (Nat.toDigits 16 self.val.toNat).asString '0' 16
public def ofDecimal? (s : String) : Option Hash :=
(inline s.toNat?).map ofNat
@[inline] public def ofString? (s : String) : Option Hash :=
ofHex? s
public def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
@[inline] public def mix (h1 h2 : Hash) : Hash :=
mk <| mixHash h1.val h2.val
public instance : MixTrace Hash := ⟨mix⟩
@[inline] public protected def toString (self : Hash) : String :=
toString self.val
self.hex
public instance : ToString Hash := ⟨Hash.toString⟩
@ -139,12 +174,20 @@ public instance : ToString Hash := ⟨Hash.toString⟩
mk (hash b)
@[inline] public protected def toJson (self : Hash) : Json :=
toJson self.val
toJson self.hex
public instance : ToJson Hash := ⟨Hash.toJson⟩
@[inline] public protected def fromJson? (json : Json) : Except String Hash :=
(⟨·⟩) <$> fromJson? json
public protected def fromJson? (json : Json) : Except String Hash := do
match json with
| .str s =>
unless isHex s do
throw "invalid hash: expected hexadecimal string"
unless s.utf8ByteSize = 16 do
throw "invalid hash: expected hexadecimal string of length 16"
return ofHex s
| .num n => ofJsonNumber? n |>.mapError (s!"invalid hash: {·}")
| _ => throw "invalid hash: expected string or number"
public instance : FromJson Hash := ⟨Hash.fromJson?⟩

84
src/lake/Lake/CLI/Help.lean
View file

@ -36,6 +36,7 @@ COMMANDS:
pack pack build artifacts into an archive for distribution
unpack unpack build artifacts from an distributed archive
upload <tag> upload build artifacts to a GitHub release
cache manage the Lake cache
script manage and run workspace scripts
scripts shorthand for `lake script list`
run <script> shorthand for `lake script run`
@ -113,7 +114,7 @@ def helpBuild :=
"Build targets
USAGE:
lake build [<targets>...]
lake build [<targets>...] [-o <mappings>]
A target is specified with a string of the form:
@ -155,8 +156,14 @@ TARGET EXAMPLES: build the ...
@a/+A:c C file of module `A` of package `a`
:foo facet `foo` of the root package
A bare `lake build` command will build the default target(s) of the root package.
Package dependencies are not updated during a build."
A bare `lake build` command will build the default target(s) of the root
package. Package dependencies are not updated during a build.
With the Lake cache enabled, the `-o` option will cause Lake to track the
input-to-outputs mappings of targets in the root package touched during the
build and write them to the specified file at the end of the build. These
mappings can then be used to upload build artifacts to a remote cache with
`lake cache put`."
def helpQuery :=
"Build targets and output results
@ -303,6 +310,70 @@ USAGE:
If no package is specified, deletes the build directories of every package in
the workspace. Otherwise, just deletes those of the specified packages."
def helpCacheCli :=
"Manage the Lake cache
USAGE:
lake cache <COMMAND>
COMMANDS:
get [<mappings>] download artifacts into the Lake cache
put <mappings> upload artifacts to a remote cache
See `lake cache help <command>` for more information on a specific command."
def helpCacheGet :=
"Download artifacts from a remote service into the Lake cache
USAGE:
lake cache get [<mappings>] [--scope=<remote-scope>] [--max-revs=<n>]
Downloads artifacts for packages in the workspace from a remote cache service.
The cache service used can be configured via the environment variables:
LAKE_CACHE_ARTIFACT_ENDPOINT base URL for artifact downloads
LAKE_CACHE_REVISION_ENDPOINT base URL for the mapping download
If neither of these are set, Lake will use Reservoir instead.
If an input-to-outputs mappings file or a scope is provided, Lake will
download artifacts for the root package. Otherwise, it will download artifacts
for each package in the root's dependency tree in order (using Reservoir).
Non-Reservoir dependencies will be skipped.
To determine the artifacts to download, Lake uses the package's Git revision
(commit hash) to lookup its input-to-outputs mappings on the cache service.
Lake will download the artifacts for the most recent commit with available
mappings. It will backtrack up to `--max-revs`, which defaults to 100.
If set to 0, Lake will search the repository's whole history.
While downloading, Lake will continue on when a download for an artifact
fails or if the download process for a whole package fails. However, it will
report this and exit with a nonzero status code in such cases."
def helpCachePut :=
"Upload artifacts from the Lake cache to a remote service
USAGE:
lake cache put <mappings> --scope=<remote-scope>
Uploads the input-to-outputs mappings contained in the specified file along
with the corresponding output artifacts to a remote cache. The cache service
used is configured via the environment variables:
LAKE_CACHE_KEY authentication key for requests
LAKE_CACHE_ARTIFACT_ENDPOINT base URL for artifact uploads
LAKE_CACHE_REVISION_ENDPOINT base URL for the mapping upload
Files are uploaded using the AWS Signature Version 4 authentication protocol
via `curl`. Thus, the service should generally be an S3-compatible bucket.
Artifacts are uploaded to the artifact endpoint under the prefix `scope`
with a file name corresponding to their Lake content hash. The mappings file
is uploaded to the revision endpoint under the prefix `scope` with a file name
corresponding to the package's current Git revision. As such, the command will
fail if the the work tree currently has changes."
def helpScriptCli :=
"Manage Lake scripts
@ -314,7 +385,7 @@ COMMANDS:
run <script> run a script
doc <script> print the docstring of a given script
See `lake help <command>` for more information on a specific command."
See `lake script help <command>` for more information on a specific command."
def helpScriptList :=
"List available scripts
@ -430,6 +501,11 @@ public def helpScript : (cmd : String) → String
| "doc" => helpScriptDoc
| _ => helpScriptCli
public def helpCache : (cmd : String) → String
| "get" => helpCacheGet
| "put" => helpCachePut
| _ => helpCacheCli
public def help : (cmd : String) → String
| "new" => helpNew
| "init" => helpInit

184
src/lake/Lake/CLI/Main.lean
View file

@ -64,6 +64,11 @@ public structure LakeOptions where
ansiMode : AnsiMode := .auto
outFormat : OutFormat := .text
offline : Bool := false
outputsFile? : Option FilePath := none
forceDownload : Bool := false
scope? : Option String := none
rev? : Option String := none
maxRevs : Nat := 100
def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
opts.outLv?.getD opts.verbosity.minLogLv
@ -117,6 +122,7 @@ def LakeOptions.mkBuildConfig
failLv := opts.failLv
outLv := opts.outLv
ansiMode := opts.ansiMode
outputsFile? := opts.outputsFile?
out; showSuccess
export LakeOptions (mkLoadConfig mkBuildConfig)
@ -190,6 +196,7 @@ def lakeShortOption : (opt : Char) → CliM PUnit
| 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
| 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
| 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
| 'o' => do let outputsFile? ← takeOptArg "-o" "path"; modifyThe LakeOptions ({· with outputsFile?})
| 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
| 'U' => do
logWarning "the '-U' shorthand for '--update' is deprecated"
@ -216,6 +223,20 @@ def lakeLongOption : (opt : String) → CliM PUnit
| "--offline" => modifyThe LakeOptions ({· with offline := true})
| "--wfail" => modifyThe LakeOptions ({· with failLv := .warning})
| "--iofail" => modifyThe LakeOptions ({· with failLv := .info})
| "--force-download" => modifyThe LakeOptions ({· with forceDownload := true})
| "--scope" => do
let scope ← takeOptArg "--scope" "cache scope"
modifyThe LakeOptions ({· with scope? := some scope})
| "--repo" => do
let repo ← takeOptArg "--repo" "repository"
modifyThe LakeOptions ({· with scope? := some repo})
| "--rev" => do
let rev ← takeOptArg "--rev" "Git revision"
modifyThe LakeOptions ({· with rev? := some rev})
| "--max-revs" => do
let some n ← (·.toNat?) <$> takeOptArg "--max-revs" "number of revisions"
| error "argument to `--max-revs` should be a natural number"
modifyThe LakeOptions ({· with maxRevs := n})
| "--log-level" => do
let outLv ← takeOptArg' "--log-level" "log level" LogLevel.ofString?
modifyThe LakeOptions ({· with outLv? := outLv})
@ -303,6 +324,158 @@ def parseTemplateLangSpec (spec : String) : Except CliError (InitTemplate × Con
namespace lake
/-! ### `lake cache` CLI -/
namespace cache
protected def get : CliM PUnit := do
processOptions lakeOption
let opts ← getThe LakeOptions
let mappings? ← takeArg?
noArgsRem do
let cfg ← mkLoadConfig opts
let ws ← loadWorkspace cfg
let cache := ws.lakeCache
if let some file := mappings? then
let some remoteScope := opts.scope?
| error "to use `cache get` with a mappings file, `--scope` must be set"
let service : CacheService :=
if let some artifactEndpoint := ws.lakeEnv.cacheArtifactEndpoint? then
{artifactEndpoint}
else
{apiEndpoint? := some ws.lakeEnv.reservoirApiUrl}
let map ← CacheMap.load file
service.downloadOutputArtifacts map cache remoteScope ws.root.cacheScope opts.forceDownload
else
let service : CacheService ← id do
match ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
| some artifactEndpoint, some revisionEndpoint =>
return {artifactEndpoint, revisionEndpoint}
| none, none =>
return {apiEndpoint? := some ws.lakeEnv.reservoirApiUrl}
| some artifactEndpoint, none =>
error (invalidEndpointConfig artifactEndpoint "")
| none, some revisionEndpoint =>
error (invalidEndpointConfig "" revisionEndpoint)
if let some remoteScope := opts.scope? then
let service := if service.apiEndpoint?.isNone then service else {
artifactEndpoint := s!"{ws.lakeEnv.reservoirApiUrl}/artifacts"
revisionEndpoint := s!"{ws.lakeEnv.reservoirApiUrl}/outputs"
}
let map ← getOutputs cache service ws.root remoteScope opts
service.downloadOutputArtifacts map cache remoteScope ws.root.cacheScope opts.forceDownload
else if service.apiEndpoint?.isSome then -- Reservoir
-- TODO: Parallelize?
let ok ← ws.packages.foldlM (start := 1) (init := true) (m := LoggerIO) fun ok pkg => do
try
if pkg.scope.isEmpty then
logInfo s!"{pkg.name}: skipping non-Reservoir dependency`"
else
let remoteScope := s!"{pkg.scope}/{pkg.name.toString (escape := false)}"
let map ← getOutputs cache service pkg remoteScope opts
service.downloadOutputArtifacts map cache remoteScope pkg.cacheScope opts.forceDownload
return ok
catch _ =>
return false
unless ok do
error "failed to download artifacts for some dependencies"
else
error "to use `cache get` with a custom endpoint, the `--scope` option must be set"
where
invalidEndpointConfig artifactEndpoint revisionEndpoint :=
s!"invalid endpoint configuration:\
\n LAKE_CACHE_ARTIFACT_ENDPOINT={artifactEndpoint}\
\n LAKE_CACHE_REVISION_ENDPOINT={revisionEndpoint}\n\
To use `cache get` with a custom endpoint, both environment variables \
must be set to non-empty strings. To use Reservoir, neither should be set."
getOutputs cache service pkg remoteScope opts : LoggerIO CacheMap := do
let repo := GitRepo.mk pkg.dir
if let some rev := opts.rev? then
let rev ← repo.resolveRevision rev
let some map ← service.downloadRevisionOutputs? rev cache remoteScope
| error s!"{remoteScope}: outputs not found for revision {rev}"
return map
else
if (← repo.hasDiff) then
logWarning s!"{pkg.name}: package has changes; \
only artifacts for committed code will be downloaded"
if .warning ≤ opts.failLv then
failure
let n := opts.maxRevs
let revs ← repo.getHeadRevisions n
let map? ← revs.findSomeM? fun rev =>
service.downloadRevisionOutputs? rev cache remoteScope
let some map := map?
| let revisions :=
if n = 0 || revs.size < n then "for any revision" else s!"in {n} revisions from HEAD"
error s!"{remoteScope}: no outputs found {revisions}"
return map
protected def put : CliM PUnit := do
processOptions lakeOption
let file ← takeArg "mappings"
let opts ← getThe LakeOptions
let some scope := opts.scope?
| error "the `--scope` option must be set for `cache put`"
noArgsRem do
let cfg ← mkLoadConfig opts
let ws ← loadWorkspace cfg
let service : CacheService ← id do
match ws.lakeEnv.cacheKey?, ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
| some key, some artifactEndpoint, some revisionEndpoint =>
return {key, artifactEndpoint, revisionEndpoint}
| key?, artifactEndpoint?, revisionEndpoint? =>
error (invalidEndpointConfig key? artifactEndpoint? revisionEndpoint?)
let pkg := ws.root
let repo := GitRepo.mk pkg.dir
if (← repo.hasDiff) then
logWarning s!"{pkg.name}: package has changes; \
artifacts will be uploaded for the most recent commit"
if .warning ≤ opts.failLv then
exit 1
let rev ← repo.getHeadRevision
let map ← CacheMap.load file
let descrs ← map.collectOutputDescrs
let paths ← ws.lakeCache.getArtifactPaths descrs
service.uploadArtifacts ⟨descrs, rfl⟩ paths scope
-- Mappings are uploaded after artifacts to allow downloads to assume that
-- if the mappings exist, the artifacts should also exist
service.uploadRevisionOutputs rev file scope
where
invalidEndpointConfig key? artifactEndpoint? revisionEndpoint? :=
s!"invalid endpoint configuration:\
\n LAKE_CACHE_KEY is {if key?.isNone then "unset" else "set"}\
\n LAKE_CACHE_ARTIFACT_ENDPOINT={artifactEndpoint?.getD ""}\
\n LAKE_CACHE_REVISION_ENDPOINT={revisionEndpoint?.getD ""}\n\
To use `cache put`, these environment variables must be set to non-empty strings."
protected def add : CliM PUnit := do
processOptions lakeOption
let file ← takeArg "mappings"
let pkg? ← takeArg?
let opts ← getThe LakeOptions
noArgsRem do
let cfg ← mkLoadConfig opts
let ws ← loadWorkspace cfg
let pkg ← match pkg? with
| some pkg => parsePackageSpec ws pkg
| _ => pure ws.root
let scope := pkg.cacheScope
let map ← CacheMap.load file
ws.lakeCache.writeMap scope map
protected def help : CliM PUnit := do
IO.println <| helpCache <| ← takeArgD ""
end cache
def cacheCli : (cmd : String) → CliM PUnit
| "add" => cache.add
| "get" => cache.get
| "put" => cache.put
| "help" => cache.help
| cmd => throw <| CliError.unknownCommand cmd
/-! ### `lake script` CLI -/
namespace script
@ -455,6 +628,16 @@ protected def upload : CliM PUnit := do
let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
ws.root.uploadRelease tag
protected def cache : CliM PUnit := do
if let some cmd ← takeArg? then
processLeadingOptions lakeOption -- between `lake cache <cmd>` and args
if (← getWantsHelp) then
IO.println <| helpCache cmd
else
cacheCli cmd
else
throw <| CliError.missingCommand
protected def setupFile : CliM PUnit := do
processOptions lakeOption
let opts ← getThe LakeOptions
@ -657,6 +840,7 @@ def lakeCli : (cmd : String) → CliM PUnit
| "pack" => lake.pack
| "unpack" => lake.unpack
| "upload" => lake.upload
| "cache" => lake.cache
| "setup-file" => lake.setupFile
| "test" => lake.test
| "check-test" => lake.checkTest

75
src/lake/Lake/Config/Artifact.lean
View file

@ -8,20 +8,75 @@ module
prelude
public import Lake.Build.Trace
open System
open System Lean
namespace Lake
/-- A file with a known content hash. -/
public structure Artifact where
/-- The path to the artifact on the file system. -/
path : FilePath
/-- The name of the artifact. This is used, for example, as a caption in traces. -/
name := path.toString
/-- The modification time of the artifact (or `0` if unknown). -/
mtime : MTime
/-- The content hash of the artifact. -/
/-- Returns the relative file path used for an artifact in the Lake cache (i.e., `{hash}.{ext}`). -/
@[inline] public def artifactPath (contentHash : Hash) (ext := "art") : FilePath :=
if ext.isEmpty then contentHash.toString else s!"{contentHash}.{ext}"
/-- The information needed to identify a single artifact within the Lake cache. -/
public structure ArtifactDescr where
/-- The artifact's content hash. -/
hash : Hash
/-- The artifact's file extension. -/
ext : String := "art"
deriving Inhabited, Repr
/--
A content-hashed artifact that should have the file extension `ext`.
Many applications care about the extension of a file (e.g., use it determine
what kind of operation to perform), so the content hash alone may not be sufficient to
produce a useable artifact for consumers.
-/
@[inline] public def artifactWithExt (contentHash : Hash) (ext := "art") : ArtifactDescr :=
{hash := contentHash, ext}
-- discourage direct use of the constructor
attribute [deprecated artifactWithExt (since := "2025-08-30")] ArtifactDescr.mk
namespace ArtifactDescr
/-- Returns the relative file path used for the output's artifact in the Lake cache (c.f. `artifactPath`). -/
@[inline] public def toFilePath (self : ArtifactDescr) : FilePath :=
artifactPath self.hash self.ext
public instance : ToString ArtifactDescr := ⟨(·.toFilePath.toString)⟩
public instance : ToJson ArtifactDescr := ⟨(toJson ·.toFilePath)⟩
/-- Parse an output's relative file path into an `ArtifactDescr`. -/
public def ofFilePath? (path : FilePath) : Except String ArtifactDescr := do
let s := path.toString
let pos := s.posOf '.'
if h : s.atEnd pos then
let some hash := Hash.ofString? s
| throw "expected artifact file name to be a content hash"
return {hash, ext := ""}
else
let some hash := Hash.ofString? <| s.extract 0 pos
| throw "expected artifact file name to be a content hash"
let ext := s.extract (s.next' pos h) s.endPos
return {hash, ext}
public protected def fromJson? (data : Json) : Except String ArtifactDescr := do
match fromJson? data with
| .ok (out : String) => ofFilePath? out
| .error e => throw s!"artifact in unexpected JSON format: {e}"
public instance : FromJson ArtifactDescr := ⟨ArtifactDescr.fromJson?⟩
end ArtifactDescr
/-- A file with a known content hash. -/
public structure Artifact extends descr : ArtifactDescr where
/-- The preferred path to the artifact on the file system. -/
path : FilePath
/-- The artifact's. This is used, for example, as a caption in traces. -/
name := path.toString
/-- The artifact's modification time (or `0` if unknown). -/
mtime : MTime
deriving Inhabited, Repr
namespace Artifact

399
src/lake/Lake/Config/Cache.lean
View file

@ -9,61 +9,18 @@ prelude
public import Lake.Util.Log
public import Lake.Config.Artifact
public import Lake.Build.Trace
import Lake.Build.Actions
import Lake.Util.Url
import Lake.Util.Proc
import Lake.Util.Reservoir
import Lake.Util.IO
open Lean System
namespace Lake
/-- The Lake cache directory. -/
public structure Cache where
dir : FilePath
deriving Inhabited
namespace Cache
/--
Returns whether the Lake cache is disabled.
An empty directory string indicates the cache is disabled.
-/
public def isDisabled (cache : Cache) : Bool :=
cache.dir.toString.isEmpty
/-- Returns the artifact directory for the Lake cache. -/
@[inline] public def artifactDir (cache : Cache) : FilePath :=
cache.dir / "artifacts"
/-- Returns the path to artifact in the Lake cache with extension `ext`. -/
public def artifactPath (cache : Cache) (contentHash : Hash) (ext := "art") : FilePath :=
cache.artifactDir / if ext.isEmpty then contentHash.toString else s!"{contentHash}.{ext}"
/--
Returns the path to the artifact in the Lake cache with extension `ext` if it exists.
If the Lake cache is disabled, the behavior of this function is undefined.
-/
public def getArtifact? (cache : Cache) (contentHash : Hash) (ext := "art") : BaseIO (Option Artifact) := do
let path := cache.artifactPath contentHash ext
if let .ok mtime ← getMTime path |>.toBaseIO then
return some {path, mtime, hash := contentHash}
else if (← path.pathExists) then
return some {path, mtime := 0, hash := contentHash}
else
return none
/-- The file where the package's input mapping is stored in the Lake cache. -/
@[inline] public def inputsDir (cache : Cache) : FilePath :=
cache.dir / "inputs"
/-- The file where a package's input mapping is stored in the Lake cache. -/
public def inputsFile (pkgName : String) (cache : Cache) : FilePath :=
cache.inputsDir / s!"{pkgName}.jsonl"
end Cache
/--
Maps an input hash to a structure of artifact content hashes.
Maps an input hash to a structure of output artifact content hashes.
These mappings are stored in a per-package JSON Lines file in the Lake cache.
-/
@ -71,6 +28,45 @@ public abbrev CacheMap := Std.HashMap Hash Json
namespace CacheMap
/-- The current version of the input-to-output mappings file format. -/
public def schemaVersion : String := "2025-09-10"
def checkSchemaVersion (inputName : String) (line : String) : LogIO Unit := do
if line.isEmpty then
error s!"{inputName}: expected schema version on line 1"
match Json.parse line >>= fromJson? with
| .ok (ver : String) =>
if ver != schemaVersion then
logWarning s!"{inputName}: unknown schema version '{ver}'; may not parse correctly"
| .error e =>
logWarning s!"{inputName}: invalid schema version on line 1: {e}"
/-- Parse a `Cache` from a JSON Lines string. -/
public partial def parse (inputName : String) (contents : String) : LoggerIO CacheMap := do
let rec loop (i : Nat) (cache : CacheMap) (stopPos pos : String.Pos) := do
let lfPos := contents.posOfAux '\n' stopPos pos
let line := contents.extract pos lfPos
if line.trim.isEmpty then
return cache
let cache ← id do
match Json.parse line >>= fromJson? with
| .ok (inputHash, arts) =>
return cache.insert inputHash arts
| .error e =>
logWarning s!"{inputName}: invalid JSON on line {i}: {e}"
return cache
if h : contents.atEnd lfPos then
return cache
else
loop (i+1) cache stopPos (contents.next' lfPos h)
let lfPos := contents.posOfAux '\n' contents.endPos 0
let line := contents.extract 0 lfPos
checkSchemaVersion inputName line.trim
if h : contents.atEnd lfPos then
return {}
else
loop 2 {} contents.endPos (contents.next' lfPos h)
@[inline] private partial def loadCore
(h : IO.FS.Handle) (fileName : String)
: LogIO CacheMap := do
@ -84,36 +80,65 @@ namespace CacheMap
| .error e =>
logWarning s!"{fileName}: invalid JSON on line {i}: {e}"
loop (i+1) cache
loop 1 {}
let line ← h.getLine
checkSchemaVersion fileName line
loop 2 {}
/-- Load a `CacheMap` from a JSON Lines file. -/
public def load (inputsFile : FilePath) : LogIO CacheMap := do
match (← IO.FS.Handle.mk inputsFile .read |>.toBaseIO) with
/--
Loads a `CacheMap` from a JSON Lines file.
Errors if the the file is ill-formatted or the read fails for other reasons.
-/
public def load (file : FilePath) : LogIO CacheMap := do
match (← IO.FS.Handle.mk file .read |>.toBaseIO) with
| .ok h =>
h.lock (exclusive := false)
loadCore h inputsFile.toString
| .error (.noFileOrDirectory ..) =>
return {}
loadCore h file.toString
| .error e =>
error s!"{inputsFile}: failed to open file: {e}"
error s!"{file}: failed to open file: {e}"
/-
Loads a `CacheMap` from a JSON Lines file. Returns `none` if the file does not exist.
Errors if the manifest is ill-formatted or the read fails for other reasons.
-/
public def load? (file : FilePath) : LogIO (Option CacheMap) := do
match (← IO.FS.Handle.mk file .read |>.toBaseIO) with
| .ok h =>
h.lock (exclusive := false)
loadCore h file.toString
| .error (.noFileOrDirectory ..) =>
return none
| .error e =>
error s!"{file}: failed to open file: {e}"
/--
Save a `CacheMap` to a JSON Lines file.
Entries already in the file but not in the map will not be removed.
-/
public def save (inputsFile : FilePath) (cache : CacheMap) : LogIO Unit := do
createParentDirs inputsFile
discard <| IO.FS.Handle.mk inputsFile .append -- ensure file exists
match (← IO.FS.Handle.mk inputsFile .readWrite |>.toBaseIO) with
public def updateFile (file : FilePath) (cache : CacheMap) : LogIO Unit := do
createParentDirs file
discard <| IO.FS.Handle.mk file .append -- ensure file exists
match (← IO.FS.Handle.mk file .readWrite |>.toBaseIO) with
| .ok h =>
h.lock (exclusive := true)
let currEntries ← loadCore h inputsFile.toString
let currEntries ← loadCore h file.toString
let cache := cache.fold (fun m k v => m.insert k v) currEntries
h.rewind
cache.forM fun k v =>
h.putStrLn (toJson (k, v)).compress
| .error e =>
error s!"{inputsFile}: failed to open file: {e}"
error s!"{file}: failed to open file: {e}"
/-- Write a `CacheMap` to a JSON Lines file. -/
public def writeFile (file : FilePath) (cache : CacheMap) : LogIO Unit := do
createParentDirs file
match (← IO.FS.Handle.mk file .write |>.toBaseIO) with
| .ok h =>
h.lock (exclusive := true)
h.putStrLn (toJson schemaVersion).compress
cache.forM fun k v =>
h.putStrLn (toJson (k, v)).compress
| .error e =>
error s!"{file}: failed to open file: {e}"
/-- Returns the output data associated with the input hash in the cache. -/
public nonrec def get? (inputHash : Hash) (cache : CacheMap) : Option Json :=
@ -127,6 +152,32 @@ public def insertCore (inputHash : Hash) (val : Json) (cache : CacheMap) : Cache
@[inline] public def insert [ToJson α] (inputHash : Hash) (val : α) (cache : CacheMap) : CacheMap :=
cache.insertCore inputHash (toJson val)
/-- Extract each output from their structured data into a flat array of artifact descriptions. -/
public partial def collectOutputDescrs (map : CacheMap) : LogIO (Array ArtifactDescr) := do
throwIfLogs <| map.foldM (init := #[]) fun as _ o => go as o
where go as o := do
match o with
| .null =>
return as
| .bool b =>
logError s!"unsupported output: {b}"
return as
| .num o =>
match Hash.ofJsonNumber? o with
| .ok hash =>
return as.push {hash}
| .error reason =>
logError s!"unsupported output; {reason}: {o}"
return as
| .str o =>
match ArtifactDescr.ofFilePath? o with
| .ok a => return as.push a
| .error e =>
logError s!"unsupported output: {e}"
return as
| .arr os => os.foldlM (init := as) go
| .obj os => os.foldlM (init := as) fun as _ o => go as o
end CacheMap
/-- A mutable reference to a `CacheMap`. -/
@ -134,6 +185,9 @@ public abbrev CacheRef := IO.Ref CacheMap
namespace CacheRef
@[inline] public def mk (init : CacheMap := {}) : BaseIO CacheRef :=
IO.mkRef init
@[inline, inherit_doc CacheMap.get?]
public def get? (inputHash : Hash) (cache : CacheRef) : BaseIO (Option Json) :=
cache.modifyGet fun m => (m.get? inputHash, m)
@ -143,3 +197,224 @@ public def insert [ToJson α] (inputHash : Hash) (val : α) (cache : CacheRef) :
cache.modify (·.insert inputHash (toJson val))
end CacheRef
/-- The Lake cache directory. -/
public structure Cache where
dir : FilePath
deriving Inhabited
namespace Cache
/-- Returns the artifact directory for the Lake cache. -/
@[inline] public def artifactDir (cache : Cache) : FilePath :=
cache.dir / "artifacts"
/-- Returns the path to artifact in the Lake cache with extension `ext`. -/
@[inline] public protected def artifactPath (cache : Cache) (contentHash : Hash) (ext := "art") : FilePath :=
cache.artifactDir / artifactPath contentHash ext
/-- Returns the artifact in the Lake cache corresponding the given artifact description. -/
public def getArtifact? (cache : Cache) (descr : ArtifactDescr) : BaseIO (Option Artifact) := do
let path := cache.artifactDir / descr.toFilePath
if let .ok mtime ← getMTime path |>.toBaseIO then
return some {descr, path, mtime}
else if (← path.pathExists) then
return some {descr, path, mtime := 0}
else
return none
/-- Returns path to the artifact for each output. Errors if any are missing. -/
public def getArtifactPaths
(cache : Cache) (descrs : Array ArtifactDescr)
: LogIO (Vector FilePath descrs.size) := throwIfLogs do
(Vector.mk descrs rfl).mapM fun out => do
let art := cache.artifactDir / out.toFilePath
unless (← art.pathExists) do
logError s!"artifact not found in cache: {art}"
return art
/-- The directory where input-to-output mappings are stored in the Lake cache. -/
@[inline] public def outputsDir (cache : Cache) : FilePath :=
cache.dir / "outputs"
/-- The file containing the outputs of the the given input for the package. -/
@[inline] public def outputsFile (cache : Cache) (scope : String) (inputHash : Hash) : FilePath :=
cache.outputsDir / scope / s!"{inputHash}.json"
/-- Cache the outputs corresponding to the given input for the package. -/
public def writeOutputsCore
(cache : Cache) (scope : String) (inputHash : Hash) (outputs : Json)
: IO Unit := do
let file := cache.outputsFile scope inputHash
createParentDirs file
IO.FS.writeFile file outputs.compress
/-- Cache the outputs corresponding to the given input for the package. -/
@[inline] public def writeOutputs
[ToJson α] (cache : Cache) (scope : String) (inputHash : Hash) (outputs : α)
: IO Unit := cache.writeOutputsCore scope inputHash (toJson outputs)
/-- Cache the input-to-outputs mappings from a `CacheMap`. -/
public def writeMap (cache : Cache) (scope : String) (map : CacheMap) : IO Unit :=
map.forM fun i o => cache.writeOutputsCore scope i o
/-- Retrieve the cached outputs corresponding to the given input for the package (if any). -/
public def readOutputs? (cache : Cache) (scope : String) (inputHash : Hash) : LogIO (Option Json) := do
let path := cache.outputsFile scope inputHash
match (← IO.FS.readFile path |>.toBaseIO) with
| .ok contents =>
match Json.parse contents with
| .ok outputs => return outputs
| .error e =>
logWarning s!"{path}: invalid JSON: {e}"
return none
| .error (.noFileOrDirectory ..) => return none
| .error e => error s!"{path}: read failed: {e}"
/-- The directory where input-to-output mappings of downloaded package revisions are cached. -/
@[inline] public def revisionDir (cache : Cache) : FilePath :=
cache.dir / "revisions"
/-- Returns path to the input-to-output mappings of a downloaded package revision. -/
@[inline] public def revisionPath (cache : Cache) (scope : String) (rev : String) : FilePath :=
cache.revisionDir / scope / s!"{rev}.jsonl"
end Cache
/-- Uploads a file to an online bucket using the Amazon S3 protocol. -/
def uploadS3
(file : FilePath) (contentType : String) (url : String) (key : String)
: LoggerIO Unit := do
proc {
cmd := "curl"
args := #[
"-s",
"--aws-sigv4", "aws:amz:auto:s3", "--user", key,
"-X", "PUT", "-T", file.toString, url,
"-H", s!"Content-Type: {contentType}"
]
} (quiet := true)
/--
Configuration of a remote cache service (e.g., Reservoir or an S3 bucket).
All fields are not required to be valid.
A user should set at least the necessary ones for a given function.
-/
public structure CacheService where
key : String := ""
artifactEndpoint : String := ""
revisionEndpoint : String := ""
/-- Reservoir API endpoint. -/
apiEndpoint? : Option String := none
namespace CacheService
/-- The MIME type of Lake/Reservoir artifact. -/
public def artifactContentType : String := "application/vnd.reservoir.artifact"
public def artifactUrl (contentHash : Hash) (scope : String) (service : CacheService) : String :=
let scope := "/".intercalate <| scope.split (· == '/') |>.map uriEncode
if let some apiEndpoint := service.apiEndpoint? then
s!"{apiEndpoint}/packages/{scope}/artifacts/{contentHash.hex}.art"
else
s!"{service.artifactEndpoint}/{scope}/{contentHash.hex}.art"
public def downloadArtifact
(descr : ArtifactDescr) (cache : Cache) (scope : String)
(service : CacheService) (force := false)
: LoggerIO Unit := do
let url := service.artifactUrl descr.hash scope
let path := cache.artifactDir / descr.toFilePath
if (← path.pathExists) && !force then
return
logInfo s!"\
{scope}: downloading artifact {descr.hash}\
\n local path: {path}\
\n remote URL: {url}"
download url path
let hash ← computeFileHash path
if hash != descr.hash then
logError s!"{path}: downloaded artifact does not have expect hash"
IO.FS.removeFile path
failure
public def downloadArtifacts
(descrs : Array ArtifactDescr) (cache : Cache) (scope : String)
(service : CacheService) (force := false)
: LoggerIO Unit := do
let ok ← descrs.foldlM (init := true) fun ok descr =>
try
service.downloadArtifact descr cache scope force
return ok
catch _ =>
return false
unless ok do
error s!"{scope}: failed to download some artifacts"
public def downloadOutputArtifacts
(map : CacheMap) (cache : Cache) (remoteScope localScope : String)
(service : CacheService) (force := false)
: LoggerIO Unit := do
cache.writeMap localScope map
let descrs ← map.collectOutputDescrs
service.downloadArtifacts descrs cache remoteScope force
public def uploadArtifact
(contentHash : Hash) (art : FilePath) (scope : String) (service : CacheService)
: LoggerIO Unit := do
let url := service.artifactUrl contentHash scope
logInfo s!"\
{scope}: uploading artifact {contentHash}\
\n local path: {art}\
\n remote URL: {url}"
uploadS3 art artifactContentType url service.key
public def uploadArtifacts
(descrs : Vector ArtifactDescr n) (paths : Vector FilePath n) (scope : String) (service : CacheService)
: LoggerIO Unit := n.forM fun n h => uploadArtifact descrs[n].hash paths[n] scope service
/-- The MIME type of Lake/Reservoir input-to-output mappings for a Git revision. -/
public def mapContentType : String := "application/vnd.reservoir.outputs+json-lines"
public def revisionUrl (rev : String) (scope : String) (service : CacheService) : String :=
let scope := "/".intercalate <| scope.split (· == '/') |>.map uriEncode
if let some apiEndpoint := service.apiEndpoint? then
s!"{apiEndpoint}/packages/{scope}/build-outputs?rev={rev}"
else
s!"{service.revisionEndpoint}/{scope}/{rev}.jsonl"
public def downloadRevisionOutputs?
(rev : String) (cache : Cache) (scope : String)
(service : CacheService) (force := false)
: LoggerIO (Option CacheMap) := do
let path := cache.revisionPath rev scope
if (← path.pathExists) && !force then
return ← CacheMap.load path
let url := service.revisionUrl rev scope
logInfo s!"\
{scope}: downloading build outputs for revision {rev}\
\n local path: {path}\
\n remote URL: {url}"
let headers := if service.apiEndpoint?.isSome then Reservoir.lakeHeaders else {}
let contents? ← try getUrl? url headers catch e =>
logError s!"{scope}: output lookup failed"
throw e
let some contents := contents?
| return none
createParentDirs path
IO.FS.writeFile path contents
CacheMap.load path
public def uploadRevisionOutputs
(rev : String) (outputs : FilePath) (scope : String) (service : CacheService)
: LoggerIO Unit := do
let url := service.revisionUrl rev scope
logInfo s!"\
{scope}: uploading build outputs for revision {rev}\
\n local path: {outputs}\
\n remote URL: {url}"
uploadS3 outputs mapContentType url service.key
end CacheService

47
src/lake/Lake/Config/Env.lean
View file

@ -28,7 +28,7 @@ public structure Env where
lean : LeanInstall
/-- The Elan installation (if any) of the environment. -/
elan? : Option ElanInstall
/-- The Reservoir API endpoint URL (e.g., `https://reservoir.lean-lang.org/api`). -/
/-- The Reservoir API endpoint URL (e.g., `https://reservoir.lean-lang.org/api/v1`). -/
reservoirApiUrl : String
/-- Overrides the detected Lean's githash as the string Lake uses for Lean traces. -/
githashOverride : String
@ -41,8 +41,17 @@ public structure Env where
noCache : Bool
/-- Whether the Lake artifact cache should be enabled by default (i.e., `LAKE_ARTIFACT_CACHE`). -/
enableArtifactCache : Bool
/-- The directory of the Lake cache. Set by `LAKE_CACHE_DIR`. If `none`, the cache is disabled. -/
lakeCache : Cache
/--
The system directory for the Lake cache. Set by `LAKE_CACHE_DIR`.
If `none`, no suitable system directory for the cache exists.
-/
lakeCache? : Option Cache
/-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/
cacheKey? : Option String
/-- The base URL for artifact uploads and downloads from the cache (i.e., `LAKE_CACHE_ARTIFACT_ENDPOINT`). -/
cacheArtifactEndpoint? : Option String
/-- The base URL for revision uploads and downloads from the cache (i.e., `LAKE_CACHE_REVISION_ENDPOINT`). -/
cacheRevisionEndpoint? : Option String
/-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/
initToolchain : String
/-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/
@ -89,16 +98,22 @@ namespace Env
public def computeToolchain : BaseIO String := do
return (← IO.getEnv "ELAN_TOOLCHAIN").getD Lean.toolchain
/-- Compute the cache location used by Lake from the process environment. May be disabled. -/
public def computeCache (elan? : Option ElanInstall) (toolchain : String) : BaseIO Cache := do
/--
Compute the system cache location from the process environment.
If `none`, no system directory for workspace the cache exists.
-/
public def computeCache? (elan? : Option ElanInstall) (toolchain : String) : BaseIO (Option Cache) := do
if let some cacheDir ← IO.getEnv "LAKE_CACHE_DIR" then
return ⟨cacheDir⟩
if cacheDir.isEmpty then
return none
else
return some ⟨cacheDir⟩
else if let some elan := elan? then
return ⟨elan.toolchainDir toolchain / "lake" / "cache"⟩
return some ⟨elan.toolchainDir toolchain / "lake" / "cache"⟩
else if let some cacheHome ← getSystemCacheHome? then
return ⟨cacheHome / "lake"⟩
return some ⟨cacheHome / "lake"⟩
else
return ⟨""⟩
return none
/--
Compute a `Lake.Env` object from the given installs
@ -118,7 +133,10 @@ public def compute
reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
enableArtifactCache := (← IO.getEnv "LAKE_ARTIFACT_CACHE").bind envToBool? |>.getD false
lakeCache := ← computeCache elan? toolchain
lakeCache? := ← computeCache? elan? toolchain
cacheKey? := (← IO.getEnv "LAKE_CACHE_KEY").map (·.trim)
cacheArtifactEndpoint? := (← IO.getEnv "LAKE_CACHE_ARTIFACT_ENDPOINT").map normalizeUrl
cacheRevisionEndpoint? := (← IO.getEnv "LAKE_CACHE_REVISION_ENDPOINT").map normalizeUrl
githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
toolchain
initToolchain
@ -135,9 +153,11 @@ where
| .error e => throw s!"'LAKE_PKG_URL_MAP' has invalid JSON: {e}"
@[macro_inline] getUrlD var default := do
if let some url ← IO.getEnv var then
return if url.back == '/' then url.dropRight 1 else url
return normalizeUrl url
else
return default
normalizeUrl url :=
if url.back == '/' then url.dropRight 1 else url
/--
The string Lake uses to identify Lean in traces.
@ -213,7 +233,9 @@ public def baseVars (env : Env) : Array (String × Option String) :=
("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
("LAKE_NO_CACHE", toString env.noCache),
("LAKE_ARTIFACT_CACHE", toString env.enableArtifactCache),
("LAKE_CACHE_DIR", if env.lakeCache.isDisabled then none else env.lakeCache.dir.toString),
("LAKE_CACHE_KEY", env.cacheKey?),
("LAKE_CACHE_ARTIFACT_ENDPOINT", env.cacheArtifactEndpoint?),
("LAKE_CACHE_REVISION_ENDPOINT", env.cacheRevisionEndpoint?),
("LEAN", env.lean.lean.toString),
("LEAN_SYSROOT", env.lean.sysroot.toString),
("LEAN_AR", env.lean.ar.toString),
@ -223,6 +245,7 @@ public def baseVars (env : Env) : Array (String × Option String) :=
/-- Environment variable settings for the `Lake.Env`. -/
public def vars (env : Env) : Array (String × Option String) :=
let vars := env.baseVars ++ #[
("LAKE_CACHE_DIR", if let some cache := env.lakeCache? then cache.dir.toString else ""),
("LEAN_PATH", some env.leanPath.toString),
("LEAN_SRC_PATH", some env.leanSrcPath.toString),
("LEAN_GITHASH", env.leanGithash),

24
src/lake/Lake/Config/Monad.lean
View file

@ -139,6 +139,23 @@ public def getLeanArgs : m (Array String) :=
@[inline] public def getAugmentedEnv : m (Array (String × Option String)) :=
(·.augmentedEnvVars) <$> getWorkspace
/-- Returns the Lake cache for the environment. -/
@[inline] public def getLakeCache : m Cache :=
(·.lakeCache) <$> getWorkspace
@[inline, inherit_doc Cache.getArtifact?]
public def getArtifact? [Bind m] [MonadLiftT BaseIO m] (descr : ArtifactDescr) : m (Option Artifact) :=
getLakeCache >>= (·.getArtifact? descr)
/--
Returns whether the package the artifact cache is enabled for the package.
If the package has not configured the artifact cache itself through `Package.enableArtifactCache?`,
this will default to the workspace configuration.
-/
public def Package.isArtifactCacheEnabled [MonadWorkspace m] (self : Package) : m Bool :=
(self.enableArtifactCache?.getD ·.enableArtifactCache) <$> getWorkspace
end
section
@ -170,13 +187,6 @@ variable [Functor m]
@[inline] public def getElanToolchain : m String :=
(·.toolchain) <$> getLakeEnv
/-- Returns the Lake cache for the environment. May be disabled. -/
@[inline] public def getLakeCache : m Cache :=
(·.lakeCache) <$> getLakeEnv
@[inline, inherit_doc Cache.getArtifact?]
public def getArtifact? [Bind m] [MonadLiftT BaseIO m] (contentHash : Hash) (ext := "art") : m (Option Artifact) :=
getLakeEnv >>= (·.lakeCache.getArtifact? contentHash ext)
/-! ### Search Path Helpers -/

16
src/lake/Lake/Config/Package.lean
View file

@ -73,10 +73,15 @@ public structure Package where
/-- The driver used for `lake lint` when this package is the workspace root. -/
lintDriver : String := config.lintDriver
/--
Input-to-content map for hashes of package artifacts.
Input-to-output(s) map for hashes of package artifacts.
If `none`, the artifact cache is disabled for the package.
-/
cacheRef? : Option CacheRef := none
inputsRef? : Option CacheRef := none
/--
Input-to-output(s) map for hashes of package artifacts.
If `none`, the artifact cache is disabled for the package.
-/
outputsRef? : Option CacheRef := none
deriving Inhabited
@ -339,10 +344,9 @@ public def nativeLibDir (self : Package) : FilePath :=
@[inline] public def enableArtifactCache? (self : Package) : Option Bool :=
self.config.enableArtifactCache?
/-- The file where the package's input-to-content mapping is stored in the Lake cache. -/
public def inputsFileIn (cache : Cache) (self : Package) : FilePath :=
let pkgName := self.name.toString (escape := false)
cache.inputsFile pkgName
/-- The directory within the Lake cache were package-scoped files are stored. -/
public def cacheScope (self : Package) :=
self.name.toString (escape := false)
/-- Try to find a target configuration in the package with the given name. -/
public def findTargetDecl? (name : Name) (self : Package) : Option (NConfigDecl self.name name) :=

22
src/lake/Lake/Config/Workspace.lean
View file

@ -31,7 +31,10 @@ public structure Workspace : Type where
A value of `none` means that Lake is not restartable via the CLI.
-/
lakeArgs? : Option (Array String) := none
/-- The packages within the workspace (in `require` declaration order). -/
/--
The packages within the workspace
(in `require` declaration order with the root coming first).
-/
packages : Array Package := {}
/-- Name-package map of packages within the workspace. -/
packageMap : DNameMap NPackage := {}
@ -50,10 +53,6 @@ namespace Workspace
@[inline] def bootstrap (ws : Workspace) : Bool :=
ws.root.bootstrap
/-- The Lake cache. May be disabled. -/
@[inline] public def lakeCache (ws : Workspace) : Cache :=
ws.lakeEnv.lakeCache
/-- The path to the workspace's directory (i.e., the directory of the root package). -/
@[inline] public def dir (self : Workspace) : FilePath :=
self.root.dir
@ -70,6 +69,18 @@ namespace Workspace
@[inline] public def lakeDir (self : Workspace) : FilePath :=
self.root.lakeDir
/-- The Lake cache. -/
@[inline] public def lakeCache (ws : Workspace) : Cache :=
ws.lakeEnv.lakeCache?.getD ⟨ws.lakeDir⟩
/-- Whether the Lake artifact cache should be enabled by default for packages in the workspace. -/
@[inline] public def enableArtifactCache (ws : Workspace) : Bool :=
ws.lakeEnv.enableArtifactCache
/-- Whether the Lake artifact cache should is enabled for workspace's root package. -/
public def isRootArtifactCacheEnabled (ws : Workspace) : Bool :=
ws.root.enableArtifactCache?.getD ws.enableArtifactCache
/-- The path to the workspace's remote packages directory relative to `dir`. -/
@[inline] public def relPkgsDir (self : Workspace) : FilePath :=
self.root.relPkgsDir
@ -248,6 +259,7 @@ These are the settings use by `lake env` / `Lake.env` to run executables.
-/
public def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
let vars := self.lakeEnv.baseVars ++ #[
("LAKE_CACHE_DIR", some self.lakeCache.dir.toString),
("LEAN_PATH", some self.augmentedLeanPath.toString),
("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
-- Allow the Lean version to change dynamically within core

2
src/lake/Lake/Load/Manifest.lean
View file

@ -241,7 +241,7 @@ public def load (file : FilePath) : IO Manifest := do
/--
Parse a manifest file. Returns `none` if the file does not exist.
Errors if the manifest is ill-formatted or the read files for other reasons.
Errors if the manifest is ill-formatted or the read fails for other reasons.
-/
public def load? (file : FilePath) : IO (Option Manifest) := do
match (← inline (load file) |>.toBaseIO) with

8
src/lake/Lake/Load/Package.lean
View file

@ -87,11 +87,3 @@ public def loadPackageCore
public def loadPackage (config : LoadConfig) : LogIO Package := do
Lean.searchPathRef.set config.lakeEnv.leanSearchPath
(·.1) <$> loadPackageCore "[root]" config
/-- Load the package's input-to-content mapping from the Lake cache (if enabled). -/
public protected def Package.loadInputsFrom (env : Env) (pkg : Package) : LogIO Package := do
if env.lakeCache.isDisabled || !(pkg.enableArtifactCache?.getD env.enableArtifactCache) then
return pkg
else
let inputs ← CacheMap.load (pkg.inputsFileIn env.lakeCache)
return {pkg with cacheRef? := ← IO.mkRef inputs}

1
src/lake/Lake/Load/Resolve.lean
View file

@ -49,7 +49,6 @@ def loadDepPackage
scope := dep.scope
remoteUrl := dep.remoteUrl
}
let pkg ← pkg.loadInputsFrom ws.lakeEnv
if let some env := env? then
let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
return (pkg, ws)

2
src/lake/Lake/Load/Workspace.lean
View file

@ -29,7 +29,7 @@ Does not resolve dependencies.
private def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
Lean.searchPathRef.set config.lakeEnv.leanSearchPath
let (root, env?) ← loadPackageCore "[root]" config
let root ← root.loadInputsFrom config.lakeEnv
let root := {root with outputsRef? := ← CacheRef.mk}
let ws : Workspace := {
root
lakeEnv := config.lakeEnv

88
src/lake/Lake/Reservoir.lean
View file

@ -9,8 +9,9 @@ prelude
public import Lake.Util.Log
public import Lake.Util.JsonObject
public import Lake.Config.Env
public import Lake.Util.Reservoir
import Lake.Util.Proc
import all Init.Data.String.Extra
import Lake.Util.Url
/-! # Package Registries
@ -102,86 +103,6 @@ public instance : FromJson RegistryPkg := ⟨RegistryPkg.fromJson?⟩
end RegistryPkg
public def hexEncodeByte (b : UInt8) : Char :=
if b = 0 then '0' else
if b = 1 then '1' else
if b = 2 then '2' else
if b = 3 then '3' else
if b = 4 then '4' else
if b = 5 then '5' else
if b = 6 then '6' else
if b = 7 then '7' else
if b = 8 then '8' else
if b = 9 then '9' else
if b = 0xa then 'A' else
if b = 0xb then 'B' else
if b = 0xc then 'C' else
if b = 0xd then 'D' else
if b = 0xe then 'E' else
if b = 0xf then 'F' else
'*'
/-- Encode a byte as a URI escape code (e.g., `%20`). -/
public def uriEscapeByte (b : UInt8) (s := "") : String :=
s.push '%' |>.push (hexEncodeByte <| b >>> 4) |>.push (hexEncodeByte <| b &&& 0xF)
/-- Folds a monadic function over the UTF-8 bytes of `Char` from most significant to least significant. -/
@[specialize] public def foldlUtf8M [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
let s := init
let v := c.val
if v ≤ 0x7f then
f s v.toUInt8
else if v ≤ 0x7ff then
let s ← f s <| (v >>> 6).toUInt8 &&& 0x1f ||| 0xc0
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
else if v ≤ 0xffff then
let s ← f s <| (v >>> 12).toUInt8 &&& 0x0f ||| 0xe0
let s ← f s <| (v >>> 6).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
else
let s ← f s <| (v >>> 18).toUInt8 &&& 0x07 ||| 0xf0
let s ← f s <| (v >>> 12).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| (v >>> 6).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
public abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ :=
Id.run <| foldlUtf8M c (pure <| f · ·) init
example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by
simp only [foldlUtf8, foldlUtf8M, String.utf8EncodeChar_eq_utf8EncodeCharFast, String.utf8EncodeCharFast]
if h1 : c.val ≤ 0x7f then simp [h1]
else if h2 : c.val ≤ 0x7ff then simp [h1, h2]
else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3]
else simp [h1, h2, h3]
/-- Encode a character as a sequence of URI escape codes representing its UTF8 encoding. -/
public def uriEscapeChar (c : Char) (s := "") : String :=
foldlUtf8 c (init := s) fun s b => uriEscapeByte b s
/-- A URI unreserved mark as specified in [RFC2396](https://datatracker.ietf.org/doc/html/rfc2396#section-2.3). -/
public def isUriUnreservedMark (c : Char) : Bool :=
c matches '-' | '_' | '.' | '!' | '~' | '*' | '\'' | '(' | ')'
/-- Encodes anything but a URI unreserved character as a URI escape sequences. -/
public def uriEncodeChar (c : Char) (s := "") : String :=
if c.isAlphanum || isUriUnreservedMark c then
s.push c
else
uriEscapeChar c s
/-- Encodes a string as an ASCII URI component, escaping special characters (and unicode). -/
public def uriEncode (s : String) : String :=
s.foldl (init := "") fun s c => uriEncodeChar c s
/-- Perform a HTTP `GET` request of a URL (using `curl`) and return the body. -/
public def getUrl (url : String) (headers : Array String := #[]) : LogIO String := do
let args := #["-s", "-L", "--retry", "3"] -- intermittent network errors can occur
let args := headers.foldl (init := args) (· ++ #["-H", ·])
captureProc {cmd := "curl", args := args.push url}
/-- A Reservoir API response object. -/
public inductive ReservoirResp (α : Type u)
| data (a : α)
@ -201,11 +122,6 @@ public instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.
public def Reservoir.pkgApiUrl (lakeEnv : Lake.Env) (owner pkg : String) :=
s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
public def Reservoir.lakeHeaders := #[
"X-Reservoir-Api-Version:1.0.0",
"X-Lake-Registry-Api-Version:0.1.0"
]
public def Reservoir.fetchPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Option RegistryPkg) := do
let url := Reservoir.pkgApiUrl lakeEnv owner pkg
let out ←

1
src/lake/Lake/Toml/Data/DateTime.lean
View file

@ -7,6 +7,7 @@ module
prelude
public import Lake.Util.Date
import Lake.Util.String
/-!
# TOML Date-Time

1
src/lake/Lake/Toml/Data/Value.lean
View file

@ -9,6 +9,7 @@ prelude
public import Init.Data.Float
public import Lake.Toml.Data.Dict
public import Lake.Toml.Data.DateTime
import Lake.Util.String
/-!
# TOML Value

3
src/lake/Lake/Util.lean
View file

@ -32,7 +32,10 @@ public import Lake.Util.OrderedTagAttribute
public import Lake.Util.OrdHashSet
public import Lake.Util.Proc
public import Lake.Util.RBArray
public import Lake.Util.Reservoir
public import Lake.Util.Store
public import Lake.Util.StoreInsts
public import Lake.Util.String
public import Lake.Util.Task
public import Lake.Util.Url
public import Lake.Util.Version

10
src/lake/Lake/Util/Date.lean
View file

@ -7,6 +7,7 @@ module
prelude
public import Init.Data.Ord.Basic
import Lake.Util.String
/-!
# Date
@ -17,15 +18,6 @@ parser (for nightlies).
namespace Lake
public def lpad (s : String) (c : Char) (len : Nat) : String :=
"".pushn c (len - s.length) ++ s
public def rpad (s : String) (c : Char) (len : Nat) : String :=
s.pushn c (len - s.length)
public def zpad (n : Nat) (len : Nat) : String :=
lpad (toString n) '0' len
/-- A date (year-month-day). -/
public structure Date where
year : Nat

16
src/lake/Lake/Util/Git.lean
View file

@ -53,6 +53,9 @@ public def cwd : GitRepo := ⟨"."⟩
@[inline] public def dirExists (repo : GitRepo) : BaseIO Bool :=
repo.dir.isDir
@[inline] public def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
captureProc {cmd := "git", args, cwd := repo.dir}
@[inline] public def captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String) :=
captureProc? {cmd := "git", args, cwd := repo.dir}
@ -83,6 +86,11 @@ public def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit :=
public def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev]
public def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
if Git.isFullObjectName rev then return rev
if let some rev ← repo.resolveRevision? rev then return rev
error s!"{repo}: revision not found '{rev}'"
@[inline] public def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) :=
repo.resolveRevision? "HEAD"
@ -91,6 +99,12 @@ public def getHeadRevision (repo : GitRepo) : LogIO String := do
error s!"{repo}: could not resolve 'HEAD' to a commit; \
the repository may be corrupt, so you may need to remove it and try again"
public def getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array String) := do
let args := #["rev-list", "HEAD"]
let args := if n != 0 then args ++ #["-n", toString n] else args
let revs ← repo.captureGit args
return revs.split (· == '\n') |>.toArray
public def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
if Git.isFullObjectName rev then return rev
if let some rev ← repo.resolveRevision? s!"{remote}/{rev}" then return rev
@ -122,7 +136,7 @@ public def getFilteredRemoteUrl?
: BaseIO (Option String) := OptionT.run do Git.filterUrl? (← repo.getRemoteUrl? remote)
public def hasNoDiff (repo : GitRepo) : BaseIO Bool := do
repo.testGit #["diff", "--exit-code"]
repo.testGit #["diff", "HEAD", "--exit-code"]
@[inline] public def hasDiff (repo : GitRepo) : BaseIO Bool := do
not <$> repo.hasNoDiff

13
src/lake/Lake/Util/JsonObject.lean
View file

@ -37,17 +37,20 @@ public instance : ToJson JsonObject := ⟨JsonObject.toJson⟩
public instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩
@[inline] public nonrec def insert [ToJson α] (obj : JsonObject) (prop : String) (val : α) : JsonObject :=
obj.insert prop (toJson val)
public def insertJson (obj : JsonObject) (prop : String) (val : Json) : JsonObject :=
obj.insert prop (toJson val) -- specializes `insert`
@[inline] public def insert [ToJson α] (obj : JsonObject) (prop : String) (val : α) : JsonObject :=
obj.insertJson prop (toJson val)
@[inline] public def insertSome [ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) : JsonObject :=
if let some val := val? then obj.insert prop val else obj
public nonrec def erase (obj : JsonObject) (prop : String) : JsonObject :=
inline <| obj.erase prop
obj.erase prop -- specializes `erase`
@[inline] public def getJson? (obj : JsonObject) (prop : String) : Option Json :=
obj.get? prop
public def getJson? (obj : JsonObject) (prop : String) : Option Json :=
obj.get? prop -- specializes `get?`
@[inline] public def get [FromJson α] (obj : JsonObject) (prop : String) : Except String α :=
match obj.getJson? prop with

10
src/lake/Lake/Util/Log.lean
View file

@ -409,6 +409,16 @@ from an `ELogT` (e.g., `LogIO`).
let log ← getLog
return (a, log.takeFrom iniPos)
/-- If `x` produces any logs, group them into an error block. -/
@[inline] public def throwIfLogs [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] (x : m α) : m α := do
let iniPos ← getLogPos
let a ← x
let endPos ← getLogPos
if iniPos ≠ endPos then
throw iniPos
else
return a
/-- Performs `x` and backtracks any error to the log position before `x`. -/
@[inline] public def withLogErrorPos
[Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] (self : m α)

7
src/lake/Lake/Util/Proc.lean
View file

@ -39,15 +39,18 @@ public def proc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO Unit := d
if out.exitCode ≠ 0 then
error s!"external command '{args.cmd}' exited with code {out.exitCode}"
public def captureProc (args : IO.Process.SpawnArgs) : LogIO String := do
public def captureProc' (args : IO.Process.SpawnArgs) : LogIO (IO.Process.Output) := do
let out ← rawProc args (quiet := true)
if out.exitCode = 0 then
return out.stdout.trim -- remove, e.g., newline at end
return out
else errorWithLog do
logVerbose (mkCmdLog args)
logOutput out logInfo
logError s!"external command '{args.cmd}' exited with code {out.exitCode}"
@[inline] public def captureProc (args : IO.Process.SpawnArgs) : LogIO String := do
return (← captureProc' args).stdout.trim -- remove, e.g., newline at end
public def captureProc? (args : IO.Process.SpawnArgs) : BaseIO (Option String) := do
EIO.catchExceptions (h := fun _ => pure none) do
let out ← IO.Process.output args

17
src/lake/Lake/Util/Reservoir.lean Normal file
View file

@ -0,0 +1,17 @@
/-
Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
module
prelude
public import Init.Prelude
import Init.Data.Array.Basic
namespace Lake
public def Reservoir.lakeHeaders : Array String := #[
"X-Reservoir-Api-Version:1.0.0",
"X-Lake-Registry-Api-Version:0.1.0"
]

35
src/lake/Lake/Util/String.lean Normal file
View file

@ -0,0 +1,35 @@
/-
Copyright (c) 2024 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
module
prelude
public import Init.Data.ToString.Basic
import Init.Data.String.Extra
import Init.Data.Nat.Fold
namespace Lake
public def lpad (s : String) (c : Char) (len : Nat) : String :=
"".pushn c (len - s.length) ++ s
public def rpad (s : String) (c : Char) (len : Nat) : String :=
s.pushn c (len - s.length)
public def zpad (n : Nat) (len : Nat) : String :=
lpad (toString n) '0' len
/-- Returns whether a string is composed of only hexadecimal digits. -/
public def isHex (s : String) : Bool :=
s.utf8ByteSize.all fun i h =>
let c := s.getUtf8Byte ⟨i⟩ h
if c ≤ 57 then -- '9'
48 ≤ c -- '0'
else if c ≤ 102 then -- 'f'
97 ≤ c -- 'a'
else if c ≤ 70 then -- 'F'
65 ≤ c -- 'A'
else
false

138
src/lake/Lake/Util/Url.lean Normal file
View file

@ -0,0 +1,138 @@
/-
Copyright (c) 2022 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
module
prelude
public import Lake.Util.Log
import all Init.Data.String.Extra
import Lake.Util.JsonObject
import Lake.Util.Proc
open Lean
namespace Lake
public def hexEncodeByte (b : UInt8) : Char :=
if b = 0 then '0' else
if b = 1 then '1' else
if b = 2 then '2' else
if b = 3 then '3' else
if b = 4 then '4' else
if b = 5 then '5' else
if b = 6 then '6' else
if b = 7 then '7' else
if b = 8 then '8' else
if b = 9 then '9' else
if b = 0xa then 'A' else
if b = 0xb then 'B' else
if b = 0xc then 'C' else
if b = 0xd then 'D' else
if b = 0xe then 'E' else
if b = 0xf then 'F' else
'*'
/-- Encode a byte as a URI escape code (e.g., `%20`). -/
public def uriEscapeByte (b : UInt8) (s := "") : String :=
s.push '%' |>.push (hexEncodeByte <| b >>> 4) |>.push (hexEncodeByte <| b &&& 0xF)
/-- Folds a monadic function over the UTF-8 bytes of `Char` from most significant to least significant. -/
@[specialize] public def foldlUtf8M [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
let s := init
let v := c.val
if v ≤ 0x7f then
f s v.toUInt8
else if v ≤ 0x7ff then
let s ← f s <| (v >>> 6).toUInt8 &&& 0x1f ||| 0xc0
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
else if v ≤ 0xffff then
let s ← f s <| (v >>> 12).toUInt8 &&& 0x0f ||| 0xe0
let s ← f s <| (v >>> 6).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
else
let s ← f s <| (v >>> 18).toUInt8 &&& 0x07 ||| 0xf0
let s ← f s <| (v >>> 12).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| (v >>> 6).toUInt8 &&& 0x3f ||| 0x80
let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
return s
public abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ :=
Id.run <| foldlUtf8M c (pure <| f · ·) init
example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by
simp only [foldlUtf8, foldlUtf8M]
simp only [String.utf8EncodeChar_eq_utf8EncodeCharFast, String.utf8EncodeCharFast]
if h1 : c.val ≤ 0x7f then simp [h1]
else if h2 : c.val ≤ 0x7ff then simp [h1, h2]
else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3]
else simp [h1, h2, h3]
/-- Encode a character as a sequence of URI escape codes representing its UTF8 encoding. -/
public def uriEscapeChar (c : Char) (s := "") : String :=
foldlUtf8 c (init := s) fun s b => uriEscapeByte b s
/--
A URI unreserved mark as specified in [RFC3986][2].
Unlike the older [RFC2396][1], RFC2396 also reserves `!`, `*`, `'`, `(`, and `)`.
Lake uses RFC3986 here because the `curl` implementation of AWS Sigv4
that Lake uses to upload artifacts requires these additional characters to be escaped.
[1]: https://datatracker.ietf.org/doc/html/rfc2396#section-2.3
[2]: https://datatracker.ietf.org/doc/html/rfc3986#section-2.3
-/
public def isUriUnreservedMark (c : Char) : Bool :=
c matches '-' | '_' | '.' | '~'
/-- Encodes anything but a URI unreserved character as a URI escape sequences. -/
public def uriEncodeChar (c : Char) (s := "") : String :=
if c.isAlphanum || isUriUnreservedMark c then
s.push c
else
uriEscapeChar c s
/-- Encodes a string as an ASCII URI component, escaping special characters (and unicode). -/
public def uriEncode (s : String) : String :=
s.foldl (init := "") fun s c => uriEncodeChar c s
/--
Performs a HTTP `GET` request of a URL (using `curl` with JSON output) and, if successful,
return the body. Otherwise, returns `none` on a 404 and errors on anything else.
-/
public def getUrl?
(url : String) (headers : Array String := #[])
: LogIO (Option String) := withLogErrorPos do
let args := #[
"-s", "-L", "-w", "%{stderr}%{json}\n",
"--retry", "3" -- intermittent network errors can occur
]
let args := headers.foldl (init := args) (· ++ #["-H", ·])
let out ← captureProc' {cmd := "curl", args := args.push url}
match Json.parse out.stderr >>= JsonObject.fromJson? with
| .ok data =>
let code ← id do
match (data.get? "response_code" <|> data.get? "http_code") with
| .ok (some code) => return code
| .ok none => error s!"curl's JSON output did not contain a response code"
| .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}"
if code == 200 then
return some out.stdout.trim
else if code == 404 then
return none
else
error s!"failed to GET URL, error {code}"
| .error e =>
error s!"curl produced invalid JSON output: {e}"
/-- Perform a HTTP `GET` request of a URL (using `curl`) and return the body. -/
public def getUrl (url : String) (headers : Array String := #[]) : LogIO String := do
let args := #[
"-s", "-L",
"--retry", "3" -- intermittent network errors can occur
]
let args := headers.foldl (init := args) (· ++ #["-H", ·])
captureProc {cmd := "curl", args := args.push url}

3
src/lake/Makefile
View file

@ -58,6 +58,9 @@ check-lake:
tests/%.test:
cd tests/$* && ./test.sh
tests/%.online-test:
cd tests/$* && ./online-test.sh
tests/%.clean:
cd tests/$* && ./clean.sh || true

2
src/lake/tests/cache/clean.sh vendored
View file

@ -1 +1 @@
rm -rf .lake lake-manifest.json produced.out Ignored.lean
rm -rf .lake lake-manifest.json produced.out Ignored.lean .git

6
src/lake/tests/cache/non-reservoir.toml vendored Normal file
View file

@ -0,0 +1,6 @@
name = "test"
# Example non-Reservoir dependency
[[require]]
name = "hello"
path = "../../examples/hello"

129
src/lake/tests/cache/online-test.sh vendored Executable file
View file

@ -0,0 +1,129 @@
#!/usr/bin/env bash
source ../common.sh
./clean.sh
# Test the functionality of the Reservoir (or other remote) cache
# Check necessary environment variables art set
if [ -z "${LAKE_CACHE_KEY:-}" ]; then
echo "Must be run with LAKE_CACHE_KEY set"
exit 1
fi
if [ -z "${TEST_ENDPOINT:-}" ]; then
echo "Must be run with TEST_ENDPOINT set"
exit 1
fi
TEST_ARTIFACT_ENDPOINT="${TEST_ARTIFACT_ENDPOINT:-$TEST_ENDPOINT/a0}"
TEST_REVISION_ENDPOINT="${TEST_REVISION_ENDPOINT:-$TEST_ENDPOINT/r0}"
TEST_CDN_ENDPOINT="${TEST_CDN_ENDPOINT:-https://reservoir.lean-cache.cloud}"
TEST_CDN_ARTIFACT_ENDPOINT="${TEST_CDN_ARTIFACT_ENDPOINT:-$TEST_CDN_ENDPOINT/a0}"
TEST_CDN_REVISION_ENDPOINT="${TEST_CDN_REVISION_ENDPOINT:-$TEST_CDN_ENDPOINT/r0}"
TEST_RESERVOIR_URL="${TEST_RESERVOIR_URL:-https://reservoir.lean-lang.org}"
export RESERVOIR_API_URL="$TEST_RESERVOIR_URL/api/v0"
with_upload_endpoints() {
LAKE_CACHE_ARTIFACT_ENDPOINT="$TEST_ARTIFACT_ENDPOINT" \
LAKE_CACHE_REVISION_ENDPOINT="$TEST_REVISION_ENDPOINT" \
"$@"
}
with_cdn_endpoints() {
LAKE_CACHE_ARTIFACT_ENDPOINT="$TEST_CDN_ARTIFACT_ENDPOINT" \
LAKE_CACHE_REVISION_ENDPOINT="$TEST_CDN_REVISION_ENDPOINT" \
"$@"
}
# Since committing a Git repository to a Git repository is not well-supported,
# We reinitialize the repository on each test.
init_git
# Store Lake cache in a local directory
TEST_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)"
export LAKE_CACHE_DIR="$TEST_DIR/.lake/cache"
echo "# TESTS"
# Test `cache get` command errors for bad configurations
with_cdn_endpoints test_err 'the `--scope` option must be set' cache get
LAKE_CACHE_ARTIFACT_ENDPOINT=bogus test_err 'both environment variables must be set' cache get
LAKE_CACHE_REVISION_ENDPOINT=bogus test_err 'both environment variables must be set' cache get
# Test `cache put` command errors for bad configurations
test_err 'the `--scope` option must be set' cache put bogus.jsonl
test_err 'these environment variables must be set' \
cache put bogus.jsonl --scope='!/bogus'
LAKE_CACHE_KEY= test_err 'these environment variables must be set' \
cache put bogus.jsonl --scope='!/bogus'
LAKE_CACHE_REVISION_ENDPOINT=bogus test_err 'these environment variables must be set' \
cache put bogus.jsonl --scope='!/bogus'
LAKE_CACHE_REVISION_ENDPOINT=bogus test_err 'these environment variables must be set' \
cache put bogus.jsonl --scope='!/bogus'
# Test revision failure
REV=$(git rev-parse HEAD)
test_err "revision not found" cache get --scope='!/bogus' --rev='bogus'
test_err "outputs not found for revision" cache get --scope='!/bogus' --rev=$REV
# Test `cache get` skipping non-Reservoir dependencies
test_run -f non-reservoir.toml update
test_out 'hello: skipping non-Reservoir dependency' -f non-reservoir.toml cache get
# Build artifacts
test_run build +Test -o .lake/outputs.jsonl
test_exp -f .lake/outputs.jsonl
test_cmd_eq 3 wc -l < .lake/outputs.jsonl
test_cmd cp -r .lake/cache .lake/cache-backup
# Test cache put/get with a custom endpoint
with_upload_endpoints test_run cache put .lake/outputs.jsonl --scope='!/test'
test_cmd rm -rf .lake/build "$LAKE_CACHE_DIR"
with_cdn_endpoints test_err 'failed to download some artifacts' \
cache get .lake/outputs.jsonl --scope='!/bogus'
with_cdn_endpoints test_run cache get .lake/outputs.jsonl --scope='!/test'
test_run build +Test --no-build
# Test that outputs and artifacts are not re-downloaded
with_cdn_endpoints test_not_out "downloading" cache get .lake/outputs.jsonl --scope='!/test'
with_cdn_endpoints test_not_out "downloading artifact" cache get --scope='!/test'
with_cdn_endpoints test_not_out "downloading" cache get --scope='!/test'
# Test `--force-download`
with_cdn_endpoints test_out "downloading" cache get --scope='!/test' --force-download
# Test dirty work tree warnings
test_cmd touch Ignored.lean
test_cmd git add -f Ignored.lean
with_upload_endpoints test_err "package has changes" --wfail \
cache put .lake/outputs.jsonl --scope='!/test'
test_err "package has changes" --wfail cache get --scope='!/test'
test_cmd git commit -m "v2"
# Test revision search
test_cmd rm -rf .lake/build "$LAKE_CACHE_DIR"
with_cdn_endpoints test_err "no outputs found" --wfail cache get --scope='!/test' --max-revs=1
with_cdn_endpoints test_run cache get --scope='!/test'
test_run build +Test --no-build
# Test Reservoir download
test_run -f reservoir2.toml update --keep-toolchain
test_out "the artifact cache is not enabled for this package" \
-d .lake/packages/Cli build -o "$TEST_DIR/.lake/cli-outputs.jsonl"
LAKE_ARTIFACT_CACHE=true test_run -d .lake/packages/Cli \
build -o "$TEST_DIR/.lake/cli-outputs.jsonl" --no-build
with_upload_endpoints test_run -d .lake/packages/Cli \
cache put "$TEST_DIR/.lake/cli-outputs.jsonl" --scope "leanprover/lean4-cli"
test_cmd rm -rf .lake/packages/Cli/.lake/build "$LAKE_CACHE_DIR"
test_fails -f reservoir.toml build @Cli --no-build
test_err "failed to download artifacts for some dependencies" \
-f reservoir2.toml cache get --max-revs=1
test_run -f reservoir.toml cache get --max-revs=1
test_run -f reservoir.toml build @Cli --no-build
# Test Reservoir with `--scope`/`--repo` uses GitHub scope
test_cmd rm -rf .lake/cache
test_run -d .lake/packages/Cli cache get --repo=leanprover/lean4-cli --max-revs=1
test_run -d .lake/packages/Cli build --no-build
# Cleanup
rm -rf .git produced.out

7
src/lake/tests/cache/reservoir.toml vendored Normal file
View file

@ -0,0 +1,7 @@
name = "test"
enableArtifactCache = true
# Example package with dependencies on Reservoir
[[require]]
name = "Cli"
scope = "leanprover"

12
src/lake/tests/cache/reservoir2.toml vendored Normal file
View file

@ -0,0 +1,12 @@
name = "test"
enableArtifactCache = true
# Example package with dependencies not in Reservoir's cache
[[require]]
name = "doc-gen4"
scope = "leanprover"
# Example package with dependencies on Reservoir
[[require]]
name = "Cli"
scope = "leanprover"

84
src/lake/tests/cache/test.sh vendored
View file

@ -5,62 +5,60 @@ source ../common.sh
# Test the functionality of the Lake artifact cache
# Store Lake cache in a local directory
TEST_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)"
CACHE_DIR="$TEST_DIR/.lake/cache"
export LAKE_CACHE_DIR="$CACHE_DIR"
# Verify packages without `enableArtifactCache` do not use the cache by default
LAKE_CACHE_DIR="$CACHE_DIR" test_run build -f unset.toml Test:static
test_run build -f unset.toml Test:static
test_exp ! -d "$CACHE_DIR"
# Verify they also do not if `LAKE_ARTIFACT_CACHE` is set to `false`
LAKE_CACHE_DIR="$CACHE_DIR" LAKE_ARTIFACT_CACHE=false \
test_run build -f unset.toml Test:static
LAKE_ARTIFACT_CACHE=false test_run build -f unset.toml Test:static
test_exp ! -d "$CACHE_DIR"
# Verify packages with `enableArtifactCache` set to `false``
# also do not if `LAKE_ARTIFACT_CACHE` is set to `true`
LAKE_CACHE_DIR="$CACHE_DIR" LAKE_ARTIFACT_CACHE=true \
test_run build -f disabled.toml Test:static
LAKE_ARTIFACT_CACHE=true test_run build -f disabled.toml Test:static
test_exp ! -d "$CACHE_DIR"
# Verify that packages without `enableArtifactCache` and
# `LAKE_ARTIFACT_CACHE` is set to `true` do use the cache
LAKE_CACHE_DIR="$CACHE_DIR" LAKE_ARTIFACT_CACHE=true \
test_run build -f unset.toml Test:static
LAKE_ARTIFACT_CACHE=true test_run build -f unset.toml Test:static
test_exp -d "$CACHE_DIR"
./clean.sh
# Ensure a build runs properly with some artifacts cached
LAKE_CACHE_DIR="$CACHE_DIR" test_run build Test:static
LAKE_CACHE_DIR="$CACHE_DIR" test_run build Test:static --no-build --wfail
test_run build Test:static
test_run build Test:static --no-build --wfail
# Test replay of a cached build
LAKE_CACHE_DIR="$CACHE_DIR" test_out 'Replayed Test:c.o' build +Test:o -v
test_out 'Replayed Test:c.o' build +Test:o -v
# Verify that a rebuild with the cache disabled is a no-op
touch .lake/build/ir/Test.c # avoid mod time fallback if trace is missing
LAKE_CACHE_DIR= test_run build +Test:o --no-build --wfail
LAKE_CACHE_DIR= test_run build Test:static --no-build --wfail
test_run -f disabled.toml build +Test:o --no-build --wfail
test_run -f disabled.toml build Test:static --no-build --wfail
# Verify the cache directory structure was created
test_exp -d "$CACHE_DIR"
test_exp -d "$CACHE_DIR/inputs"
test_exp -s "$CACHE_DIR/inputs/test.jsonl"
test_exp -d "$CACHE_DIR/outputs"
test_exp -d "$CACHE_DIR/artifacts"
# Copy the basic inputs for later
cp "$CACHE_DIR/inputs/test.jsonl" .lake/backup-inputs.json
# Copy the basic mappings for later
test_cmd cp -r "$CACHE_DIR/outputs" .lake/backup-outputs
# Checked that the cached artifact is in the expected location
# and equivalent to the standard artifact
local_art="$(LAKE_CACHE_DIR= $LAKE query +Test:o)"
cache_art="$(LAKE_CACHE_DIR="$CACHE_DIR" $LAKE query +Test:o)"
local_art="$($LAKE -f disabled.toml query +Test:o)"
cache_art="$($LAKE query +Test:o)"
test_exp "$(norm_dirname "$cache_art")" = "$CACHE_DIR/artifacts"
test_exp "$cache_art" != "$local_art"
test_cmd cmp -s "$cache_art" "$local_art"
# Verify supported artifacts end up in the cache directory
LAKE_CACHE_DIR="$CACHE_DIR" test_run build test:exe Test:static Test:shared +Test:o.export +Test:o.noexport
test_run build test:exe Test:static Test:shared +Test:o.export +Test:o.noexport
test_cached() {
target="$1"; shift
art="$(LAKE_CACHE_DIR="$CACHE_DIR" $LAKE query $target)"
art="$($LAKE query $target)"
echo "${1:-?} artifact cached: $target -> $art"
test ${1:-} "$(norm_dirname "$art")" = "$CACHE_DIR/artifacts"
}
@ -73,7 +71,7 @@ test_cached +Test:dynlib !
test_cached +Test:olean
test_cached +Test:ilean !
test_cached +Test:c
LAKE_CACHE_DIR="$CACHE_DIR" test_run build +Module
test_run build +Module
test_cached +Module:olean
test_cached +Module:olean.server
test_cached +Module:olean.private
@ -83,52 +81,58 @@ test_cached +Module:ir
check_diff /dev/null <(ls -1 "$CACHE_DIR/*.hash" 2>/dev/null)
# Verify that the executable has the right permissions to be run
LAKE_CACHE_DIR="$CACHE_DIR" test_run exe test
test_run exe test
# Verify that fetching from the cache creates a trace file that does not replay
touch Ignored.lean
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Fetched Ignored" -v build +Ignored
test_out "Fetched Ignored" -v build +Ignored
test_exp -f .lake/build/lib/lean/Ignored.trace
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Fetched Ignored" -v build +Ignored
test_out "Fetched Ignored" -v build +Ignored
# Verify that modifications invalidate the cache
echo "def foo := ()" > Ignored.lean
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Built Ignored" -v build +Ignored
test_out "Built Ignored" -v build +Ignored
# Verify module ileans are restored from the cache
LAKE_CACHE_DIR="$CACHE_DIR" test_run build +Test --no-build
test_run build +Test --no-build
test_cmd rm .lake/build/lib/lean/Test.ilean
LAKE_CACHE_DIR="$CACHE_DIR" test_out "restored artifact from cache" -v build +Test --no-build
test_out "restored artifact from cache" -v build +Test --no-build
test_exp -f .lake/build/lib/lean/Test.ilean
# Verify that things work properly if the cached artifact is removed
test_cmd rm "$cache_art"
LAKE_CACHE_DIR="$CACHE_DIR" test_out "⚠ [4/4] Replayed Test:c.o" build +Test:o -v --no-build
test_out "⚠ [4/4] Replayed Test:c.o" build +Test:o -v --no-build
test_exp -f "$cache_art" # artifact should be re-cached
test_cmd rm "$CACHE_DIR/inputs/test.jsonl"
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Replayed Test:c.o" build +Test:o -v --no-build
test_cmd rm -r "$CACHE_DIR/outputs"
test_out "Replayed Test:c.o" build +Test:o -v --no-build
test_exp -f "$cache_art" # artifact should be re-cached
# Verify that the upstream input graph is restored
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Replayed Test:c.o" build Test:static -v --no-build
# Input order is not deterministic due to parallelism, so sorting is necessary
check_diff <(sort .lake/backup-inputs.json) <(sort "$CACHE_DIR/inputs/test.jsonl")
# Verify that upstream cache mappings are restored
test_out "Replayed Test:c.o" build Test:static -v --no-build
check_diff <(ls .lake/backup-outputs) <(ls "$CACHE_DIR/outputs")
# Verify that things work properly if the local artifact is removed
test_cmd rm "$local_art"
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Replayed Test:c.o" build +Test:o -v --no-build
test_out "Replayed Test:c.o" build +Test:o -v --no-build
test_cmd rm "$local_art.trace"
LAKE_CACHE_DIR="$CACHE_DIR" test_out "Fetched Test:c.o" build +Test:o -v --no-build
test_out "Fetched Test:c.o" build +Test:o -v --no-build
# Verify that if the input cache is missing,
# the cached artifact is still used via the output hash in the trace
test_cmd rm "$CACHE_DIR/inputs/test.jsonl" .lake/build/ir/Test.c
LAKE_CACHE_DIR="$CACHE_DIR" test_run -v build +Test:c --no-build
test_cmd rm -r "$CACHE_DIR/outputs" .lake/build/ir/Test.c
test_run -v build +Test:c --no-build
# Verify that the olean does need to be present in the build directory
test_cmd rm .lake/build/lib/lean/Test.olean .lake/build/lib/lean/Test/Imported.olean
LAKE_CACHE_DIR="$CACHE_DIR" test_run -v build +Test.Imported --no-build --wfail
LAKE_CACHE_DIR="$CACHE_DIR" test_run -v build +Test
test_run -v build +Test.Imported --no-build --wfail
test_run -v build +Test
# Test producing an output mappings file
test_run build Test -o .lake/outputs.jsonl
test_exp -f .lake/outputs.jsonl
test_cmd_eq 3 wc -l < .lake/outputs.jsonl
test_run build Test:static -o .lake/outputs.jsonl
test_cmd_eq 6 wc -l < .lake/outputs.jsonl
# Cleanup
rm -f produced.out Ignored.lean

12
src/lake/tests/common.sh
View file

@ -38,6 +38,18 @@ else
norm_dirname() { dirname -- "$1"; }
fi
init_git() {
echo "# initialize test repository"
set -x
git init
git checkout -b master
git config user.name test
git config user.email test@example.com
git add --all
git commit -m "initial commit"
set +x
}
# Test functions
test_cmd() {

6
src/lake/tests/env/test.sh vendored
View file

@ -24,12 +24,14 @@ test_out "hello" -d ../../examples/hello env printenv LEAN_PATH
test_out "lake" env printenv LEAN_SRC_PATH
test_out "hello" -d ../../examples/hello env printenv LEAN_SRC_PATH
test_out "hello" -d ../../examples/hello env printenv PATH
LAKE_CACHE_DIR= test_out "hello" -d ../../examples/hello env printenv PATH
# Test other variables are set
test_eq "false" env printenv LAKE_NO_CACHE
test_eq "false" env printenv LAKE_ARTIFACT_CACHE
# No cache directory is available in Windows CI (i.e., Windows Server)
# test_run env printenv LAKE_CACHE_DIR
# Test that a workspace always sets the cache directory
LAKE_CACHE_DIR= test_run env -d ../../examples/hello env printenv LAKE_CACHE_DIR
# Test that `env` preserves the input environment for certain variables
echo "# TEST: Setting variables for lake env"

4
src/lake/tests/trace/test.sh
View file

@ -18,7 +18,9 @@ test_run build --no-build
# Tests that Lake accepts pure numerical traces
if command -v jq > /dev/null; then # skip if no jq found
jq -r '.depHash' .lake/build/lib/lean/Foo.trace > .lake/build/lib/lean/Foo.trace.hash
test_cmd mv .lake/build/lib/lean/Foo.trace.hash .lake/build/lib/lean/Foo.trace
test_cmd cat .lake/build/lib/lean/Foo.trace.hash
perl -le "print hex('$(cat .lake/build/lib/lean/Foo.trace.hash)')" > .lake/build/lib/lean/Foo.trace
test_cmd cat .lake/build/lib/lean/Foo.trace
test_run build --no-build
fi

2
src/shell/CMakeLists.txt
View file

@ -197,7 +197,7 @@ ENDFOREACH(T)
# toolchain: requires elan to download toolchain
# online: downloads remote repositories
file(GLOB_RECURSE LEANLAKETESTS
"${LEAN_SOURCE_DIR}/lake/tests/test.sh"
#"${LEAN_SOURCE_DIR}/lake/tests/test.sh"
"${LEAN_SOURCE_DIR}/lake/examples/test.sh")
FOREACH(T ${LEANLAKETESTS})
if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")