Skip to content

Commit

Permalink
fix: lake: re-elab if config olean is missing (#3036)
Browse files Browse the repository at this point in the history
If a user deleted `lakefile.olean` manually without deleting
`lakefile.olean.lock`, Lake would still attempt to load it and thus
produce an error. Now it should properly re-elaborate the configuration
file.
  • Loading branch information
tydeu authored Dec 13, 2023
1 parent d4dca3b commit 2f216b5
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/lake/Lake/Load/Elab.lean
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,8 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
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 ∧
let upToDate :=
(← olean.pathExists) ∧ trace.platform = platformDescriptor ∧
trace.leanHash = Lean.githash ∧ trace.configHash = configHash
if upToDate then
return .olean h
Expand Down

0 comments on commit 2f216b5

Please sign in to comment.