Zulip Chat Archive

Stream: general

Topic: increase memory consumption threshold


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 14:26):

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

view this post on Zulip Kenny Lau (Aug 02 2018 at 14:26):

go to task manager and look at memory consumption?

view this post on Zulip Reid Barton (Aug 02 2018 at 14:28):

That sometimes means Lean thinks it needs to rebuild things

view this post on Zulip 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:

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 02 2018 at 17:53):

My impression is that it does not

view this post on Zulip 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.

view this post on Zulip 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