Zulip Chat Archive

Stream: new members

Topic: memory usage with vscode, lean and mathlib


view this post on Zulip Ingo Wechsung (Dec 06 2020 at 12:33):

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?

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:34):

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.

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:36):

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

view this post on Zulip Ingo Wechsung (Dec 06 2020 at 12:36):

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?

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:38):

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.

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:39):

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.

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:40):

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

view this post on Zulip Ingo Wechsung (Dec 06 2020 at 12:58):

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.

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:58):

Hopefully leanproject build will finish in finite time!

view this post on Zulip Ingo Wechsung (Dec 06 2020 at 13:01):

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.

view this post on Zulip Patrick Massot (Dec 06 2020 at 13:13):

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

view this post on Zulip Patrick Massot (Dec 06 2020 at 13:13):

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

view this post on Zulip Ingo Wechsung (Dec 06 2020 at 13:39):

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 :)

view this post on Zulip Yakov Pechersky (Dec 06 2020 at 15:10):

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

view this post on Zulip Jon Eugster (May 13 2021 at 20:49):

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?

view this post on Zulip Eric Wieser (May 13 2021 at 20:55):

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

view this post on Zulip Jon Eugster (May 13 2021 at 20:58):

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

view this post on Zulip Ruben Van de Velde (May 13 2021 at 21:02):

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"

view this post on Zulip Jon Eugster (May 13 2021 at 21:03):

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?

view this post on Zulip Alex J. Best (May 13 2021 at 21:09):

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


Last updated: May 13 2021 at 21:12 UTC