leanproject new gives SSLError

Stream: new members

[Zhang Ruichong]

Thank you for your timely response, but I do not really understand.
image.png
There is neither a folder named "test" nor "test/project".

[Eric Wieser]

@Zhang Ruichong, I've moved your message; I was replying to @Strahinja Strahinja here not you.

[Eric Wieser]

Did the tutorial project work fine for you?

[Eric Wieser]

I believe that you didn't read the "You can now read instructions about creating and working on" instructions at the botom of the windows install page, https://leanprover-community.github.io/install/windows.html#lean-projects

[Zhang Ruichong]

Well, I have read it
but it showed this

$ leanproject new project1

cd project1
git init -q
git checkout -b lean-3.42.1
Switched to a new branch 'lean-3.42.1'
configuring project1 0.1
HTTPSConnectionPool(host='raw.githubusercontent.com', port=443): Max retries exceeded with url: /leanprover-community/mathlib/master/leanpkg.toml (Caused by SSLError(SSLEOFError(8, 'EOF occurred in violation of protocol (_ssl.c:1123)')))

I guess that it was requiring mathlib from GitHub, but due to some reason the connection failed, so I'm actually running a project without mathlib. Am I correct?

[Kevin Buzzard]

Is this a great firewall of China problem?

[Eric Wieser]

Well, I have read it, but it showed this

Great! In general, if you follow our instructions and they don't work, it's better to show us how they fail, than to try something else and then show us how _that_ fails

[Eric Wieser]

Zhang Ruichong said:

I'm actually running a project without mathlib. Am I correct?

You're running a project which our tools failed to configure correctly, so there's no guarantees your project is valid at all once the error appears.

[Zhang Ruichong]

Almost surely is the firewall problem :(
Have to use a proxy
Some tools such as Edge browser and Git can recognize proxy and use it, but some can't.

[Eric Wieser]

Perhaps that's something we can fix

[Eric Wieser]

(such as by folowing the approach at https://stackoverflow.com/a/16311657/102441)

[Zhang Ruichong]

github.com is not fully blocked in China
It's only a DNS pollution, so we can access it by 140.82.112.4 directly

[Eric Wieser]

But on your system, git can access github.com by name by automatically using a system-wide proxy?

[Eric Wieser]

If so, then we should make mathlibtools do that too

[Zhang Ruichong]

Seems so, I rarely use Git so I haven't checked

[Eric Wieser]

What does python3 -c "import urllib.request; print(len(urllib.request.getproxies()))" give on your system? (you might need to replace python3 with py -3 if you're on windows)

[Zhang Ruichong]

Python 3.9.1 (tags/v3.9.1:1e5d33e, Dec 7 2020, 17:08:21) [MSC v.1927 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license()" for more information.

import urllib.request
urllib.request.getproxies()
{'http': 'http://127.0.0.1:3456', 'https': 'https://127.0.0.1:3456', 'ftp': 'ftp://127.0.0.1:3456'}
len(urllib.request.getproxies())
3

[Eric Wieser]

Having looked more closely, I'd expect that to just work; requests should respect the system proxies by default

[Eric Wieser]

Although I'm a bit uncertain whether you're allowed to proxy http and https traffic via the same port