Zulip Chat Archive

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:
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 (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 :
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 (Sep 24 2020 at 22:10):

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 (Sep 24 2020 at 22:10):

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

Bryan Gin-ge Chen (Sep 24 2020 at 22:11):

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

ZY Cao (Sep 24 2020 at 22:12):

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 (Sep 24 2020 at 22:13):

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 (Sep 24 2020 at 22:16):

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

Joel Schargorodsky (Sep 24 2020 at 22:29):

@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 (Sep 24 2020 at 22:52):

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 (Sep 24 2020 at 22:53):

And then input lean --path.

Joel Schargorodsky (Sep 25 2020 at 00:26):

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 (Sep 25 2020 at 00:27):

in the project's directory, rather

Bryan Gin-ge Chen (Sep 25 2020 at 00:50):

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 (Sep 25 2020 at 01:08):

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 (Sep 25 2020 at 01:20):

I cloned an existing project from github.

Bryan Gin-ge Chen (Sep 25 2020 at 01:21):

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 (Sep 25 2020 at 01:22):

Here's a page with more info about leanproject.

Joel Schargorodsky (Sep 25 2020 at 15:19):

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 (Sep 25 2020 at 15:21):

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 (Sep 25 2020 at 15:23):

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 (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):

How about this.

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
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 (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.

Patrick Massot (Sep 25 2020 at 15:55):

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: Dec 20 2023 at 11:08 UTC