Zulip Chat Archive

Stream: general

Topic: leanproject get-c SSL issue

Yakov Pechersky (Jan 17 2021 at 16:58):

 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 (Jan 17 2021 at 16:58):

Is anyone else getting that?

Rob Lewis (Jan 17 2021 at 16:59):

Working fine for me

Miles (Jan 17 2021 at 17:00):

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 (Jan 17 2021 at 17:07):

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

Julian Berman (Jan 17 2021 at 19:05):

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 (Jan 17 2021 at 19:05):

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)

Last updated: Aug 03 2023 at 10:10 UTC