Zulip Chat Archive

Stream: general

Topic: install

Michael Aragon (Aug 03 2021 at 16:11):

I am following the instructions to install LEAN on my PC from https://leanprover-community.github.io/install/windows.html. However, I am getting an error when trying to follow step 2 under "Installing elan".

This is the error I get. Could this be due to a security restriction since I am working on my company PC?
curl: (60) SSL certificate problem: self signed certificate in certificate chain
More details here: https://curl.se/docs/sslcerts.html

curl failed to verify the legitimacy of the server and therefore could not
establish a secure connection to it. To learn more about this situation and
how to fix it, please visit the web page mentioned above.

Julian Berman (Aug 04 2021 at 08:44):

Yes, that seems likely. Is that the full error you see, I forget if elan will tell you what URL it's trying to hit (but it's probably one on raw.githubusercontent.com)

Julian Berman (Aug 04 2021 at 08:44):

Oh, never mind that, that step is a curl command.

Julian Berman (Aug 04 2021 at 08:45):

If you go to https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh in a browser, do you see something? Probably you will, in which case you're correct, your employer is man-in-the-middling you :)

jgrecbio (Aug 07 2021 at 17:11):

Hello all, sorry if this is not the place to ask this question,
But has anyone tried to install lean3 on macOS with a M1 chip ?

jgrecbio (Aug 07 2021 at 17:12):

I was able to install lean4, but without the support of matlib, it does seem less useful

Patrick Massot (Aug 07 2021 at 17:24):

Yes, you can search this forum for M1.

Last updated: Aug 03 2023 at 10:10 UTC