From eb432cd3b71f0ffbc817e2e124a06df62d12fbbb Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 19 Dec 2023 16:29:41 -0500
Subject: [PATCH] fix: lake: save config trace before elab (#3069)

Lake will now delete any old `.olean` and save the new trace before
elaborating a configuration file. This will enable the automatic
reconfiguration of the file if elaboration fails.

Fixes an issue that was [discussed on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Invalid.20lake.20configuration/near/406717198).
---
 src/lake/Lake/Load/Elab.lean | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean
index a2ca6e8f6d79..01f334dfb01a 100644
--- a/src/lake/Lake/Load/Elab.lean
+++ b/src/lake/Lake/Load/Elab.lean
@@ -210,11 +210,25 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
     h.unlock
     return env
   | .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
+    /-
+    NOTE: We write the trace before elaborating the configuration file
+    to enable automatic reconfiguration on the next `lake` invocation if
+    elaboration fails. To ensure a failure triggers a reconfigure, we must also
+    remove any previous out-of-date `.olean`. Otherwise, Lake will treat the
+    older `.olean` as matching the new trace.
+    -/
+    match (← IO.FS.removeFile olean |>.toBaseIO) with
+    | .ok _ | .error (.noFileOrDirectory ..) =>
+      h.putStrLn <| Json.pretty <| toJson
+        {platform := platformDescriptor, leanHash := Lean.githash,
+          configHash, options := lakeOpts : ConfigTrace}
+      h.truncate
+      let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
+      Lean.writeModule env olean
+      h.unlock
+      return env
+    | .error e =>
+      logError <| toString e
+      h.unlock
+      IO.FS.removeFile traceFile
+      failure