installing elan

Stream: general

[Michael Beeson]

When I give the approved installation command (on a Mac)
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
I get an error about an expired SSL certificate. Hence I cannot install the Lean prover.
Help!

[Bryan Gin-ge Chen]

The approved installation instructions on a Mac are here (perhaps you're already following them). The expired SSL certificate error is very strange though; I can't reproduce it.

[Alex J. Best]

I can't reproduce this either, but according to https://stackoverflow.com/questions/18964175/how-to-fix-curl-60-ssl-certificate-invalid-certificate-chain it seems if you download https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh by hand and edit all calls to curl in that script to add -k. and then run it with cat elan-init.sh | sh it might work. (when I say edit calls to curl I mean the lines like ensure curl -sSf should be changed to ensure curl -sSfk.)

[Michael Beeson]

I found that some people had a similar problem on Linux and fixed it using something like
sudo apt-get ca-certificates. But I don't know the Mac OS analogue. (brew ca-certificates didn't work.)

[Bryan Gin-ge Chen]

Are you able to open https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh in your browser?

[Michael Beeson]

Yes, I can open that script, and I tried editing it as someone suggested above to add the -k option, but that produced a different error, namely,
curl: (35) error:1407742E:SSL routines:SSL23_GET_SERVER_HELLO:tlsv1 alert protocol version
elan: command failed: curl -sSfk https://github.com/Kha/elan/releases/latest
curl: (35) error:1407742E:SSL routines:SSL23_GET_SERVER_HELLO:tlsv1 alert protocol version
elan: command failed: curl -sSfLk https://github.com/Kha/elan/releases/download//elan-x86_64-apple-darwin.tar.gz -o /var/folders/_b/h558g4210fx_2cchc9p4d6c00000gn/T/tmp.0tDPbhOl/elan-init.tar.gz

[Alex J. Best]

Maybe updating curl by reinstalling it using homebrew (https://brew.sh/) would help, if it isn't already up to date. What does curl -v output?

[Michael Beeson]

reinstalled curl using brew, no change in the error messages,
:beer: /usr/local/Cellar/curl/7.69.1: 459 files, 3.2MB
iMac:Documents beeson$ curl -v
curl: no URL specified!
curl: try 'curl --help' or 'curl --manual' for more information

[Michael Beeson]

Also tried exporting a certificate file from Keychain and passing it to curl with the -file option, which however
was not recognized. Mac usually uses keychain rather than certificate files but can export them.

[Pit Sinning]

I think it might be that you're using a deprecated OpenSSL version. Or perhaps you need to update your root CAs https://curl.haxx.se/docs/caextract.html
I'm unsure how Mac OS handles CAs though.

[Pit Sinning]

also, try curl -V (uppercase) instead

[Michael Beeson]

OK so I finally went to GitHub and downloaded elan directly, and that worked. So now I have Lean installed. Thanks for trying to help me. Too bad it didn't work for me like in Scott's nice video.

[Scott Morrison]

Sorry about the video. It may well be out of date. I now longer have my (virtual) windows machine sitting around, so it's nontrivial for me to verify it. If someone tells me they've tested it and it's now wrong, I'll take it down.

[Johan Commelin]

@Scott Morrison I think the problem is the Mac installation video

[Johan Commelin]

I guess both of them are quite out of date nowadays....

[Scott Morrison]

I'll go take them down.