leanproject get-c SSL issue

Stream: general

[Yakov Pechersky]

❯ leanproject get-c
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/0796941b7f84eaee8d395e0e30fc967c67fc4ea1.tar.xz to /home/yakov/.mathlib/0796941b7f84eaee8d395e0e30fc967c67fc4ea1.tar.xz
HTTPSConnectionPool(host='oleanstorage.azureedge.net', port=443): Max retries exceeded with url: /mathlib/0796941b7f84eaee8d395e0e30fc967c67fc4ea1.tar.xz (Caused by SSLError(SSLError("bad handshake: Error([('SSL routines', 'tls_process_server_certificate', 'certificate verify failed')])")))

[Yakov Pechersky]

Is anyone else getting that?

[Rob Lewis]

Working fine for me

[Miles]

I didn't get that specific error, but from past experience that usually means either your security certificate is expired, it's not on your PATH/can't be found, Lean doesn't know how to use it, or you're using some kind of VPN/proxy for which it isn't valid.

[Gabriel Ebner]

Another possibility is that the date/time is set incorrectly on your computer.

[Julian Berman]

That error comes from openssl, so if you get it you usually can/should run e.g. openssl s_client -connect oleanstorage.azureedge.net:443 and it will give you more information

[Julian Berman]

If you ever suspect it's not your issue though, ssllabs is a good way to confirm -- https://www.ssllabs.com/ssltest/ (stick the domain name in the box, it will tell you if it thinks SSL is valid after a few minutes)