increase memory consumption threshold

Stream: general

[Kevin Buzzard]

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]

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

[Kenny Lau]

go to task manager and look at memory consumption?

[Reid Barton]

That sometimes means Lean thinks it needs to rebuild things

[Gabriel Ebner]

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]

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]

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]

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]

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

[Reid Barton]

My impression is that it does not

[Reid Barton]

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]

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