## Stream: general

### Topic: increase memory consumption threshold

#### Kevin Buzzard (Aug 02 2018 at 14:22):

Someone is trying to use Lean on a Win 7 machine here and we're constantly running into memory issues. Lean suggests "increase memory consumption threshold" -- is this something which is possible to do and which might actually work? It's a Windows 7 machine using .olean files which were built on Windows 10 :-/ but that's only because none of us are using Win7 so we can't make the .olean files for Win7.

#### Kevin Buzzard (Aug 02 2018 at 14:26):

Every third time we hit Lean : restart we get away with it :-)

#### Kenny Lau (Aug 02 2018 at 14:26):

go to task manager and look at memory consumption?

#### Reid Barton (Aug 02 2018 at 14:28):

That sometimes means Lean thinks it needs to rebuild things

#### Gabriel Ebner (Aug 02 2018 at 17:44):

1) As @Reid Barton said, try leanpkg build first. 2) In vscode, go to user settings (ctrl+shift+p user settings), and search for lean. :smile:

#### Kevin Buzzard (Aug 02 2018 at 17:46):

It didn't look unreasonable. I initially felt like we were on the boundary of what the machine was capable of, but it didn't make much sense because the machine had 16 gigs of ram and it never got filled up. Maybe it's the dodgy .olean files (and the fact that they were zipped up from some other computer and I'm not sure the timestamps would have survived -- I don't know anything about Windows timestamps).

#### Kevin Buzzard (Aug 02 2018 at 17:47):

I don't think I can run leanpkg build -- I didn't try, but the machine did not have git and I didn't have admin privileges and I think that in the past this has been enough to stop the build from working -- it fails right at the start before trying to build anything. That was the root of the problem.

#### Reid Barton (Aug 02 2018 at 17:52):

The default limit is a mere 1GB, so it makes sense that you did not see the machine's memory fill up.
My guess is also a timestamp issue.

#### Reid Barton (Aug 02 2018 at 17:53):

When lean is invoked by the editor, does it write out .olean files for modules it compiles?

#### Reid Barton (Aug 02 2018 at 17:53):

My impression is that it does not

#### Reid Barton (Aug 02 2018 at 17:56):

It's also easy to accidentally modify a mathlib source file (especially if you are using jump-to-definition) and that also tends to cause this behavior.

#### Gabriel Ebner (Aug 02 2018 at 18:29):

I don't think I can run leanpkg build -- I didn't try, but the machine did not have git

You can also do lean --make

Last updated: May 14 2021 at 12:18 UTC