Changelog

leanprover/lean4 · · 2 commits

Lake config recovery gets more robust

Lake now flushes config traces before truncation and falls back to reconfiguration when the trace is unreadable or invalid.

Recover from interrupted config writes (kim-em357167b)

Lake now flushes the compiled-configuration trace before truncating the file and starting the slower elaboration step. That closes a window where an interrupted lake process could leave behind a zero-length placeholder, making later runs unrecoverable.

Reconfigure on unparsable config traces (kim-emecf55de)

If Lake can’t parse the saved configuration trace, it now treats that the same as a stale or missing trace and reconfigures automatically instead of aborting with an error. This makes startup more resilient when the trace is corrupted or partially written.

Other misc changes

  • None.