Zulip Chat Archive

Stream: new members

Topic: Windows Installation Issue


view this post on Zulip 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.

view this post on Zulip 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"
]
}

view this post on Zulip Kevin Buzzard (Sep 24 2020 at 20:59):

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

view this post on Zulip ZY Cao (Sep 24 2020 at 21:07):

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

view this post on Zulip 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*

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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"
]
}

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 22:10):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 22:11):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip ZY Cao (Sep 24 2020 at 22:16):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 22:53):

And then input lean --path.

view this post on Zulip 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"
]
}

view this post on Zulip Joel Schargorodsky (Sep 25 2020 at 00:27):

in the project's directory, rather

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Joel Schargorodsky (Sep 25 2020 at 01:20):

I cloned an existing project from github.

view this post on Zulip 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).

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 01:22):

Here's a page with more info about leanproject.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Joel Schargorodsky (Sep 25 2020 at 15:26):

I merely opened a particular file in the igl2020 folder.

view this post on Zulip 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)."?

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:27):

Sorry, I wrote that before seeing your latest message.

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:27):

So this is what went wrong.

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 15:34):

How about this.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 15:37):

Oh yes, including screenshots would be great.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 15:38):

you_didnt_open_the_project_folder.png

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Joel Schargorodsky (Sep 25 2020 at 15:39):

leanscreenshot.png

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 15:40):

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

view this post on Zulip Joel Schargorodsky (Sep 25 2020 at 15:40):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Sep 25 2020 at 15:41):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:52):

I thought it was already displaying a big warning

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:54):

I just checked and it doesn't.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:54):

So we lost that somehow.

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:55):

no_warning.gif

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:56):

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

view this post on Zulip Patrick Massot (Sep 25 2020 at 15:57):

@Gabriel Ebner any idea?

view this post on Zulip 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