diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 20e2c2911a..bf70a5d7ed 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -10,35 +10,23 @@ import Lake.Config.ExternLibConfig import Lake.Config.WorkspaceConfig import Lake.Config.Dependency import Lake.Config.Script +import Lake.Load.Config import Lake.Util.DRBMap import Lake.Util.OrdHashSet -import Lake.Load.Config +import Lake.Util.Platform open System Lean namespace Lake -/-- A string descriptor of the `System.Platform` OS (`windows`, `macOS`, or `linux`). -/ -def osDescriptor : String := - if Platform.isWindows then - "windows" - else if Platform.isOSX then - "macOS" - else - "linux" - /-- -A `tar.gz` file name suffix encoding the the current Platform. -(i.e, `osDescriptor` joined with `System.Platform.numBits`). +Platform-specific archive file with an optional name prefix +(i.e., `{name}-{platformDescriptor}.tar.gz`). -/ -def archiveSuffix := - s!"{osDescriptor}-{Platform.numBits}.tar.gz" - -/-- If `name?`, `{name}-{archiveSuffix}`, otherwise just `archiveSuffix`. -/ def nameToArchive (name? : Option String) : String := match name? with - | none => archiveSuffix - | some name => s!"{name}-{archiveSuffix}" + | none => s!"{platformDescriptor}.tar.gz" + | some name => s!"{name}-{platformDescriptor}.tar.gz" /-- First tries to convert a string into a legal name. diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean index b4ec76233e..a777e35186 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/src/lake/Lake/Load/Elab.lean @@ -7,6 +7,7 @@ import Lean.Elab.Frontend import Lake.DSL.Extensions import Lake.Load.Config import Lake.Build.Trace +import Lake.Util.Platform import Lake.Util.Log namespace Lake @@ -76,51 +77,113 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String) We call it here via `@[extern]` with a mock implementation. -/ @[extern "lean_environment_add"] -private def add (env : Environment) (_ : ConstantInfo) : Environment := env +private opaque addToEnv (env : Environment) (_ : ConstantInfo) : Environment /-- -Import the OLean for the configuration file if `reconfigure` is not set -and an up-to-date one exists (i.e., one newer than the configuration and the -toolchain). Otherwise, elaborate the configuration and save it to the OLean. +Import a configuration `.olean` (e.g., `lakefile.olean`). +Auxiliary definition for `importConfigFile`. -/ -def importConfigFile (wsDir pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) +def importConfigFileCore (olean : FilePath) (leanOpts : Options) : IO Environment := do + /- + We could import the olean together with its imports using one + `importModules` call, but that would mean we pay for a full + `finalizeImports` each time, which is linear in the number of imported + constants and extension entries (in fact, it is paid two more times: when + marking the `Environment` object as multi-threaded, and when releasing + it). As most lakefiles use the same set of imports, we instead construct + an `Environment` for it only once, and then apply the lakefile contents + on top of it like the elaborator would. Thus the non-shared part of the + `Environment` is very small. + -/ + let (mod, _) ← readModuleData olean + let mut env ← importModulesUsingCache mod.imports leanOpts 1024 + -- Apply constants (does not go through the kernel, so order is irrelevant) + env := mod.constants.foldl addToEnv env + /- + Apply extension entries (`PersistentEnvExtension.addEntryFn` is pure and + does not have access to the whole environment, so no dependency worries + here either) + -/ + let extDescrs ← persistentEnvExtensionsRef.get + let extNameIdx ← mkExtNameMap 0 + for (extName, ents) in mod.entries do + if let some entryIdx := extNameIdx.find? extName then + for ent in ents do + env := extDescrs[entryIdx]!.addEntry env ent + return env + +instance : ToJson Hash := ⟨(toJson ·.val)⟩ +instance : FromJson Hash := ⟨((⟨·⟩) <$> fromJson? ·)⟩ + +structure ConfigTrace where + platform : String + leanHash : String + configHash : Hash + options : NameMap String + deriving ToJson, FromJson + +inductive ConfigLock +| olean (h : IO.FS.Handle) +| lean (h : IO.FS.Handle) (lakeOpts : NameMap String) + +/-- +Import the `.olean` for the configuration file if `reconfigure` is not set and +an up-to-date one exists (i.e., one with matching configuration and on the same +toolchain). Otherwise, elaborate the configuration and save it to the `.olean`. +-/ +def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do let some configName := FilePath.mk <$> configFile.fileName | error "invalid configuration file name" let olean := lakeDir / configName.withExtension "olean" - let useOLean ← id do - if reconfigure then return false - let .ok oleanMTime ← getMTime olean |>.toBaseIO | return false - unless oleanMTime > (← getMTime configFile) do return false - let toolchainFile := wsDir / toolchainFileName - let .ok toolchainMTime ← getMTime toolchainFile |>.toBaseIO | return true - return oleanMTime > toolchainMTime - if useOLean then - /- We could import the olean together with its imports using one - `importModules` call, but that would mean we pay for a full - `finalizeImports` each time, which is linear in the number of imported - constants and extension entries (in fact, it is paid two more times: when - marking the `Environment` object as multi-threaded, and when releasing - it). As most lakefiles use the same set of imports, we instead construct - an `Environment` for it only once, and then apply the lakefile contents - on top of it like the elaborator would. Thus the non-shared, part of the - `Environment` is very small. -/ - let (mod, _) ← readModuleData olean - let mut env ← importModulesUsingCache mod.imports leanOpts 1024 - -- Apply constants (does not go through the kernel, so order is irrelevant) - env := mod.constants.foldl add env - -- Apply extension entries (`PersistentEnvExtension.addEntryFn` is pure and - -- does not have access to the whole environment, so no dependency worries - -- here either) - let extDescrs ← persistentEnvExtensionsRef.get - let extNameIdx ← mkExtNameMap 0 - for (extName, ents) in mod.entries do - if let some entryIdx := extNameIdx.find? extName then - for ent in ents do - env := extDescrs[entryIdx]!.addEntry env ent + let traceFile := lakeDir / configName.withExtension "olean.trace" + /- + Remark: To prevent race conditions between the `.olean` and its trace file + (i.e., one process writes a new configuration while another reads an old one + and vice versa), Lake takes opens a single handle on the trace file and + acquires a lock on it. The lock is held while the lock data is read and + the olean is either imported or a new one is written with new lock data. + -/ + let configHash ← computeTextFileHash configFile + let configLock : ConfigLock ← id do + let validateTrace h : IO ConfigLock := id do + if reconfigure then + h.lock; return .lean h lakeOpts + h.lock (exclusive := false) + let contents ← h.readToEnd; h.rewind + let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson? + | error "compiled configuration is invalid; run with `-R` to reconfigure" + let upToDate := trace.platform = platformDescriptor ∧ + trace.leanHash = Lean.githash ∧ trace.configHash = configHash + if upToDate then + return .olean h + else + -- Upgrade to an exclusive lock + let lockFile := lakeDir / configName.withExtension "olean.lock" + let hLock ← IO.FS.Handle.mk lockFile .write + hLock.lock; h.unlock; h.lock; hLock.unlock + return .lean h trace.options + if (← traceFile.pathExists) then + validateTrace <| ← IO.FS.Handle.mk traceFile .readWrite + else + IO.FS.createDirAll lakeDir + match (← IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with + | .ok h => + h.lock; return .lean h lakeOpts + | .error (.alreadyExists ..) => + validateTrace <| ← IO.FS.Handle.mk traceFile .readWrite + | .error e => error e.toString + match configLock with + | .olean h => + let env ← importConfigFileCore olean leanOpts + h.unlock return env - else - IO.FS.createDirAll lakeDir + | .lean h lakeOpts => let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile Lean.writeModule env olean + h.putStrLn <| Json.pretty <| toJson + {platform := platformDescriptor, leanHash := Lean.githash, + configHash, options := lakeOpts : ConfigTrace} + h.truncate + h.unlock return env diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index a92c61cba0..d690610cf8 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -34,7 +34,7 @@ def MaterializedDep.loadPackage (dep : MaterializedDep) (wsDir : FilePath) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do let dir := wsDir / dep.relPkgDir let lakeDir := dir / defaultLakeDir - let configEnv ← importConfigFile wsDir dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure + let configEnv ← importConfigFile dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts return { dir @@ -51,7 +51,7 @@ Does not resolve dependencies. def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do Lean.searchPathRef.set config.env.leanSearchPath let configEnv ← importConfigFile - config.rootDir config.rootDir (config.rootDir / defaultLakeDir) + config.rootDir (config.rootDir / defaultLakeDir) config.configOpts config.leanOpts config.configFile config.reconfigure let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts let root := { diff --git a/src/lake/Lake/Util/Platform.lean b/src/lake/Lake/Util/Platform.lean new file mode 100644 index 0000000000..3dcf04aa02 --- /dev/null +++ b/src/lake/Lake/Util/Platform.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone +-/ + +namespace Lake + +/-- +A string descriptor of the `System.Platform` OS +(i.e., `windows`, `macOS`, `emscripten`, or `linux`). +-/ +def platformOs : String := + if System.Platform.isWindows then + "windows" + else if System.Platform.isOSX then + "macOS" + else if System.Platform.isEmscripten then + "emscripten" + else + "linux" + +/- A string descriptor of the current `System.Platform` -- OS and bit-width. -/ +def platformDescriptor := + s!"{platformOs}-{System.Platform.numBits}"