Issues on windows for new users

Stream: general

[Edward Ayers]

Hi I had a new user today and we were trying to install lean on windows by following the mathlib instructions, there were loads of issues getting everything working however. This might just be because we didn't follow the instructions well enough though. I'm posting the issues we had just to see if there are any easy wins to fix them.
- ~/.profile was not sourced by git bash, either in the vscode terminal or in a new git-bash window. I had to move it to ~/.bashrc
- VSCode did not manage to find the lean executable in ~/.elan/bin. This was not rectified by running the 'install using elan' prompt. I fixed this by explicitly setting the lean executable vscode setting, but that took a couple of attempts because you had to use the windows-style path not the bash-style path.
- Running the install by elan prompt happened multiple times in desperation, and this meant that it was added to .profile multiple times so the path would have ~/.elan/bin in it multiple times.
- Finally, the import fail 'not in LEAN_PATH' error for import topology.basic came up but it was not clear how to fix it, I think this was solved through some combination of restarts and calling leanpkg build / configure. Does anyone know what exactly causes this error?

[Floris van Doorn]

It's hard to reply to some of these comments if you didn't follow the instructions closely. I've installed Lean a couple of times now following the instructions closely, and they worked for me. If you see a way to make the instructions more robust, feel free to tell us.

- Finally, the import fail 'not in LEAN_PATH' error for import topology.basic came up but it was not clear how to fix it, I think this was solved through some combination of restarts and calling leanpkg build / configure. Does anyone know what exactly causes this error?

This tends to happen if you open a .lean file directly in VSCode without opening the whole project folder:

On the main screen, or in the File menu, click "Open folder" (on a Mac, just "Open"), and choose the folder my_project (not one of its subfolders).

[Floris van Doorn]

It can of course also happen if you have skipped other steps from the installation instructions, like calling leanpkg configure for the first time.

[Bryan Gin-ge Chen]

I think the latest version of the VS Code extension now warns users if they open a file in a folder without a leanpkg.path file.

[0076_Haikal Isa Al Mahdi]

I am here to ask a few question. Hope anyone can give me the clear explanation. Given how slow Lean is in my machine (i use vscode), 1) What's the system requirement to run Lean and its libraries? 2) Is Lean supposed to be hyperreactive for any cursor movement? 3) Why the lean playground suffers from the performance issue?.

Thank you

[Yaël Dillies]

Generally speaking, you will suffer if your machine doesn't have >=32GB of RAM

[Kevin Buzzard]

Is that really true? I tell people 16 nowadays.

[Henrik Böving]

1) That depends on what you include in "its libraries" for Lean core alone you can probably get away with just 8GB. For mathlib you need at least 8 just for mathlib alone so probably you want 16 or more.
2) That again depends on what you mean by hyper reactive and what specifically you are working on. Sometimes having instant feedback is just not possible because your proof is still computing. If you have an example of a particular slowness do tell us about it
3) in my experience on a sufficiently fast internet connection the lean playground is sufficiently fast at least if it is not under contention.

[Yaël Dillies]

Kevin Buzzard said:

Is that really true? I tell people 16 nowadays.

My (Windows) laptop has 16GB and it almost grinds to a halt when running even a single instance of lean

[Johan Commelin]

Henrik's (1) doesn't seem to factor in the OS. That might explain why 16GB is not enough on some systems.

[Violeta Hernández]

I had a laptop with 12GB and this was barely enough to work on Mathlib. I regularly had to close my browser while using it as otherwise all my RAM would get used up. Now I have a newer laptop with 24GB, and it works like a charm.

[Henrik Böving]

Johan Commelin said:

Henrik's (1) doesn't seem to factor in the OS. That might explain why 16GB is not enough on some systems.

For the type of loads that we keep track of in radar this does take the OS into account. We know that a current mathlib import takes 3GB of memory and similarly maxrss when building mathlib from scratch is also at 3GB. My understanding is that a Windows gobbles up ~4GB of memory just on its own so 16 should hopefully leave quite a bit of RAM free to do other things besides Lean. We have noticed that e.g. Firefox can consume quite a bit of additional RAM so sometimes it is also a synergy of programs that leads to these issues.

If you are experiencing situations where 16 GB of RAM is not enough please do tell us about them! Even if it turns out that the reason is "legitimate" we need to know that this situation exists and track it as a metric in our benchmarking setup.

In particular please provide the following information:

• what mathlib version were you working on, please provide the commit, e.g. via git rev-parse HEAD
• what editor are you using
  • especially with VSCode a list of extensions you installed can be helpful as well. In the past we've even been able to track down bugs in official Microsoft extensions
• do you have multiple tabs/buffers open in the editor at the same time? If so how many? We can share the information from importing the olean files but every tab in your editor has certain non-shareable informations so you can't just open infinitely many tabs without running out of memory
• what file were you working on, what were you doing? Ideally a video of the action that causes the issue if you can pin it down to doing a particular thing
• what anti-virus / corporate spyware if any do you have on your machine
• are you using storage in the cloud such as Dropbox, OneDrive etc.
• if you are in vscode send us the setup information by opening the forall menu and selecting "show setup information"
  image.png
  

it should look like so:
image.png

• if you are on a non vscode editor please do provide the information through other means such as lscpu etc.

• If you are on Windows please do send us some information from the task manager/resource monitor:

  • for the task manager sort your processes by memory and find e.g. the vscode process tree then open it, please send us a screenshot of this:
    image.png

    

  • next open the resource monitor and switch to memory, sort this by working set size and also send us a screenshot of it like so:
    image.png

    

• if you are on Linux please send us:

  • the output of cat /proc/meminfo. If this file is not available the output of free -hm instead.

  • a screenshot of htop with the following configuration: htop -F 'lean|lake|code|nvim|emacs' -t now you need to set a few config options:

    1. press f2 to go into setup, in display options make sure to set hide userland process threads: image.png

       

    2. navigate to screens and ensure that M_PRIV and M_PSS are added to the columns:
       image.png

       

    3. you should now be greeted with a screen such as the following, please send us a screenshot of it:
       image.png

       

• if you are on MacOS my understanding is you can at least follow a similar approach as Linux to get this information but I don't have access to a MacOS machine at the moment

[Johan Commelin]

@Henrik Böving I stand corrected.
Thanks!