install

Stream: general

[Michael Aragon]

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]

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]

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

[Julian Berman]

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]

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]

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

[Patrick Massot]

Yes, you can search this forum for M1.