## Stream: new members

### Topic: Windows Installation Issue

#### j s (Sep 24 2020 at 20:47):

I have installed Lean as well as Mathlib, but when I run import tactic, a red squiggly line is displayed; it seems that I am
unable to import mathlib. This is on Windows 10.

#### ZY Cao (Sep 24 2020 at 20:55):

I followed the instructions at
https://leanprover-community.github.io/get_started.html

But the #eval 2+2did not work.
Here is the outcome:
$which lean /c/Users/曹/.elan/bin/lean$ lean --path
{
"is_user_leanpkg_path": true,
"leanpkg_path_file": "C:\\Users\\曹\\.lean\\leanpkg.path",
"path": [
"C:\\Users\\▒\\.elan\\toolchains\\stable\\bin\\..\\library",
"C:\\Users\\▒\\.elan\\toolchains\\stable\\bin\\..\\lib\\lean\\library"
]
}

#### Kevin Buzzard (Sep 24 2020 at 20:59):

All this looks good. Did you open a project (and not just a file)?

#### ZY Cao (Sep 24 2020 at 21:07):

Yes, I opened the tutorial project, and still have the same issue

#### Joel Schargorodsky (Sep 24 2020 at 21:16):

The error code that I receive when I hover my mouse over the red squiggly lines is as follows:
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more*

#### Bryan Gin-ge Chen (Sep 24 2020 at 21:27):

What do you see when you run lean --path in the directory of the project you're looking at? (for both @Joel Schargorodsky and @ZY Cao)

#### Bryan Gin-ge Chen (Sep 24 2020 at 21:28):

Also @ZY Cao what do you mean by "But the #eval 2+2 did not work. ". Did you get an error message? Or just no output in the info view panel?

#### ZY Cao (Sep 24 2020 at 22:09):

I got an error saying :
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

#### ZY Cao (Sep 24 2020 at 22:10):

for lean --path, I got:

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:25):

OK, if you did that then messing around with leanproject further shouldn't be necessary (in principle). When you said "cloned" I thought you meant you just ran something like git clone https://github.com/vaibhavkarve/igl2020.

Sorry if I already asked this, but when you're opening Lean files, you're opening the entire igl2020 directory in VS Code first, right?

#### Joel Schargorodsky (Sep 25 2020 at 15:26):

I merely opened a particular file in the igl2020 folder.

#### Patrick Massot (Sep 25 2020 at 15:27):

Did you pay special attention to the line "If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder tutorials (not one of its subfolders)."?

#### Patrick Massot (Sep 25 2020 at 15:27):

Sorry, I wrote that before seeing your latest message.

#### Patrick Massot (Sep 25 2020 at 15:27):

So this is what went wrong.

#### Patrick Massot (Sep 25 2020 at 15:28):

But you should have seen a popup message from VScode warning you.

#### Joel Schargorodsky (Sep 25 2020 at 15:28):

I think I may have just resolved my issue by adding igl2020 to Workspace; the error messages that were present on VS Code no longer appear.

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:30):

Great! I don't think the vscode-lean extension supports VS Code workspaces with multiple roots (relevant issue), so note that if you add more folders to the workspace things might break.

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:33):

It seems that opening a file instead of the project folder is still the most common issue that new users run into. Do you have any recommendations on how we might make it more clear that this step is necessary?

#### Kevin Buzzard (Sep 25 2020 at 15:34):

Is there a way that a user can "rescue" the situation, once they've opened a file and are staring at our "it didn't work" website?

#### Kevin Buzzard (Sep 25 2020 at 15:35):

instad of actually having to close VS Code and start again -- I mean -- what is the difference in VS Code when you open a file or open a project -- there will be some really easy diagnosis of this with some screenshot comparison and then we just tell them to click on "add project" and to add their project

#### Kevin Buzzard (Sep 25 2020 at 15:36):

just with two big pictures of what it should look like and what to do if it looks like what their screen looks like because they opened a file

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:37):

Oh yes, including screenshots would be great.

#### Joel Schargorodsky (Sep 25 2020 at 15:38):

Would you like me to send a screenshot of what I currently see in my VS Code terminal?

#### Kevin Buzzard (Sep 25 2020 at 15:38):

you_didnt_open_the_project_folder.png

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:38):

For rescuing, yes, I think they can either just choose "Open / Open folder" and then select the project folder or do something with workspaces.

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:39):

I think by default the color of the status bar is purple rather than blue if you opened a file instead of a folder.

#### Joel Schargorodsky (Sep 25 2020 at 15:39):

leanscreenshot.png

#### Kevin Buzzard (Sep 25 2020 at 15:39):

Maybe people don't even know how to open VS Code except by finding a Lean file and clicking on it -- maybe this is all completely new to them and they don't even know what the VS Code icon looks like

#### Kevin Buzzard (Sep 25 2020 at 15:40):

"open VS Code" = "open lean file" to some people maybe?

#### Joel Schargorodsky (Sep 25 2020 at 15:40):

I don't think I require any further assistance at the moment. Thanks for your guidance.

#### Kevin Buzzard (Sep 25 2020 at 15:40):

Oh sure :-) We're just discussing about how this is coming up a lot recently, and how best to fix it for future users.

#### Heather Macbeth (Sep 25 2020 at 15:41):

@ZY Cao maybe this will help with your issue, too? (See discussion above.)

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:42):

I think ZY's issue was related to the fact that his username had a unicode character in it and that was somehow breaking things: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Windows.20Installation.20Issue/near/211195694

#### Alex J. Best (Sep 25 2020 at 15:48):

Could we get the VSCode extension to determine if a folder is open and flash a big warning about it within vscode?
Currently if I open a file instead of a project I see

00_first_proofs.lean:1:1
Messages (2)
00_first_proofs.lean:1:0
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more


in the infoview and I have to realise there is a useful link and copy paste it to my browser to read the advice. But I'd imagine the extension must already know if a file has been opened rather than a folder?

#### Patrick Massot (Sep 25 2020 at 15:52):

I thought it was already displaying a big warning

#### Patrick Massot (Sep 25 2020 at 15:54):

I just checked and it doesn't.

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:54):

It's supposed to pop up an alert which shows up in the bottom right.

#### Patrick Massot (Sep 25 2020 at 15:54):

So we lost that somehow.

no_warning.gif

#### Patrick Massot (Sep 25 2020 at 15:56):

This used to work, but everything related to VSCode extensions is very brittle.

#### Patrick Massot (Sep 25 2020 at 15:57):

@Gabriel Ebner any idea?

#### Gabriel Ebner (Sep 25 2020 at 17:03):

Please file an issue on the vscode-lean bug tracker. I can take a look at it after the weekend.

Last updated: May 14 2021 at 03:27 UTC