Windows Installation Issue

Stream: new members

[j s]

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]

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]

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

[ZY Cao]

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

[Joel Schargorodsky]

The error code that I receive when I hover my mouse over the red squiggly lines is as follows:
file 'tactic' not found in the search path
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]

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]

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]

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

[ZY Cao]

for lean --path, I got:
$ 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"
]
}

[Bryan Gin-ge Chen]

Oh, I wonder if the fact that your username is "曹" is causing problems.

[Bryan Gin-ge Chen]

The character in the filename under "path" is ▒ not 曹.

[ZY Cao]

I was wondering the same thing. Would it help if I simply change it to something in English? Something the program can recognize?

[Bryan Gin-ge Chen]

That sounds like a reasonable thing to try. I'm not sure whether it's lean or elan that has a problem here.

[ZY Cao]

Yeah I will try that and see if it works. Thanks for the help.

[Joel Schargorodsky]

@Bryan Gin-ge Chen I'm fairly new to lean, and do not know how to access the directory. Can you tell me how?

[Bryan Gin-ge Chen]

I'm assuming you followed all the instructions here and then here?

If so, then open a git bash terminal window and navigate to the root of the directory of the project that you're working in with cd.

[Bryan Gin-ge Chen]

And then input lean --path.

[Joel Schargorodsky]

this is the output that I receive when I run lean --path in the gitbash terminal:
{
"is_user_leanpkg_path": false,
"leanpkg_path_file": "C:\\Users\\bensc\\igl2020\\leanpkg.path",
"path": [
"C:\\Users\\bensc\\.elan\\toolchains\\leanprover-community-lean-3.19.0\\bin\\..\\library",
"C:\\Users\\bensc\\.elan\\toolchains\\leanprover-community-lean-3.19.0\\bin\\..\\lib\\lean\\library",
"C:\\Users\\bensc\\igl2020\\_target/deps/mathlib/src",
"C:\\Users\\bensc\\igl2020\\./src"
]
}

[Joel Schargorodsky]

in the project's directory, rather

[Bryan Gin-ge Chen]

I'm a little puzzled as to why there are both forward slashes and backslashes in the "path" field. How did you create the igl2020 project, did you use leanproject new?

[Shing Tak Lam]

Bryan Gin-ge Chen said:

I'm a little puzzled as to why there are both forward slashes and backslashes in the "path" field. How did you create the igl2020 project, did you use leanproject new?

Mine is the same (in a working Lean project on Windows), and I did use leanproject new.

[Joel Schargorodsky]

I cloned an existing project from github.

[Bryan Gin-ge Chen]

If you have leanproject installed then I think running leanproject get-mathlib-cache in the igl2020 directory will fix things (after you restart Lean).

[Bryan Gin-ge Chen]

Here's a page with more info about leanproject.

[Joel Schargorodsky]

Bryan Gin-ge Chen said:

If you have leanproject installed then I think running leanproject get-mathlib-cache in the igl2020 directory will fix things (after you restart Lean).

I ran this in the igl2020 directory. I get receive this as output:
Invalid git repository

[Bryan Gin-ge Chen]

What's the repo that you cloned and how is it related to igl2020 on your computer? i.e. is igl2020 a sub-directory of the repo, or vice versa?

[Joel Schargorodsky]

I followed the following instructions; I don't know if this will satisfy your inquiry:
Run the following $ leanproject get vaibhavkarve/igl2020 in your terminal or command prompt. This will create a new folder called igl2020 and it will copy mathlib oleans into it.

[Bryan Gin-ge Chen]

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]

I merely opened a particular file in the igl2020 folder.

[Patrick Massot]

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]

Sorry, I wrote that before seeing your latest message.

[Patrick Massot]

So this is what went wrong.

[Patrick Massot]

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

[Joel Schargorodsky]

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]

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]

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]

How about this.

[Kevin Buzzard]

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]

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]

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]

Oh yes, including screenshots would be great.

[Joel Schargorodsky]

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

[Kevin Buzzard]

you_didnt_open_the_project_folder.png

[Bryan Gin-ge Chen]

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]

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]

leanscreenshot.png

[Kevin Buzzard]

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]

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

[Joel Schargorodsky]

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

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

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]

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
file 'data/real/basic' not found in the search path
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]

I thought it was already displaying a big warning

[Patrick Massot]

I just checked and it doesn't.

[Bryan Gin-ge Chen]

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

[Patrick Massot]

So we lost that somehow.

[Patrick Massot]

no_warning.gif

[Patrick Massot]

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

[Patrick Massot]

@Gabriel Ebner any idea?

[Gabriel Ebner]

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