## Stream: new members

### Topic: Hardware demand after mathlib upgrade

#### 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. #### 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. #### 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) #### Reid Barton (Sep 26 2020 at 22:43): I guess you're in a separate project with mathlib as a dependency? #### 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. #### 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? #### 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... #### 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. #### 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? #### 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) #### 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. #### 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. #### 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. #### 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. #### Miroslav Olšák (Sep 26 2020 at 23:53): Is there a way to estimate at which percentage of the compilation it is? #### Yury G. Kudryashov (Sep 26 2020 at 23:55): No. #### 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.

#### 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.

#### Miroslav Olšák (Sep 27 2020 at 00:33):

So I tried leanproject

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### Alex J. Best (Sep 27 2020 at 01:30):

leanproject new project_name

#### Miroslav Olšák (Sep 27 2020 at 01:32):

Oh, that was not so difficult :-)

#### Miroslav Olšák (Sep 27 2020 at 01:33):

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

#### 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.

#### Miroslav Olšák (Sep 27 2020 at 01:33):

I have noticed, that is nice.

#### 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,

#### Miroslav Olšák (Sep 27 2020 at 01:35):

I am looking at leanproject global-install now.

#### Miroslav Olšák (Sep 27 2020 at 01:37):

where did it install the mathlib?

#### 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.

#### Miroslav Olšák (Sep 27 2020 at 01:41):

~/.lean, probably...

#### 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...

#### Yury G. Kudryashov (Sep 27 2020 at 01:46):

I just work on mathlib branches.

#### 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