Zulip Chat Archive

Stream: general

Topic: lean failing quietly

Kevin Buzzard (Mar 06 2018 at 22:20):

Lean has got worse and worse recently, at least for me. I am sorely tempted to just check out a version from a week or two ago and compile that and use it instead. I have a largeish file open (350 lines) and after Lean: Restart in VS Code I get the orange "compiling" lines and then they just disappear, there are no red failure lines, nothing in lean messages, and lean isn't running any more in the sense that none of my #checks are underlined in green.

Kevin Buzzard (Mar 06 2018 at 22:21):

I am getting those memory overflow messages on a regular basis and having to restart

Kevin Buzzard (Mar 06 2018 at 22:21):

I appreciate it's super-complex software but it didn't used to be like this

Kevin Buzzard (Mar 06 2018 at 22:24):

I am actually missing the overflow messages now I am having to deal with silent failures. I removed all olean files and hopefully things will be a bit better (I thought we did not have to do this any more but it seems to have made some difference).

Kevin Buzzard (Mar 06 2018 at 22:25):

Is there any way I can give user feedback about all the overflow errors? They strike all the time.

Kevin Buzzard (Mar 06 2018 at 22:44):

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

Kevin Buzzard (Mar 06 2018 at 22:44):

that one

Scott Morrison (Mar 06 2018 at 23:08):

Have you increased your memory limit, or are you just running with the default? I think most people are running with more than the default.

Scott Morrison (Mar 06 2018 at 23:10):

Note that it’s not just the file you have open that affects memory requirements: imports matter too, although I don’t have any sense of the relative memory requirements of stuff loaded from olean files vs processed in this session.

Scott Morrison (Mar 06 2018 at 23:12):

Probably the default memory limit in the VS Code and emacs extensions should just be raised, so newcomers don’t get tripped up by this.

Scott Morrison (Mar 06 2018 at 23:14):

On the other hand, Lean silently failing is bad news. If you’ve got something that reproducibly causes VS Code’s Lean extension to silently fail, you should 1. Check if lean —make also fails (it may tell you something more informative) 2. Post it here!

Last updated: Dec 20 2023 at 11:08 UTC