## Stream: new members

### Topic: memory usage with vscode, lean and mathlib

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

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

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

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

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

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

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

#### Kevin Buzzard (Dec 06 2020 at 12:58):

Hopefully leanproject build will finish in finite time!

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

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

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

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

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

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

#### Eric Wieser (May 13 2021 at 20:55):

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

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

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

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

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