Zulip Chat Archive

Stream: general

Topic: installing elan


Michael Beeson (Apr 10 2020 at 23:41):

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 (Apr 11 2020 at 00:04):

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 (Apr 11 2020 at 00:05):

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 (Apr 11 2020 at 00:17):

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 (Apr 11 2020 at 00:20):

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

Michael Beeson (Apr 11 2020 at 00:24):

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 (Apr 11 2020 at 00:31):

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 (Apr 11 2020 at 00:39):

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 (Apr 11 2020 at 00:41):

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 (Apr 11 2020 at 00:41):

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 (Apr 11 2020 at 00:51):

also, try curl -V (uppercase) instead

Michael Beeson (Apr 11 2020 at 00:51):

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 (Apr 11 2020 at 01:38):

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 (Apr 11 2020 at 05:31):

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

Johan Commelin (Apr 11 2020 at 05:31):

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

Scott Morrison (Apr 11 2020 at 09:14):

I'll go take them down.

Parker Friedland (Jan 01 2025 at 02:53):

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 (Jan 01 2025 at 03:04):

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 (Jan 01 2025 at 03:05):

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

Parker Friedland (Jan 01 2025 at 03:14):

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

Parker Friedland (Jan 01 2025 at 03:15):

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 (Jan 01 2025 at 03:35):

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 (Jan 01 2025 at 03:37):

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

Parker Friedland (Jan 01 2025 at 03:40):

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 (Jan 01 2025 at 03:56):

all good works now


Last updated: May 02 2025 at 03:31 UTC