Cache Get Failed: Unable to get local issuer SSL certificate

Stream: general

[Riyaz Ahuja]

Hello, I'm trying to unpack the cached Mathlib so that I don't have to lake build the whole thing. Usually on my local machine, I can lake exe cache get and there is no problems, but I'm trying to get this running now on a remote SLURM computing cluster, where when I run the same command on a fresh install of lean, I get:

Attempting to download 5826 file(s)
SSL certificate problem: unable to get local issuer certificate
Downloaded: 0 file(s) [attempted 1/5826 = 0%], 1 failedSSL certificate problem: unable to get local issuer certificate
Downloaded: 0 file(s) [attempted 2/5826 = 0%], 2 failedSSL certificate problem: unable to get local issuer certificate
[...]

Other than this one issue, Lean works perfectly fine on the cluster, so I am wondering if there is any other way to get mathlib unpacked on the cluster without having to build the whole thing from scratch? Or if there is any additional commands (perhaps a curl?) that lake exe cache get is running behind the scenes that I can use to troubleshoot more and/or send to my administrator to get the certificate fixed.

Thanks

[Kim Morrison]

Yes, it is running behind the scenes. You could probably modify the file Cache/IO.lean in Mathlib to bring the curl commands it executes.

[Riyaz Ahuja]

I see, thanks! It ended up being because the <- getCurl in runCurlStreaming was pointing to some cached curl binary in the cluster, rather than the one I installed via conda. Weird issue, but as long as it works and I don't need to wait 2 hours for mathlib to build, I'm happy :)