Zulip Chat Archive

Stream: new members

Topic: installing mathlib on win10

Chennes (Jul 14 2023 at 02:42):

I am stuck at this step of first step of "Creating a Lean project" (https://leanprover-community.github.io/install/project.html)
image.png

Chennes (Jul 14 2023 at 02:44):

I have installed lean4 succfully to have the result of #eval 18 + 19 in https://leanprover-community.github.io/install/windows.html

Scott Morrison (Jul 14 2023 at 04:57):

This is an SSL problem. Can you connect to https sites (particularly github) normally? Are you behind a restrictive firewall?

Chennes (Jul 14 2023 at 05:10):

OK. I can connect to github and I successfully cloned "git clone https://github.com/leanprover-community/mathematics_in_lean." in the first step "Working on an existing project", although I am behind GFW :joy:

Chennes (Jul 14 2023 at 05:15):

@Scott Morrison In fact I come up with anther question:

As we finish the steps in "Working on an existing project", could we just import mathlib to check in MIT document?
However I failed in the following situation.

image.png

Scott Morrison (Jul 14 2023 at 05:16):

I'm sorry, I don't understand your question.

Last updated: Dec 20 2023 at 11:08 UTC