lake build failure

Stream: general

[Julian Berman]

This isn't a full bug report/reproducer clearly, but I found again when updating to 4.8.0-rc1 and rebuilding mathlib4 that lake build produced obscure output and fails (repeatedly), necessitating an rm -r .lake, at which point now it appears to be running fine. Here's the output I got from updating to 4.8.0-rc1 and then running lake build in my Mathlib4 repository which I haven't built in around a month. Including the first 15 and last 15 lines and then the full file below as Zulip seems unhappy with the length:

⊙  caffeinate -i lake build                                                                                                                                                                                                                                                     julian@Mini
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: updating repository '././.lake/packages/Qq' to revision '53156671405fbbd5402ed17a79bd129b961bd8d6'
info: aesop: updating repository '././.lake/packages/aesop' to revision '2225b0e4a3528da20499e2304b521e0c4c2a4563'
info: proofwidgets: updating repository '././.lake/packages/proofwidgets' to revision 'e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5'
info: Cli: updating repository '././.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
info: importGraph: updating repository '././.lake/packages/importGraph' to revision 'c46d22bbe4f8363c0829ce0eb48a95012cdc0d79'
[279/4462] Building Aesop.RuleSet.Filter
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/packages/aesop/.lake/build/lib /opt/homebrew/Cellar/lean/4.8.0-rc1/bin/lean ././.lake/packages/aesop/././Aesop/RuleSet/Filter.lean -R ././.lake/packages/aesop/./. -o ././.lake/packages/aesop/.lake/build/lib/Aesop/RuleSet/Filter.olean -i ././.lake/packages/aesop/.lake/build/lib/Aesop/RuleSet/Filter.ilean -c ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleSet/Filter.c --json
error: ././.lake/packages/aesop/././Aesop/RuleSet/Filter.lean:69:18-69:33: failed to synthesize instance
  BEq RuleSetName
error: Lean exited with code 1
[287/4462] Building Aesop.Builder.Apply
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/packages/aesop/.lake/build/lib /opt/homebrew/Cellar/lean/4.8.0-rc1/bin/lean ././.lake/packages/aesop/././Aesop/Builder/Apply.lean -R ././.lake/packages/aesop/./. -o ././.lake/packages/aesop/.lake/build/lib/Aesop/Builder/Apply.olean -i ././.lake/packages/aesop/.lake/build/lib/Aesop/Builder/Apply.ilean -c ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Apply.c --json
error: ././.lake/packages/aesop/././Aesop/Builder/Apply.lean:41:4-41:76: failed to synthesize instance

and last 20:

  Monad ElabM
error: Lean exited with code 1
[295/4462] Building Aesop.Builder.Unfold
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/packages/aesop/.lake/build/lib /opt/homebrew/Cellar/lean/4.8.0-rc1/bin/lean ././.lake/packages/aesop/././Aesop/Builder/Unfold.lean -R ././.lake/packages/aesop/./. -o ././.lake/packages/aesop/.lake/build/lib/Aesop/Builder/Unfold.olean -i ././.lake/packages/aesop/.lake/build/lib/Aesop/Builder/Unfold.ilean -c ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Unfold.c --json
error: ././.lake/packages/aesop/././Aesop/Builder/Unfold.lean:39:2-39:59: failed to synthesize instance
  Pure ElabM
error: ././.lake/packages/aesop/././Aesop/Builder/Unfold.lean:38:2-38:44: failed to synthesize instance
  Bind ElabM
error: ././.lake/packages/aesop/././Aesop/Builder/Unfold.lean:37:2-37:51: failed to synthesize instance
  Bind ElabM
error: Lean exited with code 1
Some build steps logged failures:
- Building Aesop.RuleSet.Filter
- Building Aesop.Builder.Apply
- Building Aesop.Builder.Cases
- Building Aesop.Builder.NormSimp
- Building Aesop.Builder.Tactic
- Building Aesop.Builder.Forward
- Building Aesop.Builder.Unfold
error: build failed

Full output

If there's something I can include in the future that helps diagnose why lake is confused let me know.

[Julian Berman]

A question which is only intended to be the slightest bit leading is "should lake build imply lake clean if the toolchain has changed / mismatches the contents of .lake, which I presume must have some idea of what it was the last time things were built"? It's the case that oleans are pinned to a version right, so is there any reason to be any more clever than "guess I should throw everything away before starting"?

[Kim Morrison]

Yes, I find that I need rm -rf .lake too often when switching toolchains. It would be good to get to the bottom of this. @Mac Malone, do you have any suggestions about how we might obtain a repro for this?

[Mac Malone]

My suggestion is to figure out why those Lean errors are being produced. For example, have those instances changed between the old version and the new version you are updating to? If so, that would imply that Lean/Lake is somehow reusing the old oleans. In that case, it would be useful to know which oleans it is reusing and why (e.g., what are traces, etc.).

[Mac Malone]

From there it may be possible to build a MWE, which would really help with fixing whatever is going wrong here.

[Julian Berman]

My recollection is that the specific errors there are slight red herrings, I'm pretty sure I see something like this nearly each time I upgrade, albeit that's around once a month obviously given the release cycle, but it's definitely not the first time, I knew immediately that blowing away the directory was going to fix it when I saw the error -- anyways I say that because I am fairly sure that the last two times this happened the errors were some other different ones than instance synthesis it was whatever other kind of errors happened -- so I definitely assumed the cause was reusing old oleans, but I don't/didn't know how to answer the "why are they being used" question -- if you have any specific advice for how to debug that (I take it you were teaching me that one of the traces will tell me at least some information there?) them I'm happy to try to poke next month.

[Julian Berman]

Oh maybe I don't even need to wait until then, do I have any other built projects cloned other than Mathlib...

[Julian Berman]

I just upgraded to rc2 and sure enough have the same issue -- removing .lake of course again gets me a working build.
This time before doing so I backed up the directory, so I have a "broken" copy as well still.

[Julian Berman]

Let me know if there's anything I can poke at to diagnose.