fix: stricter lakefile.olean compatibility check

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.

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

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 := {

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}"