Hardware demand after mathlib upgrade

Stream: new members

[Miroslav Olšák]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Miroslav Olšák]

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]

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

[Yury G. Kudryashov]

• 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]

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

[Kevin Buzzard]

@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]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

No.

[Miroslav Olšák]

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]

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

[Miroslav Olšák]

So I tried leanproject

[Miroslav Olšák]

And it actually downloaded newer version (why?)

[Miroslav Olšák]

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

[Yury G. Kudryashov]

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]

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]

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]

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

[Miroslav Olšák]

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

[Alex J. Best]

leanproject new project_name

[Miroslav Olšák]

Oh, that was not so difficult :-)

[Miroslav Olšák]

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

[Alex J. Best]

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

[Miroslav Olšák]

I have noticed, that is nice.

[Alex J. Best]

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

[Miroslav Olšák]

I am looking at leanproject global-install now.

[Miroslav Olšák]

where did it install the mathlib?

[Alex J. Best]

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

[Miroslav Olšák]

~/.lean, probably...

[Miroslav Olšák]

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]

I just work on mathlib branches.

[Yury G. Kudryashov]

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