excessive memory consumption detected at expression trave...

Stream: new members

[Luisitoon]

Hi, all! I am Luis from Barcelona! I am just trying to run Lean 3 on Debian-based Linux (Ubuntu) with VS Code and the Lean Infoview shows me the following error: "excessive memory consumption detected at expression traversal (potential solution: increase memory consumption threshold)". Have you ever got across this error? Everything is fine but this... (I have both Windows and Ubuntu on the laptop, everything runs perfectly on Windows, but not on Ubuntu...)

[Notification Bot]

A message was moved here from #general > golf request by Kyle Miller.

[Kyle Miller]

@Luisitoon Had you ever had Lean working before?

How did you install and set up Lean? Did you follow https://leanprover-community.github.io/get_started.html#regular-install ?

[Luisitoon]

Hi, Kyle! Thank you for your quick answer! As I said, on Windows works perfectly fine, but on Ubuntu, despite appearing the "Orange bars", after a while they disappear and it shows that error. I have been following the leanprover community tutorial to install Lean on Ubuntu (https://www.youtube.com/watch?v=02ff4WrW0FU&ab_channel=leanprovercommunity).

[Luisitoon]

The thing is that I need to run it on Ubuntu because I want to create a Lean Game for students, such as the Natural Number Game from Kevin Buzzard, and using Ubuntu is easier than using Windows in this case :)

[Mauricio Collares]

Offtopic: Watching the video, it seems this line of the install script works by accident: it is equivalent to "apt install -y code" and does not use the downloaded code.deb, but the Ubuntu repository has a "code" package

[Junyan Xu]

"excessive memory consumption detected at expression traversal (potential solution: increase memory consumption threshold)".

In my experience this usually happens when I don't have the oleans. Did you run leanproject get-cache?

[Luisitoon]

YESSS!! It finally worked!! Thank you both for your answers!! The problem was that I had to run the command "leanproject get-mathlib-cache" and then restart Lean in VS Code. If anyone tries to solve this error again, I recommend you to look at this forum as well: https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Memory.20consumption.20of.20mathlib.html