diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index f81621957c..afedb4dd8b 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -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 diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean index 942bf5a97f..990cf08deb 100644 --- a/src/lake/Lake/Build/Context.lean +++ b/src/lake/Lake/Build/Context.lean @@ -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. diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 94a4fbfc91..047e1b5783 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -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 := diff --git a/src/lake/Lake/Build/ModuleArtifacts.lean b/src/lake/Lake/Build/ModuleArtifacts.lean index 2ce22546cb..fdd696794a 100644 --- a/src/lake/Lake/Build/ModuleArtifacts.lean +++ b/src/lake/Lake/Build/ModuleArtifacts.lean @@ -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) diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 55c84183a3..14ad348235 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -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 diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 6bec819607..98211978e6 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -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 diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 1e31f57b26..ca65a9ae59 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -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?⟩ diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index cf3fbe6438..c431aa7c9b 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -36,6 +36,7 @@ COMMANDS: pack pack build artifacts into an archive for distribution unpack unpack build artifacts from an distributed archive upload 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