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.