problems with paths

Stream: new members

[Tianchen Zhao]

eudoxus.png cmd.png
I got some problems with my path. The first image is running on an existing project, which seems fine. The second image is just running on root directory and it says leanpkg file could not find home. Does anyone have any solutions? Thank you.

By the way, leanproject command is not working as well. It might just be because I am in China. Are these two questions related? clone.png

[Alex J. Best]

Does the first issue actually cause you any issues, I use lean all the time, but always in a project, on my machine the result of your second picture points to a file that does not exist but it hasn't seemed to be an issue.

[Alex J. Best]

As for the second issue, if you navigate to that web address (oleanstorage.azureedge.net/... in the third screenshot) can you download that file and save it in the location mentioned there? What happens if you re-run leanproject after that?

[Bryan Gin-ge Chen]

Here's the URL by the way, I just tried leanproject get tutorials (from the US) and it worked for me: https://oleanstorage.azureedge.net/mathlib/4355d17105aac6e4e2e4d2ca3cffd44c61b87533.tar.xz

[Rob Lewis]

The SSL stuff looks like a broader Python config issue (https://www.google.com/search?q=ssl+error+eof+occurred+in+violation+of+protocol&oq=ssl+error+eo&aqs=chrome.0.0j69i57j0i22i30l6.3018j0j7&sourceid=chrome&ie=UTF-8)

[Rob Lewis]

But also I think leanproject probably assumes you're using git bash instead of the Windows shell, right?

[Alex J. Best]

Rob Lewis said:

But also I think leanproject probably assumes you're using git bash instead of the Windows shell, right?

I just tried this and it does work in powershell for me too (but I do normally use git bash)

[Julian Berman]

(you can also try posting or looking at the output of openssl s_client -connect oleanstorage.azureedge.net:443 which should tell you whether the firewall is intercepting your connection I believe)

[Tianchen Zhao]

(deleted)

[Tianchen Zhao]

Alex J. Best said:

Does the first issue actually cause you any issues, I use lean all the time, but always in a project, on my machine the result of your second picture points to a file that does not exist but it hasn't seemed to be an issue.

Yes the first issue just causes all my import statements to fail. I can run simple codes without any imports but as long as there is an import, it says for example "file 'tactic' not found in the search path".

[Tianchen Zhao]

I just reinstalled lean. Now lean --path gives me different outputs, but my import statements still fail.
(the first output is in root directory and the second output is in the project) 1.PNG

Maybe my second output is still wrong. Lean --path gives different output in my friend's computer. There are two additional lines in his output. Inked2_LI.jpg

[Bryan Gin-ge Chen]

It looks like you haven't added mathlib as a dependency of your eudoxus-master project. The recommended way to create a project is using leanproject new. You can run leanproject add-mathlib in that directory to add it now. See the leanproject documentation.

Note that all Lean code should be in a project directory. I'm saying this because you have mentioned the paths in the "root directory" a few times and I don't think that's the right way to think about Lean.

Hope this helps!

[Tianchen Zhao]

Bryan Gin-ge Chen said:

It looks like you haven't added mathlib as a dependency of your eudoxus-master project. The recommended way to create a project is using leanproject new. You can run leanproject add-mathlib in that directory to add it now. See the leanproject documentation.

Note that all Lean code should be in a project directory. I'm saying this because you have mentioned the paths in the "root directory" a few times and I don't think that's the right way to think about Lean.

Hope this helps!

I think you are correct on adding mathlib, but it says mathlib is not found in the path. Also, I cannot use leanproject new my_project because of the second issue I've mentioned. I will try to find solutions to that. Do you think this problem is related to the one about mathlib? Thank you for the advice! mathlib.PNG newpj.PNG

[Bryan Gin-ge Chen]

Yes, it is related. From the screenshots, it looks like you now are not able to reach raw.githubusercontent.com, which means you won't be able to add mathlib.

[Yakov Pechersky]

btw, it is leanproject add-mathlib, not lean add-mathlib

[Yakov Pechersky]

But moot if you can't access github

[Tianchen Zhao]

Yakov Pechersky said:

btw, it is leanproject add-mathlib, not lean add-mathlib

Oops thanks for that. It now says "This project already depends on mathlib", but yes I need to first access raw.githubusercontent.com.

[Tianchen Zhao]

Bryan Gin-ge Chen said:

Yes, it is related. From the screenshots, it looks like you now are not able to reach raw.githubusercontent.com, which means you won't be able to add mathlib.

I see. I will first try to reach raw.github. Thank you!

[Kevin Buzzard]

Are you the Tianchen Zhao from Imperial? You should be able to get to the GitHub sites if you use your Imperial VPN

[Tianchen Zhao]

Kevin Buzzard said:

Are you the Tianchen Zhao from Imperial? You should be able to get to the GitHub sites if you use your Imperial VPN

Yes I am. I can get to Github sites with my own VPN, but it just doesn't work using git bash. Maybe it's not a problem on VPN, but I will try Imperial VPN too.

[Tianchen Zhao]

Kevin Buzzard said:

Are you the Tianchen Zhao from Imperial? You should be able to get to the GitHub sites if you use your Imperial VPN

Omg Imperial VPN made it! I love Imperial so much! Thank you!