Problems when updating Lean

Stream: lean4

[Mac]

So I was attempting to update Lake to latest Lean version today (I had not done so since the 07-28 nightly) and ran into some challenges:

• Updating to the 08-04 nightly works fine
• Updating to the 08-05 nightly (the zero-cost oleans feature) or future versions causes the basic hello world package to hang/segfault consistently when building. Surprisingly, it does not, however, cause the bootstrap package (or many of the others) to segfault.
• Updating to the 08-12 nightly adds no new problems
• Updating to the 08-13 nightly or future versions causes Lake to experience major performance degradation due to a very long startup time. To give an idea of the time scale: before this nightly, building Lake with Lake was faster than building with make (lake: ~21s vs make: ~29s); after this nightly, make is faster (make: ~29s vs lake: ~50s).

I have no idea why the 08-05 nightly causes the hello world package to segfault. I do have a guess for the 08-13 problem, though. It may come from the parser changes in #589 which may be slowing down Lake's parsing of the package configuration files. @Sebastian Ullrich, does that sound possible and, if so, is there a way for me to fix this?

[Sebastian Ullrich]

I don't see how at least

[Mac]

@Sebastian Ullrich Then, do you have any other ideas as to what could be causing the performance problems in the 08-13 nightly? Or, for that matter, the segfault in 08-05 nightly?

[Mac]

I am kind of at a loss here as to what broke.

[Sebastian Ullrich]

Trying to guess such things is hard, that's where debuggers and profilers come in

[Sebastian Ullrich]

I suppose I should try to build Lake soon anyway... :)

[Mac]

@Sebastian Ullrich True, testing is always better than guessing and the more testing the better. XD

I did some more testing and it appears that the performance issue is, in fact, with 08-12 nightly, not the 08-13 nightly. I could swear that the first time I tested the 08-12 nightly there were no performance issues, but repeated testing seems to have proven otherwise.

[Mac]

Despite the empirical data, this makes much less sense to me as nothing in the 08-12 nightly release notes seems like it should be able to cause the problems I'm observing.

[Mac]

Well, I believe I have figured out the cause of the performance problems! I shut off my cloud sync and the problem disappeared.

I suspect that my cloud sync and Lean/Lake are in some manner competing over access to the oleans and this caused the performance problems. It is still a mystery to me why this only becomes a consistent problem on/after the 08-12 nightly., though.

I also still have not figured out why building the hello package segfaults on/after the 08-05 nightly.

[Patrick Massot]

And I thought that only mathematicians would get the idea to use git and Dropbox on the same folder...

[Sebastian Ullrich]

I have to leave, but I was at least able to confirm the segfault

[Sebastian Ullrich]

It's in importModules, perhaps unsurprisingly

[Mac]

@Patrick Massot Fair enough. :laughing: My reasoning tends to be two-fold: 1) I often have private files in my repo dir that I want synced but don't want to commit/push, and 2) Having to select exactly which folders to sync is a pain so I tend to just sync my whole workspace.

[Mac]

Sebastian Ullrich said:

I have to leave, but I was at least able to confirm the segfault

Thanks for the help! My expertise in Lean is not yet to the point that I really understand how to properly debug a Lean program executable.

[Sebastian Ullrich]

Sebastian Ullrich said:

I have to leave, but I was at least able to confirm the segfault

I have to take that back, I can't reproduce it anymore on https://github.com/leanprover/lean4/commit/a0c2142233d92cf85fdbd39238a92d7f558beb43 (the latest compatible commit). I must have accidentally run Lake with a different Lean version in the PATH from what I used to compile Lake, thus a .olean version mismatch.

[Mac]

@Sebastian Ullrich I have updated Lake to the 08-16 nightly and pushed it. The hello example still segfaults for me. Could you test (when you have the time) if it segfaults for you?

[Sebastian Ullrich]

Thanks, I will try again. Did you make sure it's using the correct stdlib?

[Sebastian Ullrich]

I suppose elan really should ensure that

[Mac]

My default toolchain is the 08-16 nightly and the workspace is also using that, so it should be. Oops, I apparently had set an override a long time ago in that dir.

[Mac]

Removing that fixed it. Sorry for all the trouble!

[Mac]

It seems like I really can't wait for #632. The amount of trouble I have managed to cause myself without that is amazing... XD