Zulip Chat Archive

Stream: new members

Topic: startup speed


view this post on Zulip Scott Olson (Sep 29 2018 at 20:31):

Is it normal for Lean to take several minutes to catch up when I freshly open my project in VSCode, even if I've completely precompiled the mathlib dependency to .olean files?

view this post on Zulip Scott Olson (Sep 29 2018 at 20:32):

Maybe not several minutes, but at least around 1 minute

view this post on Zulip Scott Olson (Sep 29 2018 at 20:32):

And once it's caught up it seems to spend a significant amount of time after that "checking import for sorry" every time

view this post on Zulip Reid Barton (Sep 29 2018 at 20:40):

I use emacs but it doesn't sound normal. How did you build the mathlib dependency?

view this post on Zulip Reid Barton (Sep 29 2018 at 20:41):

leanpkg build in your project should help. leanpkg build inside _target/deps/mathlib will confuse lean and lead to this kind of behavior

view this post on Zulip Scott Olson (Sep 29 2018 at 20:45):

Oh, interesting. I ended up doing the latter because the former wouldn't actually build mathlib at all

view this post on Zulip Scott Olson (Sep 29 2018 at 20:45):

So I probably need to go back and debug what caused the original problem instead

view this post on Zulip Patrick Massot (Sep 29 2018 at 20:47):

If you really want to make sure all of mathlib is built, even the pieces not currently needed in your project, you need do do lean --make inside _targets/deps/mathlib, not leanpkg build

view this post on Zulip Reid Barton (Sep 29 2018 at 20:48):

The original problem is just that lean is "smart" and only compiles the parts of the dependencies that are actually needed--which is annoying if that subset might increase in the future and you'd rather just build it once and be done with it.

view this post on Zulip Scott Olson (Sep 29 2018 at 20:48):

I thought it might be something like that but I wasn't sure how to get around it, thanks!

view this post on Zulip Scott Olson (Sep 29 2018 at 20:49):

Do I need to "undo" the leanpkg build I did inside _target/deps/mathlib somehow, or just run the correct command now?

view this post on Zulip Patrick Massot (Sep 29 2018 at 20:51):

running the correct command should be enough

view this post on Zulip Scott Olson (Sep 29 2018 at 20:57):

How exactly does Lean get confused here - do the .olean files mark themselves in some way, so that my project would not recognize the .olean files I previously built as its own? I'm scanning for hidden files or some other way it would possibly distinguish and finding nothing so far

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 20:57):

What OS are you using?

view this post on Zulip Scott Olson (Sep 29 2018 at 20:57):

Windows 10

view this post on Zulip Scott Olson (Sep 29 2018 at 20:58):

I run linux as well but haven't checked if I get the same behavior there yet

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 20:58):

Sebastian was saying the other day that sometimes Windows, or maybe some standard anti-virus, goes through the files and maybe randomly touches them messing up "last updated" times. I think Lean tries to recompile an olean file if it thinks that the lean file was modified after the olean file was built, and maybe it gets confused on Windows? I don't use this OS though and this is all second hand.

view this post on Zulip Reid Barton (Sep 29 2018 at 20:59):

I think it has something to do with the leanpkg.path file, but I don't know exactly what

view this post on Zulip Scott Olson (Sep 29 2018 at 20:59):

I'll keep an eye on the last updated times

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 20:59):

Sebastian was saying this in an attempt to explain why leanpkg regularly takes 10 seconds to start running on windows

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 20:59):

despite core lean shipping with the olean files

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 21:00):

(leanpkg is written in lean)

view this post on Zulip Scott Olson (Sep 29 2018 at 21:00):

I haven't had that trouble with leanpkg startup times. I installed it via elan if it makes a difference

view this post on Zulip Scott Olson (Sep 29 2018 at 21:01):

but perhaps I just don't have an AV that causes that specific problem

view this post on Zulip Scott Olson (Sep 29 2018 at 21:02):

I can confirm leanpkg build in the correct directory solved the problem for me, thanks all

view this post on Zulip Scott Olson (Sep 29 2018 at 21:03):

My problem before was misinterpreting the docs I was reading and assuming it would build all of mathlib, but I was running it before adding any imports so it actually built none of it

view this post on Zulip Scott Olson (Sep 29 2018 at 21:06):

Incidentally this solved another problem I had where VSCode's lean.exe would rise to over 2GiB of RAM during the initial build and never drop back down. Apparently it doesn't get as high when the precompiled stuff is available

view this post on Zulip Reid Barton (Sep 29 2018 at 21:13):

Oh--does your mathlib dependency specify a different version of lean than your top-level project, by any chance?

view this post on Zulip Scott Olson (Sep 29 2018 at 21:35):

Oh yeah, that would probably cause the .olean incompatibility by itself. mathlib's toml says 3.4.1 but I'm using a recently nightly in my project, because if I used 3.4.1 it checks out the lean-3.4.1 branch of mathlib and I wanted master

view this post on Zulip Scott Olson (Sep 29 2018 at 21:36):

This is probably a problem for even running lean --make inside the mathlib dir, right?

view this post on Zulip Scott Olson (Sep 29 2018 at 21:40):

I did just run lean --make earlier and we can see the olean version difference:

$ head -c 60 src/regular.olean | xxd
00000000: 6f6c 6561 6e66 696c 6500 332e 342e 322c  oleanfile.3.4.2,
00000010: 206e 6967 6874 6c79 2d32 3031 382d 3038   nightly-2018-08
00000020: 2d32 332c 2063 6f6d 6d69 7420 6231 3361  -23, commit b13a
00000030: 6331 3237 6664 3833 00ff d828            c127fd83...(

$ head -c 60 _target/deps/mathlib/data/nat/basic.olean | xxd
00000000: 6f6c 6561 6e66 696c 6500 332e 342e 312c  oleanfile.3.4.1,
00000010: 2063 6f6d 6d69 7420 3137 6665 3364 6563   commit 17fe3dec
00000020: 6166 3861 00ff f2e4 59f1 0004 0002 696e  af8a....Y.....in
00000030: 6974 0000 0402 6c6f 6769 6300            it....logic.

view this post on Zulip Reid Barton (Sep 29 2018 at 21:43):

This is probably a problem for even running lean --make inside the mathlib dir, right?

Yes if you already ran leanpkg build which created the leanpkg.path file there.

view this post on Zulip Reid Barton (Sep 29 2018 at 21:43):

Or wait.

view this post on Zulip Reid Barton (Sep 29 2018 at 21:44):

Actually I guess it is a question of elan.

view this post on Zulip Scott Olson (Sep 29 2018 at 21:44):

Yeah, elan will automatically download and build with whatever version the toml specifies

view this post on Zulip Scott Olson (Sep 29 2018 at 21:45):

I can probably do the mathlib dir manual lean --make by telling elan which specific version to build with, which seems fair to me for an optional manual step

view this post on Zulip Reid Barton (Sep 29 2018 at 21:45):

I guess the lean --make _target/deps/mathlib instructions are safer in this particular situation then, assuming that elan uses the current working directory to start its search for the toml file

view this post on Zulip Scott Olson (Sep 29 2018 at 21:46):

Ah yeah I should double check what it does in that case

view this post on Zulip Scott Olson (Sep 29 2018 at 21:47):

I gotta say it's rather convenient for me coming from Rust that elan is based on rustup because I have a pretty good grasp on exactly how it works already =)

view this post on Zulip Scott Olson (Sep 29 2018 at 21:55):

@Reid Barton You're right, using lean --make _target/deps/mathlib is the simplest/safest way to make sure it builds the whole thing with your current project's Lean version


Last updated: May 14 2021 at 06:16 UTC