Zulip Chat Archive

Stream: new members

Topic: Hardware demand after mathlib upgrade


view this post on Zulip Miroslav Olšák (Sep 26 2020 at 22:22):

As Kevin Buzzard showed his proof of pi < sqrt 2 + sqrt 3, I noticed that my mathlib is outdated (not good enough bounds for pi), so I ran

$ leanpkg upgrade

After that, when I open a lean file in Emacs, lean just uses all the processor cores, and after some time consumes all my laptop 8G memory. Is this an expected behavior? Could it be because I upgraded mathlib but not lean?
Can I see what it is doing on the background? (compiling mathlib, I guess, but in more detail) Or idealy, could I lower its memory usage? However, Emacs apparently run it with the argument "-M4096" without appropriate effect.

view this post on Zulip Reid Barton (Sep 26 2020 at 22:41):

It's recompiling mathlib. It's better to do it manually rather than letting emacs do it, especially because if emacs does it then olean files are not written. You can run leanpkg build or use leanproject.

view this post on Zulip Reid Barton (Sep 26 2020 at 22:42):

I think leanpkg upgrade will only give the latest mathlib that works with the current version of Lean though (that is, the one specified in your current leanpkg.toml)

view this post on Zulip Reid Barton (Sep 26 2020 at 22:43):

I guess you're in a separate project with mathlib as a dependency?

view this post on Zulip Yury G. Kudryashov (Sep 26 2020 at 22:46):

Do you use leanproject? It can download precompiled oleans saving you lots of time on recompiling.

view this post on Zulip Miroslav Olšák (Sep 26 2020 at 23:03):

I am not sure. I have the file leanproject somewhere on my computer, which is however not working at the moment (probably broken with some python upgrades). My problem could also be that I just tried different procedures in history which resulted in some mess in my lean versions. Why is there actually the elan, leanpgk, leanproject?

view this post on Zulip Miroslav Olšák (Sep 26 2020 at 23:04):

Now, I am running the lean --make src, carefully watching the memory usage. 1.8G so far...

view this post on Zulip Yury G. Kudryashov (Sep 26 2020 at 23:06):

  • elan can makes lean command switch between different versions based on the contents of leanpkg.toml;
  • leanpkg comes with lean;
  • leanproject is a Python script that should be used instead of leanpkg in most cases. Among other things, it can download precompiled oleans saving you a lot of time.

view this post on Zulip Yury G. Kudryashov (Sep 26 2020 at 23:08):

What is your OS? How did you install Python? Does leanproject command work? If not, what's the error message?

view this post on Zulip Kevin Buzzard (Sep 26 2020 at 23:17):

@Miroslav Olšák once you understand the workflow you never need to compile anything, so it's worth figuring out the recommended setup (which involves never using leanpkg directly)

view this post on Zulip Miroslav Olšák (Sep 26 2020 at 23:18):

I am on Gentoo, I have Python from the package manager, however I switched from to Python 3.7 as the main python3 recently, and I deleted the packages for other python versions (to not have too many redundant packages on my computer, even my hard drive is not unlimited). However, the leanproject I have on my computer was using Python3.6, so it was now complaining about missing mathlibtools. Now I fixed it, so leanproject is working.

view this post on Zulip Yury G. Kudryashov (Sep 26 2020 at 23:18):

Kevin Buzzard said:

Miroslav Olšák once you understand the workflow you never need to compile anything

Not exactly: if you change, e.g., src/algebra/group/basic.lean, then you either recompile lots of files, or push it to github and wait while it does it for you.

view this post on Zulip Miroslav Olšák (Sep 26 2020 at 23:46):

Now, I will try to wait for the compilation I launched. The memory consumption is slowly rising, now it is on 3.5G. The entire src directory, including the compiled olean's so far has 90M. I find such behavior a bit suspicious if it is just compiling the files one by one as it shows. If it eats up all the memory again, I will try to download the precompiled files.

view this post on Zulip Scott Morrison (Sep 26 2020 at 23:49):

While lean --make src only shows one file at a time, using top you'll see that it's running multithreaded. Compiling mathlib single threaded on a 2.3GHz Xeon W currently takes 135m.

lean --make can easily consume 16 cores for a substantial period while compiling mathlib.

view this post on Zulip Miroslav Olšák (Sep 26 2020 at 23:53):

Is there a way to estimate at which percentage of the compilation it is?

view this post on Zulip Yury G. Kudryashov (Sep 26 2020 at 23:55):

No.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 00:14):

There could be at least some ways :-)...

$ find . -name *.lean | wc -l
688
$ find . -name *.olean | wc -l
691
$ find . -name *.olean -ctime 0 | wc -l
650  # this number is raising

Memory usage 4.4G by the way.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 00:33):

So the compilation is finished but the mathlib version is still not up to date enough to contain the pi estimates.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 00:33):

So I tried leanproject

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 00:36):

And it actually downloaded newer version (why?)

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 00:38):

Now, I am a bit confused of what I did, but I will manage to phrase the question in a while.

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 00:38):

We can only guess because we don't know (a) what is your setup: a mathlib branch or a project depending on mathlib; (b) which version did you have; (c) what command did you run.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:26):

OK, so what I think I did is that I edited the ".toml" file to the newest lean, then I thought it would be better to create a new project elsewhere, and after failind to do so, I updated the lean and mathib anyway. This is not weird.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:27):

What I would like to ask, however, is what is the standard way to create a new project -- that is quite confusing to me.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:28):

Let's say, I have an empty directory where I would like to have write some lean files.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:30):

As far as I understand, I need to write the leanpkg.toml file where I specify the lean version.

view this post on Zulip Alex J. Best (Sep 27 2020 at 01:30):

leanproject new project_name

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:32):

Oh, that was not so difficult :-)

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:33):

And is it necessary to be inside a project to experiment with lean and mathlib?

view this post on Zulip Alex J. Best (Sep 27 2020 at 01:33):

This will make a leanpkg.toml and a leanpkg.path as well as downloading the latest mathlib + oleans for mathlib.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:33):

I have noticed, that is nice.

view this post on Zulip Alex J. Best (Sep 27 2020 at 01:33):

Yeah I think being inside a project is the way to go, even if you just want to experiment,

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:35):

I am looking at leanproject global-install now.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:37):

where did it install the mathlib?

view this post on Zulip Alex J. Best (Sep 27 2020 at 01:37):

Personally I don't use that, maybe others do, but all of my lean projects just have their own mathlib.

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:41):

~/.lean, probably...

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 01:44):

but I have to admit that the instalation is actually way simpler than I remember it :-) when one uses the right commands...

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 01:46):

I just work on mathlib branches.

view this post on Zulip Yury G. Kudryashov (Sep 27 2020 at 01:46):

This way I usually don't forget to PR the results.


Last updated: May 15 2021 at 00:39 UTC