Programme not working

Stream: new members

[Mark Powell]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Things should work in seconds, not fail in minutes.