memory usage with vscode, lean and mathlib

Stream: new members

[Ingo Wechsung]

Hi, I am trying to learn theorem proving with Lean and cloned the tutorial project from github to work through it. I use vscode with lean extension.

Unfortunately, lean seems to require lots of memory. No matter what file I open, it comes back with a lot of errors all originating from import data.real.basic saying it hasn't enough memory.
I was able to fix this by, setting the memory limit to 6000, but now my computer which has only 8GB starts paging and the system becomes unusable.

Did I something wrong, or is this normal? And what happens if one does non-basic stuff?

[Kevin Buzzard]

This is not normal. Probably you did not compile the project. Did you just git clone? This is no good. You should use leanproject which clones and compiles.

[Kevin Buzzard]

https://github.com/leanprover-community/tutorials/blob/master/README.md

[Ingo Wechsung]

Yes, I did git clone, then leanpgk configure.
Is there an extra git for leanproject, since I don't have it. I have elan, though?

[Kevin Buzzard]

If you're following the instructions on the official MS page you're in trouble, because this is two years out of date. The maths library has grown a substantial amount since then and the community has our own community web pages explaining how to do things now. Try here.

[Kevin Buzzard]

Probably leanpkg build still works, but it might take several hours. The advantage of leanproject is that it won't compile anything, it will simply download the compiled .olean binaries from an Azure server making your life a whole lot easier.

[Kevin Buzzard]

The problem is that the MS pages were written in late 2017 and since then a lot has happened.

[Ingo Wechsung]

Thank you, @Kevin Buzzard , I did the long "wget ...." thing and the leanproject is now available, and I'm now doing leanproject build, I think this will do it.

[Kevin Buzzard]

Hopefully leanproject build will finish in finite time!

[Ingo Wechsung]

Compiling a finite number of source files of finite length will, I guess :)

.... and .... it's done and when I open a source file, its now done in NO time .... thank you.

[Patrick Massot]

@Ingo Wechsung if you follow the instructions on the website then you never need to compile anything to do the tutorials.

[Patrick Massot]

If you forget about using git directly and simply type leanproject get tutorials in some terminal then you will get everything precompiled.

[Ingo Wechsung]

Yes, @Patrick Massot I understand now, but I first installed lean through the vscode extension, unfortunately. And then there simply wasn't something like leanproject

I also think that compiling the stuff is faster than loading zillions of olean files, at least here in rural germany :)

[Yakov Pechersky]

The oleans file is a compressed file that is about the size of loading 6 modern web pages.

[Jon Eugster]

Currently I get quite frequently to a point where lean crashes with excessive memory consumption. Of course I can restart Lean or reopen VS Code to fix them, but what are the general options to improve my working setup. So far I gathered that I can:

1) leanproject get-mathlib-cache to get a compiled version of mathlib
2) leanproject mk-cache; leanproject get-cache I am unsure but I assume this caches my current work.
3) I read that complicated definitions can be marked as irreducible to help Lean.

Is there more to know about memory consumption?

[Eric Wieser]

Are you working on mathlib itself, or your own project?

[Jon Eugster]

My own project.
Usually it seems to be related to skimming through the mathlib files chasing definitions.

[Ruben Van de Velde]

You might be unintentionally making changes to the mathlib files, and then lean thinks "alright, I'll recompile all of mathlib (or the parts that depend on this file, at least) for you"

[Jon Eugster]

Ruben Van de Velde said:

You might be unintentionally making changes to the mathlib files, and then lean thinks "alright, I'll recompile all of mathlib (or the parts that depend on this file, at least) for you"

and I would fix that with just checking git status and remove any changes in the mathlibs part, wouldn't I?

[Alex J. Best]

Even if you edit a file in vscode without saving vscode updates the lean server with the live version of the file. But you can close all vscode tabs except the one you want and click don't save on any you didn't intend to save. Then restart the lean server from within vscode

[Kevin Buzzard]

So I ran into this situation recently and it was quite delicate to diagnose. The general tips are: definitely don't ever edit a mathlib or core Lean file unless for some reason you really have to, close files you're not using, and if this doesn't fix the problem (which it might not) then maybe you have uncovered an issue with something not being irreducible, so post a #mwe and people can look at it and try and figure out what the problem is. People would typically happily look at sluggish files if they just import mathlib stuff. Issues you find might help to make mathlib compile faster, which is always something we like. NB I never use leanproject mk-cache.

[Eric Wieser]

I've definitely seen the behavior before where "go to definition" causes vscode to appear to rebuild mathlib files

[Eric Wieser]

Could it be something really dumb like the Olean cache being missed due to different line endings on the build server?

[Eric Wieser]

(since git is often configured to meddle with line endings on checkout)

[Mario Carneiro]

the behavior you mention I think has to do with lean deciding to replace the stored olean version of a file with the "live" version based on the lean text, which is required to give detailed hover and goal info when you are inside the file itself

[Eric Wieser]

Does that cause it to invalidate downstream olean files?

[Mario Carneiro]

unclear

[Mario Carneiro]

I learned about this hypothesis from @Gabriel Ebner , he might be able to say more

[Gabriel Ebner]

Yes, go-to-definition needs to rebuild the file if it was originally loaded from olean. (Because otherwise you don't get tactics states, hover info, etc.) I don't think it causes the reverse dependencies to be recompiled.

[Jon Eugster]

Gabriel Ebner said:

Yes, go-to-definition needs to rebuild the file if it was originally loaded from olean. (Because otherwise you don't get tactics states, hover info, etc.) I don't think it causes the reverse dependencies to be recompiled.

That makes a lot of sense, thx for the elaboration

[Filippo A. E. Nuccio]

I often use the VSCode extension Remote - SSH to run Lean on my university server rather than on my laptop, and I am wondering how should I set the memory threshold. Ideally, I would like that the remote setting be something like 100GB but that when I work locally it is only 6GB or so. I have tried to modify the setting, but it seems to me that the modifications are only stored locally, so that if I set the limit to 100GB while connected to the university, it will still be the same even if I close the connection (of course I don't have 100GB of ram on my laptop, I guess it will mean "take whatever memory you want to"). Any help/hint/advice appreciated!

[Yakov Pechersky]

When you are setting values in Settings, there are ways to make it take on different settings whether you are in Remote-SSH mode or in local mode. But I don't remember which is which atm

[Filippo A. E. Nuccio]

Thanks - if you later figure out how to do this, I'll be very much grateful.

[Yakov Pechersky]

https://code.visualstudio.com/docs/remote/ssh#_ssh-hostspecific-settings

[Filippo A. E. Nuccio]

Thanks!

[Alistair Tucker]

Kitty Gorey said:

Not sure if this is the right place to ask this but how much memory does Lean need? I followed the instructions on https://leanprover-community.github.io/install/project.html and VSCode slowly use more and more of my (laughable) ~4GB of usable RAM. Once VSCode has around 2048MB of memory used up my computer just starts acting like it's on its deathbed. Is this normal?

There may be something subtly wrong with your set-up. I don't have this problem on a 4GB Mac.