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.

[Parker Friedland]

When installing Elan in VSCode using the guide https://lean-lang.org/lean4/doc/quickstart.html
I get

PS C:\Users\parke\Downloads\Lean4_ProofVerification> Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -Destination "elan-init.ps1" PS C:\Users\parke\Downloads\Lean4_ProofVerification> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
PS C:\Users\parke\Downloads\Lean4_ProofVerification> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable info: downloading installer to C:\Users\parke\AppData\Local\Temp\ error: could not create link from 'C:\Users\parke.elan\bin\elan.exe' to 'C:\Users\parke.elan\bin\lake.exe'
Elan failed with error code 1 PS C:\Users\parke\Downloads\Lean4_ProofVerification> Write-Host "elan-init returned [$rc]" elan-init returned [1]

[Parker Friedland]

The first time I installed Ellan I think I didn't get this error it said return [0] but then when opening Main.lean in a new project I got

c:\Users\parke\.elan\toolchains\leanprover--lean4---stable\bin\lake.exe setup-file C:/Users/parke/Downloads/Lean4_ProofVerification/Main.lean Init Lean4ProofVerification failed:

stderr:
error: missing manifest; use lake update to generate one
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

So I asked QwQ (open source llm) for help and it said after telling me to update the VSCode settings.json by adding

`    "terminal.integrated.env.windows": {        "PATH": "${env:PATH};C:\\path\\to\\elan"    }`

(which I did) to check if elan was installed using sh
elan --version

which returned sh: elan: command not found

So I installed Elan again from the guide and that is the point at which I get this error.

[Parker Friedland]

though maybe it gave the same error the first time and I just missed it?

[Parker Friedland]

should I remove
"terminal.integrated.env.windows": { "PATH": "${env:PATH};C:\path\to\elan" }
?

[Parker Friedland]

though I still had the error

c:\Users\parke\.elan\toolchains\leanprover--lean4---stable\bin\lake.exe setup-file C:/Users/parke/Downloads/Lean4_ProofVerification/Main.lean Init Lean4ProofVerification failed: stderr: error: missing manifest; use lake update to generate one Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

before this

[Parker Friedland]

ah I see

"PATH": "${env:PATH};C:\path\to\elan"

should be

"PATH": "${env:PATH};C:\Users\parke\.elan\bin"

forgot to change that

[Parker Friedland]

nope same error tho I really should have put in the correct path

[Parker Friedland]

or kind of, I get the same error when installing elan but running elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

shows it is installed now

[Parker Friedland]

all good works now