Zulip Chat Archive

Stream: new members

Topic: problems with paths


view this post on Zulip Tianchen Zhao (Feb 22 2021 at 19:44):

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

view this post on Zulip Alex J. Best (Feb 22 2021 at 20:37):

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.

view this post on Zulip Alex J. Best (Feb 22 2021 at 20:38):

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?

view this post on Zulip Bryan Gin-ge Chen (Feb 22 2021 at 20:42):

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

view this post on Zulip Rob Lewis (Feb 22 2021 at 20:44):

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)

view this post on Zulip Rob Lewis (Feb 22 2021 at 20:44):

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

view this post on Zulip Alex J. Best (Feb 22 2021 at 20:57):

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)

view this post on Zulip Julian Berman (Feb 22 2021 at 20:58):

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

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 15:29):

(deleted)

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 15:32):

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

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 15:37):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2021 at 15:49):

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!

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 17:06):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2021 at 17:08):

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.

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 17:10):

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

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 17:10):

But moot if you can't access github

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 17:35):

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.

view this post on Zulip Tianchen Zhao (Feb 24 2021 at 17:35):

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!

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 19:54):

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

view this post on Zulip Tianchen Zhao (Feb 25 2021 at 04:21):

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.

view this post on Zulip Tianchen Zhao (Feb 25 2021 at 07:23):

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!


Last updated: May 10 2021 at 00:31 UTC