Skip to content

Commit

Permalink
fix: lake: save config trace before elab (#3069)
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
tydeu authored Dec 19, 2023
1 parent 312ea12 commit eb432cd
Showing 1 changed file with 22 additions and 8 deletions.
30 changes: 22 additions & 8 deletions src/lake/Lake/Load/Elab.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit eb432cd

Please sign in to comment.