lake and replay (on nightly-2024-05-24)

Stream: lean4

[Mauricio Collares]

I've been using a nightly to be able to use the new incremental tactic processing improvements, so I am not sure this happens on v4.8.0-rc2. More than once, I've been hit with a strange lake bug. In the example below, I made a bad edit to a file upstream of Mathlib.Algebra.Group.Commute.Defs, which caused a compilation error (via LSP). I then reverted the upstream change, and the following happened:

$ lake build Mathlib.Algebra.Group.Commute.Defs
✖ [58/58] Replaying Mathlib.Algebra.Group.Commute.Defs
trace: [...command-line junk here...]
error: ././././Mathlib/Algebra/Group/Commute/Defs.lean:280:37: failed to synthesize
 One ℕ
Some builds logged failures:
- Mathlib.Algebra.Group.Commute.Defs
error: build failed
$ rm -r .lake/build/ir/Mathlib/Algebra/Group/Commute .lake/build/lib/Mathlib/Algebra/Group/Commute
$ lake build Mathlib.Algebra.Group.Commute.Defs
Build completed successfully.

Is that something that has been fixed in a more recent nightly? Does lake invalidate its replay cache properly even when taking into account files with outdated dependencies processed by the LSP server?

[Sebastian Ullrich]

That sounds like lean#4303

[Mauricio Collares]

The .trace file is the same before and after, it just seems like lake replays the .log.json file whenever it exists (and it doesn't get deleted when it should, sometimes). Example:

$ lake build Mathlib.Data.Nat.Cast.Defs
✖ [54/54] Replaying Mathlib.Data.Nat.Cast.Defs
[...bla bla...]
error: ././././Mathlib/Data/Nat/Cast/Defs.lean:202:51: failed to synthesize instance
 One ℕ
error: Lean exited with code 1
Some builds logged failures:
- Mathlib.Data.Nat.Cast.Defs
error: build failed
$ cat .lake/build/lib/Mathlib/Data/Nat/Cast/Defs.log.json
[...the same output as above, but in json format...]
$ cat .lake/build/lib/Mathlib/Data/Nat/Cast/Defs.trace
14484521835112575365
$ rm .lake/build/lib/Mathlib/Data/Nat/Cast/Defs.log.json
$ lake build Mathlib.Data.Nat.Cast.Defs
Build completed successfully.
$ cat .lake/build/lib/Mathlib/Data/Nat/Cast/Defs.trace
14484521835112575365

[Mauricio Collares]

Sebastian Ullrich said:

That sounds like lean#4303

Ah, that looks like it. Thanks! I will add my comment there.