openssl error when running `lake exe cache get`

Stream: general

[Miguel Marco]

I am trying to start a lean project in a computing cluster, and I get the following error when running lake exe cache get:

Attempting to download 4014 file(s)
OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 1/4014 = 0%], 1 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 2/4014 = 0%], 2 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 3/4014 = 0%], 3 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
...

Any idea of what could be the problem?

[Mario Carneiro]

does it work to call curl directly to download a file?

[Mario Carneiro]

e.g.

curl https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar

[Mario Carneiro]

also try adding -v and show the error message

[Mario Carneiro]

what I get

$ curl https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar -v
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0*   Trying 20.150.95.196:443...
* Connected to lakecache.blob.core.windows.net (20.150.95.196) port 443 (#0)
* ALPN, offering h2
* ALPN, offering http/1.1
*  CAfile: /etc/ssl/certs/ca-certificates.crt
*  CApath: /etc/ssl/certs
* TLSv1.0 (OUT), TLS header, Certificate Status (22):
} [5 bytes data]
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
} [512 bytes data]
* TLSv1.2 (IN), TLS header, Certificate Status (22):
{ [5 bytes data]
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0* TLSv1.3 (IN), TLS handshake, Server hello (2):
{ [85 bytes data]
* TLSv1.2 (IN), TLS handshake, Certificate (11):
{ [5254 bytes data]
* TLSv1.2 (IN), TLS handshake, Server key exchange (12):
{ [365 bytes data]
* TLSv1.2 (IN), TLS handshake, Server finished (14):
{ [4 bytes data]
* TLSv1.2 (OUT), TLS header, Certificate Status (22):
} [5 bytes data]
* TLSv1.2 (OUT), TLS handshake, Client key exchange (16):
} [102 bytes data]
* TLSv1.2 (OUT), TLS header, Finished (20):
} [5 bytes data]
* TLSv1.2 (OUT), TLS change cipher, Change cipher spec (1):
} [1 bytes data]
* TLSv1.2 (OUT), TLS header, Certificate Status (22):
} [5 bytes data]
* TLSv1.2 (OUT), TLS handshake, Finished (20):
} [16 bytes data]
* TLSv1.2 (IN), TLS header, Finished (20):
{ [5 bytes data]
* TLSv1.2 (IN), TLS header, Certificate Status (22):
{ [5 bytes data]
* TLSv1.2 (IN), TLS handshake, Finished (20):
{ [16 bytes data]
* SSL connection using TLSv1.2 / ECDHE-RSA-AES256-GCM-SHA384
* ALPN, server did not agree to a protocol
* Server certificate:
*  subject: C=US; ST=WA; L=Redmond; O=Microsoft Corporation; CN=*.blob.core.windows.net
*  start date: Nov 20 00:42:40 2023 GMT
*  expire date: Jun 27 23:59:59 2024 GMT
*  subjectAltName: host "lakecache.blob.core.windows.net" matched cert's "*.blob.core.windows.net"
*  issuer: C=US; O=Microsoft Corporation; CN=Microsoft Azure TLS Issuing CA 01
*  SSL certificate verify ok.
* TLSv1.2 (OUT), TLS header, Supplemental data (23):
} [5 bytes data]
> GET /mathlib4/f/7d56bc4bb976be8d.ltar HTTP/1.1
> Host: lakecache.blob.core.windows.net
> User-Agent: curl/7.81.0
> Accept: */*
>
* TLSv1.2 (IN), TLS header, Supplemental data (23):
{ [5 bytes data]
* Mark bundle as not supporting multiuse
< HTTP/1.1 200 OK
< Content-Length: 3415
< Content-Type: application/octet-stream
< Content-MD5: 4hT1W1Edt739hfMG5CG7oA==
< Last-Modified: Fri, 17 Nov 2023 11:48:53 GMT
< ETag: 0x8DBE7632C53A08E
< Server: Windows-Azure-Blob/1.0 Microsoft-HTTPAPI/2.0
< x-ms-request-id: c506cae5-601e-002b-1ac1-2d4477000000
< x-ms-version: 2009-09-19
< x-ms-lease-status: unlocked
< x-ms-blob-type: BlockBlob
< Date: Wed, 13 Dec 2023 12:42:02 GMT
<
{ [3415 bytes data]
100  3415  100  3415    0     0   4454      0 --:--:-- --:--:-- --:--:--  4452
* Connection #0 to host lakecache.blob.core.windows.net left intact

[Miguel Marco]

I get this

[mmarco@gauss test]$ curl https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar -v
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0* Trying 20.150.95.196...
* TCP_NODELAY set
* Connected to lakecache.blob.core.windows.net (20.150.95.196) port 443 (#0)
0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0* ALPN, offering h2
* ALPN, offering http/1.1
* successfully set certificate verify locations:
* CAfile: /etc/pki/tls/certs/ca-bundle.crt
CApath: none
} [5 bytes data]
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
} [512 bytes data]
* TLSv1.3 (IN), TLS handshake, Server hello (2):
{ [85 bytes data]
* TLSv1.2 (IN), TLS handshake, Certificate (11):
{ [5254 bytes data]
* TLSv1.2 (IN), TLS handshake, Server key exchange (12):
{ [365 bytes data]
* TLSv1.2 (IN), TLS handshake, Server finished (14):
{ [4 bytes data]
* TLSv1.2 (OUT), TLS handshake, Client key exchange (16):
} [102 bytes data]
* TLSv1.2 (OUT), TLS change cipher, Change cipher spec (1):
} [1 bytes data]
* TLSv1.2 (OUT), TLS handshake, Finished (20):
} [16 bytes data]
* TLSv1.2 (IN), TLS handshake, Finished (20):
{ [16 bytes data]
* SSL connection using TLSv1.2 / ECDHE-RSA-AES256-GCM-SHA384
* ALPN, server did not agree to a protocol
* Server certificate:
* subject: C=US; ST=WA; L=Redmond; O=Microsoft Corporation; CN=*.blob.core.windows.net
* start date: Nov 20 00:42:40 2023 GMT
* expire date: Jun 27 23:59:59 2024 GMT
* subjectAltName: host "lakecache.blob.core.windows.net" matched cert's "*.blob.core.windows.net"
* issuer: C=US; O=Microsoft Corporation; CN=Microsoft Azure TLS Issuing CA 01
* SSL certificate verify ok.
} [5 bytes data]

GET /mathlib4/f/7d56bc4bb976be8d.ltar HTTP/1.1
Host: lakecache.blob.core.windows.net
User-Agent: curl/7.61.1
Accept: /

{ [5 bytes data]
< HTTP/1.1 200 OK
< Content-Length: 3415
< Content-Type: application/octet-stream
< Content-MD5: 4hT1W1Edt739hfMG5CG7oA==
< Last-Modified: Fri, 17 Nov 2023 11:48:53 GMT
< ETag: 0x8DBE7632C53A08E
< Server: Windows-Azure-Blob/1.0 Microsoft-HTTPAPI/2.0
< x-ms-request-id: dfa43897-501e-0023-75ce-2d5f04000000
< x-ms-version: 2009-09-19
< x-ms-lease-status: unlocked
< x-ms-blob-type: BlockBlob
< Date: Wed, 13 Dec 2023 14:16:04 GMT
<
{ [3415 bytes data]
100 3415 100 3415 0 0 4949 0 --:--:-- --:--:-- --:--:-- 4942
* Connection #0 to host lakecache.blob.core.windows.net left intact

[Jason Rute]

Does anyone know the solution to this? I'm getting the exact same error as the top. I can also perform @Mario Carneiro 's curl command without problem. I'm also on a compute cluster, which I'm sure is part of it. It could just be a permissions/firewall thing, but why these files and not others? (I also don't know which files curl is complaining about downloading.)

[Jason Rute]

If it is helpful: https://github.com/curl/curl/issues/10702

[Julian Berman]

I don't see any immediate obvious cause from scanning what Cache/Requests.lean does.

[Julian Berman]

Can you show type -a curl perhaps as a left field guess.

[Jason Rute]

@Julian Berman:

$ type -a curl
curl is /usr/bin/curl
curl is /bin/curl
curl is /usr/bin/curl

[Mario Carneiro]

what message do you get with the direct download?

[Julian Berman]

OK, so my ~10% likely guess is maybe a different curl is being used for one or the other. Can you try Mario's command but replace curl explicitly with /usr/bin/curl and then /bin/curl?

[Julian Berman]

Mario Carneiro said:

what message do you get with the direct download?

I think they're saying it works fine and the file downloads.

[Jason Rute]

I'll try that. Also here is a full reproduction where I make a new project with lake new myproject math and run lean exe cache get. It seems like some stuff downloads, but then it gets to a point where it errs:

$ lake new test_project_math math
$ cd test_project_math/
$ lake exe cache get
info: downloading component 'lean'
153.6 MiB / 153.6 MiB (100 %)  12.6 MiB/s ETA:   0 s
info: installing component 'lean'
info: test_project_math: no previous manifest, creating one from scratch
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to './.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to './.lake/packages/importGraph'
warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'
info: mathlib: running post-update hooks
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
installing leantar 0.1.11
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100 1906k  100 1906k    0     0  5139k      0 --:--:-- --:--:-- --:--:-- 5139k

Attempting to download 4208 file(s)
OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 1/4208 = 0%], 1 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 2/4208 = 0%], 2 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 3/4208 = 0%], 3 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
Downloaded: 0 file(s) [attempted 4/4208 = 0%], 4 failedOpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme

[Mario Carneiro]

After running this, is there a ~/.cache/mathlib/curl.cfg file?

[Mario Carneiro]

if so you could try re-running the curl command that cache uses

[Jason Rute]

The head of ~/.cache/mathlib/curl.cfg looks like this:

url = https://lakecache.blob.core.windows.net/mathlib4/f/63693f3c2d08d318.ltar
-o "/u/jasonrute/.cache/mathlib/63693f3c2d08d318.ltar.part"
url = https://lakecache.blob.core.windows.net/mathlib4/f/a89f099760a13f5b.ltar
-o "/u/jasonrute/.cache/mathlib/a89f099760a13f5b.ltar.part"
url = https://lakecache.blob.core.windows.net/mathlib4/f/87d92ae0d8d8646d.ltar
-o "/u/jasonrute/.cache/mathlib/87d92ae0d8d8646d.ltar.part"
url = https://lakecache.blob.core.windows.net/mathlib4/f/7085d882c5487719.ltar
-o "/u/jasonrute/.cache/mathlib/7085d882c5487719.ltar.part"
url = https://lakecache.blob.core.windows.net/mathlib4/f/4f4c3ec5261651a0.ltar
-o "/u/jasonrute/.cache/mathlib/4f4c3ec5261651a0.ltar.part"

What should I try running?

[Mario Carneiro]

curl \
  --request GET \
  --parallel \
  --fail \
  --silent \
  --retry 5 \
  --write-out "%{json}\n" \
  --config ~/.cache/mathlib/curl.cfg

[Mario Carneiro]

maybe without the --silent and --write-out "%{json}\n"

[Jason Rute]

That seems to be downloading something. (I also had to remove --parallel since it didn't recognize that parameter.)

[Miguel Marco]

Trying that i get

curl: option --parallel: is unknown
curl: try 'curl --help' or 'curl --manual' for more information

[Julian Berman]

What happens/happened when you tried /bin/curl?

[Mario Carneiro]

Oh, in that case you should be using the downloaded curl

[Julian Berman]

Oh -- it downloads its own third curl?

[Mario Carneiro]

which should be in ~/.cache/mathlib/curl-7.88.1

[Mario Carneiro]

It downloads curl if the system curl is too old

[Julian Berman]

Does it compile curl on the machine?

[Julian Berman]

If not probably that will fail in these kinds of cases where I bet they've changed the CA bundle

[Jason Rute]

Yes, that is the problem:

$ ~/.cache/mathlib/curl-7.88.1 https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
curl: (35) OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme

[Mario Carneiro]

no, it downloads it from https://github.com/leanprover-community/static-curl

[Julian Berman]

Yeah I don't think that will work if someone's compiled some curl on the machine that has a different CA bundle somewhere with whatever certs they're using to MITM the requests

[Mario Carneiro]

interesting, why would that be baked into the executable?

[Julian Berman]

I think it's done at compile time, but I am no curl expert, I just googled it

[Mario Carneiro]

I would have assumed the certs are coming from some system directory

[Julian Berman]

"Add the CA cert for your server to the existing default CA certificate store. The default CA certificate store can be changed at compile time with the following configure options:

--with-ca-bundle=FILE: use the specified file as the CA certificate store. CA certificates need to be concatenated in PEM format into this file."

from https://curl.se/docs/sslcerts.html

[Mario Carneiro]

is there a way to say "don't use the builtin certs"?

[Julian Berman]

Mario Carneiro said:

I would have assumed the certs are coming from some system directory

That's certainly the normal behavior but you can change it

[Julian Berman]

Mario Carneiro said:

is there a way to say "don't use the builtin certs"?

I think that will fail in other ways no? It's being done presumably because they're MITM'ing the HTTPS traffic, and they're adding their root cert. But we haven't seen the real error yet.

[Julian Berman]

I think that dumb openssl error is a way of saying it can't read the right cert store directory, from other googling

[Julian Berman]

@Jason Rute I don't know what the exact right command to run is yet, but can you try perhaps showing us openssl s_client -showcerts -connect lakecache.blob.core.windows.net:443

[Jason Rute]

I'm not sure what is in that output and since it has a lot of keys, I'm hesitant to share it here without understanding it better. What are you looking for in it?

[Julian Berman]

Yes, sorry, that's a good concern of course. They should all be public keys. I'm looking for the names of the certs that are used in connecting to that.

[Julian Berman]

there should be some way of asking you for that without the public keys

[Julian Berman]

but when I run that, the first cert I see is...

[Julian Berman]

ah it's just at the top. So I see:

CONNECTED(00000006)
depth=2 C=US, O=DigiCert Inc, OU=www.digicert.com, CN=DigiCert Global Root G2
verify return:1
depth=1 C=US, O=Microsoft Corporation, CN=Microsoft Azure TLS Issuing CA 01
verify return:1
depth=0 C=US, ST=WA, L=Redmond, O=Microsoft Corporation, CN=*.blob.core.windows.net

[Julian Berman]

do you see something like that? Two microsoft certs and a DigiCert root cert? Or do you see some other certificate that presumably is self-signed maybe

[Jason Rute]

That part is the same.

[Jason Rute]

Well different CONNECTED number. I assume that doesn't matter.

[Julian Berman]

Hrm. And does type -a openssl have more than one result?

[Julian Berman]

Bleh surely there's a way to get curl to print this out too, that's probably smarter since that's what we know doesn't work.

[Julian Berman]

Aha looks like it's --write-out {certs}

[Julian Berman]

(Sorry, clearly still guessing here) but two other things to try are to add --ca-native to the curl commands to see what happens if you try to force curl to use the system CA store -- both the system one and the lean one

[Jason Rute]

Yes, there are many results for type -a openssl. (The default was from my base conda installation.)

[Julian Berman]

so run ~/.cache/mathlib/curl-7.88.1 --ca-native https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar

[Mario Carneiro]

oh right, did we confirm that that one also fails with the downloaded curl?

[Jason Rute]

$ ~/.cache/mathlib/curl-7.88.1 --ca-native https://lakecache.blob.core.windows.net/mathlib4/f/7d56bc4bb976be8d.ltar --output out.ltar
curl: option --ca-native: is unknown
curl: try 'curl --help' for more information

[Julian Berman]

Hrm, ok, guess that's new in curl 8

[Julian Berman]

let's see what curl 7 has :/

[Julian Berman]

I am now somewhat sure this is the problem (some different CA bundle being used than the one your cluster owners were trying to force curl to use) but we have to find where that bundle is I think, and I've got to run for a bit, but can come back later if you don't figure it out

[Julian Berman]

export CURL_CA_BUNDLE=/etc/ssl/certs/ca-certificates.crt that looks like the other way to do this

[Julian Berman]

But that path won't be right for your system

[Jason Rute]

Okay, here is a hack that works for me. cc @Miguel Marco:

1. Delete ~/.cache/mathlib/curl-7.88.1
2. Install an updated curl. Since my system is locked down, I make a conda environment and installed conda install curl into it.

Then it works. (The first step seems important. It is not just enough to update curl.)

[Jason Rute]

It also means if I ever forget and run it without being in my environment it will install the bad curl and I will have to delete it.

[Mario Carneiro]

Does compiling it using nix work? There are some build instructions at https://github.com/leanprover-community/static-curl but I don't really know whether they include local certs or something

[Jason Rute]

I have to go soon, but I'll try that later.

[Jason Rute]

Actually, I realize I don't understand nix. It is sort of like conda right? Do you create an nix environment or something and install curl into that? Also you are talking about just installing curl through nix right? (I remember a while ago there was talk about installing Lean through nix.)

[Mario Carneiro]

I also don't have any first-hand experience with nix, maybe @Sebastian Ullrich can say more about how that line works. My understanding is that you can use nix-shell to enter a nix environment and then there is some content addressed build store you can make use of with nix build

[Mario Carneiro]

that said I have no idea what sources or what build script corresponds to github:NixOS/nixpkgs/8f40f2f90b9c9032d1b824442cfbbe0dbabd0dbd#pkgsStatic.curl

[Mario Carneiro]

my best guess is https://github.com/NixOS/nixpkgs/blob/8f40f2f90b9c9032d1b824442cfbbe0dbabd0dbd/pkgs/tools/networking/curl/default.nix

[Julian Berman]

Jason Rute said:

It also means if I ever forget and run it without being in my environment it will install the bad curl and I will have to delete it.

you can evade this at least with another (arguable nonhack), namely link your updated curl into ~/.local/bin and ensure that that is early on your PATH.

[Mario Carneiro]

it appears that --without-ca-bundle is set only when building on OSX

[Julian Berman]

I don't know conda unfortunately, but I would bet there's a tool in its ecosystem that does this.

[Julian Berman]

Julian Berman said:

Jason Rute said:

It also means if I ever forget and run it without being in my environment it will install the bad curl and I will have to delete it.

you can evade this at least with another (arguable nonhack), namely link your updated curl into ~/.local/bin and ensure that that is early on your PATH.

(In case the thinking emoji is confusion) -- the point is you want anything to find your newer curl before it finds the older one, and you want that to happen globally, not just in your conda env.

[Julian Berman]

I can look again at how to find your bundle if that's helpful, but if you're happy with your hack it sounds reasonable to me to move on with life

[Jason Rute]

The emoji was just that I think there is a slightly better way to do that, but ~/.local/bin is a good idea. I could also just just upgrade curl in my base conda environment (although I don't like having the base environment on since it is easy to accidentally conda install stuff into it thinking you are in your custom environment.) But the fact that lake exe cache get by default uses this "broken" curl it downloaded is a bit annoying even when I've upgraded my system curl.

[Mario Carneiro]

it won't download the broken curl if you have a good version

[Sebastian Ullrich]

So do we know which curl is using which certificate?

[Julian Berman]

Jason can you try one more thing (now or later) -- run strace -e trace=open ~/.cache/mathlib/curl-7.88.1 https://lakecache.blob.core.windows.net/ which should tell us where that curl is looking -- at least then maybe we can get the error message to change and show us the "real" error

[Julian Berman]

Sebastian Ullrich said:

So do we know which curl is using which certificate?

no but ^ may help

[Mario Carneiro]

also --write-out {certs} still hasn't been tested

[Julian Berman]

Yeah I'm less excited about that one now though because the man page says it only works when the transfer completes

[Julian Berman]

But you can try that too.

[Jason Rute]

$ strace -e trace=open ~/.cache/mathlib/_curl-7.88.1 https://lakecache.blob.core.windows.net/
open("/./nix/store/6k1wq0nhs6vwxj92vdy2hz7cg1f9997p-openssl-static-x86_64-unknown-linux-musl-3.0.8-etc/etc/ssl/openssl.cnf", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/u/jasonrute/.curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/u/jasonrute/.config/curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/etc/passwd", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
open("/etc/ssl/certs/ca-certificates.crt", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
curl: (35) OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
+++ exited with 35 +++

(Note, I moved curl-7.88.1 to _curl-7.88.1.) Also, here it is with a working curl installed through conda:

$ strace -e trace=open curl https://lakecache.blob.core.windows.net/
<?xml version="1.0" encoding="utf-8"?><Error><Code>InvalidQueryParameterValue</Code><Message>Value for one of the query parameters specified in the request URI is invalid.
RequestId:79697fb5-301e-0011-44e4-5907d4000000
Time:2024-02-07T16:44:45.8996568Z</Message><QueryParameterName>comp</QueryParameterName><QueryParameterValue /><Reason /></Error>+++ exited with 0 +++

[Jason Rute]

(The error in the second one is the same error just running that curl command. (I don't know enough about strace to know if you want me to adjust something here.)

[Julian Berman]

Hrm, yes that second output means it didn't go try to read a file somewhere to find certificates

[Julian Berman]

Have you shown us curl -v https://lakecache.blob.core.windows.net/?

[Julian Berman]

(i.e. with the working one)

[Julian Berman]

that should have the CAfile in it judging from my output

[Jason Rute]

From running that command, it appears the CAfile is in the conda virtual environment folder: CAfile: .../venv/ssl/cacert.pem

[Jason Rute]

(I redacted the rest of the path.)

[Julian Berman]

Does ~/.cache/mathlib/_curl-7.88.1 --cacert /that/conda/env/path/venv/ssl/cacert.pem https://lakecache.blob.core.windows.net/ work?

[Jason Rute]

I get the following:

~/.cache/mathlib/_curl-7.88.1 --cacert /that/conda/env/path/venv/ssl/cacert.pem https://lakecache.blob.core.windows.net/
<?xml version="1.0" encoding="utf-8"?><Error><Code>InvalidQueryParameterValue</Code><Message>Value for one of the query parameters specified in the request URI is invalid.
RequestId:287b8ec2-e01e-0013-5aff-59052e000000
Time:2024-02-07T19:55:25.5334457Z</Message><QueryParameterName>comp</QueryParameterName><Q

[Jason Rute]

I think that means, yes it works.

[Mario Carneiro]

does it work if you set CURL_CA_BUNDLE=/that/conda/env/path/venv/ssl/cacert.pem?

[Miguel Marco]

I guess this hack will not work automatically if i just use the vscode extension to start a new project with mathlib, right?

[Mario Carneiro]

if the env var works then that would just work on new projects etc

[Miguel Marco]

In my case, this works:

[mmarco@nodo01 ~]$ .cache/mathlib/curl-7.88.1 -v https://lakecache.blob.core.windows.net --cacert /etc/ssl/certs/ca-bundle.trust.crt
*   Trying 20.150.95.196:443...
* Connected to lakecache.blob.core.windows.net (20.150.95.196) port 443 (#0)
* ALPN: offers h2,http/1.1
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
*  CAfile: /etc/ssl/certs/ca-bundle.trust.crt
*  CApath: none
* TLSv1.3 (IN), TLS handshake, Server hello (2):
* TLSv1.2 (IN), TLS handshake, Certificate (11):
* TLSv1.2 (IN), TLS handshake, Server key exchange (12):
* TLSv1.2 (IN), TLS handshake, Server finished (14):
* TLSv1.2 (OUT), TLS handshake, Client key exchange (16):
* TLSv1.2 (OUT), TLS change cipher, Change cipher spec (1):
* TLSv1.2 (OUT), TLS handshake, Finished (20):
* TLSv1.2 (IN), TLS handshake, Finished (20):
* SSL connection using TLSv1.2 / ECDHE-RSA-AES256-GCM-SHA384
* ALPN: server did not agree on a protocol. Uses default.
* Server certificate:
*  subject: C=US; ST=WA; L=Redmond; O=Microsoft Corporation; CN=*.blob.core.windows.net
*  start date: Nov 20 00:42:40 2023 GMT
*  expire date: Jun 27 23:59:59 2024 GMT
*  subjectAltName: host "lakecache.blob.core.windows.net" matched cert's "*.blob.core.windows.net"
*  issuer: C=US; O=Microsoft Corporation; CN=Microsoft Azure TLS Issuing CA 01
*  SSL certificate verify ok.
* using HTTP/1.x
> GET / HTTP/1.1
> Host: lakecache.blob.core.windows.net
> User-Agent: curl/7.88.1
> Accept: */*
>
< HTTP/1.1 400 Value for one of the query parameters specified in the request URI is invalid.
< Content-Length: 351
< Content-Type: application/xml
< Server: Microsoft-HTTPAPI/2.0
< x-ms-request-id: 7f249d91-c01e-0040-1701-5a1921000000
< Date: Wed, 07 Feb 2024 20:09:03 GMT
<
<?xml version="1.0" encoding="utf-8"?><Error><Code>InvalidQueryParameterValue</Code><Message>Value for one of the query parameters specified in the request URI is invalid.
RequestId:7f249d91-c01e-0040-1701-5a1921000000
* Connection #0 to host lakecache.blob.core.windows.net left intact

but this doesn't

[mmarco@nodo01 ~]$ CURL_CA_BUNDLE=/etc/ssl/certs/
[mmarco@nodo01 ~]$ .cache/mathlib/curl-7.88.1 -v https://lakecache.blob.core.windows.net
*   Trying 20.150.95.196:443...
* Connected to lakecache.blob.core.windows.net (20.150.95.196) port 443 (#0)
* ALPN: offers h2,http/1.1
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
* TLSv1.3 (IN), TLS handshake, Server hello (2):
* TLSv1.2 (IN), TLS handshake, Certificate (11):
* TLSv1.2 (OUT), TLS alert, unknown CA (560):
* OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
* Closing connection 0
curl: (35) OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme

[Julian Berman]

You need export CURL_CA_BUNDLE

[Miguel Marco]

But this seems to work:

[mmarco@nodo01 ~]$ export CURL_CA_BUNDLE=/etc/ssl/certs/ca-bundle.trust.crt
[mmarco@nodo01 ~]$ .cache/mathlib/curl-7.88.1 -v https://lakecache.blob.core.windows.net
*   Trying 20.150.95.196:443...
* Connected to lakecache.blob.core.windows.net (20.150.95.196) port 443 (#0)
* ALPN: offers h2,http/1.1
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
*  CAfile: /etc/ssl/certs/ca-bundle.trust.crt
*  CApath: none
* TLSv1.3 (IN), TLS handshake, Server hello (2):
* TLSv1.2 (IN), TLS handshake, Certificate (11):
* TLSv1.2 (IN), TLS handshake, Server key exchange (12):
* TLSv1.2 (IN), TLS handshake, Server finished (14):
* TLSv1.2 (OUT), TLS handshake, Client key exchange (16):
* TLSv1.2 (OUT), TLS change cipher, Change cipher spec (1):
* TLSv1.2 (OUT), TLS handshake, Finished (20):
* TLSv1.2 (IN), TLS handshake, Finished (20):
* SSL connection using TLSv1.2 / ECDHE-RSA-AES256-GCM-SHA384
* ALPN: server did not agree on a protocol. Uses default.
* Server certificate:
*  subject: C=US; ST=WA; L=Redmond; O=Microsoft Corporation; CN=*.blob.core.windows.net
*  start date: Nov 20 00:42:40 2023 GMT
*  expire date: Jun 27 23:59:59 2024 GMT
*  subjectAltName: host "lakecache.blob.core.windows.net" matched cert's "*.blob.core.windows.net"
*  issuer: C=US; O=Microsoft Corporation; CN=Microsoft Azure TLS Issuing CA 01
*  SSL certificate verify ok.
* using HTTP/1.x
> GET / HTTP/1.1
> Host: lakecache.blob.core.windows.net
> User-Agent: curl/7.88.1
> Accept: */*
>
< HTTP/1.1 400 Value for one of the query parameters specified in the request URI is invalid.
< Content-Length: 351
< Content-Type: application/xml
< Server: Microsoft-HTTPAPI/2.0
< x-ms-request-id: 6762566a-f01e-002e-0301-5ab008000000
< Date: Wed, 07 Feb 2024 20:11:11 GMT
<
<?xml version="1.0" encoding="utf-8"?><Error><Code>InvalidQueryParameterValue</Code><Message>Value for one of the query parameters specified in the request URI is invalid.
RequestId:6762566a-f01e-002e-0301-5ab008000000
* Connection #0 to host lakecache.blob.core.windows.net left intact
Time:2024-02-07T20:11:12.1860407Z</Message><QueryParameterName>comp</QueryParameterName><QueryParameterValue /><Reason /></Error>

[Julian Berman]

Jason it'd be nice to also see what ls -l that/cert/file is as well -- specifically whether it's a symlink or not

[Julian Berman]

I suppose I was wrong before, it's not that you're being MITM'ed, it's indeed that the statically downloaded curl can't find your certs

[Miguel Marco]

Is there a way to ask curl where is it looking for the certs?

[Julian Berman]

Yes I'm sure there is I just didn't know it offhand and the man page didn't tell me

[Julian Berman]

You ran the same strace as I mentioned above and it didn't say anything either I assume?

[Miguel Marco]

This is interesting: it seems to be looking at the right directory... but apparently doesn't find it:

[mmarco@nodo01 ~]$ strace -e trace=open .cache/mathlib/curl-7.88.1 https://lakecache.blob.core.windows.net/
open("/./nix/store/6k1wq0nhs6vwxj92vdy2hz7cg1f9997p-openssl-static-x86_64-unknown-linux-musl-3.0.8-etc/etc/ssl/openssl.cnf", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.config/curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/etc/passwd", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
open("/etc/ssl/certs/", O_RDONLY|O_LARGEFILE) = 6
open("/etc/ssl/certs/", O_RDONLY|O_LARGEFILE) = 6
open("/etc/ssl/certs/", O_RDONLY|O_LARGEFILE) = 6
curl: (77) error setting certificate file: /etc/ssl/certs/
+++ exited with 77 +++

Maybe it is confusing files and directories?

[Julian Berman]

Did you run that with your environment variable set? Or without?

[Jason Rute]

The strace did say where it was looking: open("/etc/ssl/certs/ca-certificates.crt", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)

[Miguel Marco]

With the environment set. Let me try without it:

[mmarco@nodo01 ~]$ unset  CURL_CA_BUNDLE
[mmarco@nodo01 ~]$ strace -e trace=open .cache/mathlib/curl-7.88.1 https://lakecache.blob.core.windows.net/
open("/./nix/store/6k1wq0nhs6vwxj92vdy2hz7cg1f9997p-openssl-static-x86_64-unknown-linux-musl-3.0.8-etc/etc/ssl/openssl.cnf", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.config/curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/etc/passwd", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
open("/etc/ssl/certs/ca-certificates.crt", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
curl: (35) OpenSSL/3.0.8: error:16000069:STORE routines::unregistered scheme
+++ exited with 35 +++

[Jason Rute]

$ ls -l /the/path/to/my/conda/env/venv/ssl/cacert.pem
-rw-rw-r-- 2 jasonrute jasonrute 292541 Feb  1 22:14 /the/path/to/my/conda/env/venv/ssl/cacert.pem

[Jason Rute]

Doesn't look like a symbolic link.

[Miguel Marco]

This is what I get when I export the specific certificate file (instead of the directory)

[mmarco@nodo01 ~]$ export CURL_CA_BUNDLE=/etc/ssl/certs/ca-bundle.trust.crt
[mmarco@nodo01 ~]$ strace -e trace=open .cache/mathlib/curl-7.88.1 https://lakecache.blob.core.windows.net/
open("/./nix/store/6k1wq0nhs6vwxj92vdy2hz7cg1f9997p-openssl-static-x86_64-unknown-linux-musl-3.0.8-etc/etc/ssl/openssl.cnf", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/home/mmarco/.config/curlrc", O_RDONLY|O_LARGEFILE) = -1 ENOENT (No such file or directory)
open("/etc/passwd", O_RDONLY|O_LARGEFILE|O_CLOEXEC) = 3
open("/etc/ssl/certs/ca-bundle.trust.crt", O_RDONLY|O_LARGEFILE) = 6
<?xml version="1.0" encoding="utf-8"?><Error><Code>InvalidQueryParameterValue</Code><Message>Value for one of the query parameters specified in the request URI is invalid.
RequestId:e2598e19-701e-0034-0403-5a9f67000000
Time:2024-02-07T20:22:28.7884785Z</Message><QueryParameterName>comp</QueryParameterName><QueryParameterValue /><Reason /></Error>+++ exited with 0 +++

[Julian Berman]

Yeah that looks right/fine -- CURL_CA_BUNDLE is meant to be the file, and CURL_CA_PATH probably will work if you set it to the directory

[Julian Berman]

(Certs can either be in a directory or all catted together in one file)

[Julian Berman]

But if one works you're good. Which that looks like it is.

[Julian Berman]

I.e. lake whateeveryouwererunning should also work.

[Miguel Marco]

Thanks, I guess now I would need some tweaking in my install to set the variable when I launch the web version of vscode.

[Jason Rute]

I think curl uses another program curl-config which is supposed to be in the same bin directory as curl to find this stuff. See: https://serverfault.com/a/716313

[Jason Rute]

curl-config --ca will tell you where curl is looking.

[Alex Gu]

Jason Rute said:

Okay, here is a hack that works for me. cc Miguel Marco:

1. Delete ~/.cache/mathlib/curl-7.88.1
2. Install an updated curl. Since my system is locked down, I make a conda environment and installed conda install curl into it.

Then it works. (The first step seems important. It is not just enough to update curl.)

Just wanted to add that I also ran into this exact issue on my university cluster. Ended up fixing it by settling on this hack, but still a bit unsatisfying that this seems to be the current best way to resolve it.

[Jason Rute]

Is there a good place to file an issue about this?

[Mario Carneiro]

Someone with nix and this issue needs to test if it's possible to update static-curl

[Jason Rute]

@Mario Carneiro do you have a concrete set of instructions that one of us can follow to test this? (It looks like Nix can be installed via conda so that is at least one path we could use to run nix. If it can be locally installed like conda can, that is another option.)

[Mario Carneiro]

I'm afraid not, I have no idea how nix updates work. Maybe @Sebastian Ullrich has guidance

[Sebastian Ullrich]

I'm not clear on the exact suggestion, do we expect that simply updating the curl version will fix the issue?

[Mario Carneiro]

I think so?

[Mario Carneiro]

AFAICT that's the fix that was applied, just download the latest version over top of the one we are vendoring

[Julian Berman]

I haven't read back to see what we did here but I don't think that was it?

[Julian Berman]

Users who run into this have old curl that doesn't support --parallel

[Julian Berman]

And the behavior of one of our/Lean's tools is "OK go download newer curl"

[Julian Berman]

And that newer curl may not be configured the same way the host machine's curl was

[Mario Carneiro]

yeah but the fix is still to just get a newer curl, it's not being configured specially in Jason Rute 's directions

[Julian Berman]

OK, I thought I recalled that new enough curl was being downloaded but still wasn't working right, but my memory is bad clearly and I can't reread at the minute

[Mario Carneiro]

In part I don't know whether it is nix's fault or if the package manager / conda has access to a better mechanism for configuring curl which is why I was hoping someone would test using the latest curl in nix

[Sebastian Ullrich]

Well let's try: https://github.com/leanprover-community/static-curl/releases/tag/v8.6.0