Zulip Chat Archive

Stream: new members

Topic: Programme not working


Mark Powell (Jan 20 2022 at 19:36):

Hi, sorry if this is the wrong place to ask this, but is there any chance of some help getting lean working? I followed the instructions on my personal laptop, and it all worked fine. Then I tried it on my office computer, and it works less well. It's not a complete failure, but as good as. To test, I'm in mathematics_in_lean going through welcome.lean. When I "try it", it prints Hello World and 2+ 2 : N, f: N -> N for the checking in the next one. Then I get to the third grey box with a "try it" option. It has to import something. First it says it is loading for a rather long time. Then after a few minutes it gives me lots of error messages like this:

Error updating: excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold).

Any help much appreciated. Mark

Patrick Massot (Jan 20 2022 at 19:42):

Are you talking about using this book in a web browser or did you install Lean on your computer?

Kevin Buzzard (Jan 20 2022 at 19:54):

This error indicates that you have not got a working and fully compiled mathlib

Kevin Buzzard (Jan 20 2022 at 19:55):

Things should work in seconds, not fail in minutes.


Last updated: Dec 20 2023 at 11:08 UTC