curl error CRYPT_E_NO_REVOCATION_CHECK (0x80092012)

Stream: lean4

[Jordi Majó]

I am getting a curl error during mathlib 4 installation

lake exe cache get
PANIC at String.toNat! Init.Data.String.Extra:34:4: Nat expected
installing leantar 0.1.15
uncaught exception: failure in curl #[https://github.com/digama0/leangz/releases/download/v0.1.15/leantar-v0.1.15-x86_64-pc-windows-msvc.zip, -L, -o, C:\Users\leanj\.cache\mathlib\leantar-0.1.15.exe.zip]:
  % 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) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.

Any ideas?
Thanks

[Kim Morrison]

Is this a public repo? Instructions for reproducing the failure locally are very helpful.

[Jordi Majó]

Hi Kim, thanks for your help.

This is the first installation of Mathlib in a new laptop, following the instructions in https://leanprover-community.github.io/install/project.html#working-on-an-existing-project

after this error, Mathlib4 fails to build.

Is that enough to reproduce the error?

Thanks again

[Jordi Majó]

Hi all,
I've deleted the 'mathematics_in_lean' directory and run the installation process again.

Attached you can find the traces of the installation process until it generates the same error above.
trace.txt

Actually, it generates a similar error before, but it seems to be on an optional file.

Do you need any extra information?

[Kim Morrison]

A sequence of commands someone could copy and paste into a terminal would be preferable. Your trace.txt has many commands, and it's unclear which are relevant.

[Jordi Majó]

Hi Kim,

The sequence of commands is also in the trace.txt file. It is very simple:

C:\Users\leanj>git clone https://github.com/leanprover-community/mathematics_in_lean.git
C:\Users\leanj>cd mathematics_in_lean
C:\Users\leanj\mathematics_in_lean>lake -v exe cache get

I just included their verbose output so an expert could see what's going on...

The command that fails is 'lake exe cache get'

[Eric Wieser]

It looks like curl is broken on your machine, either due to being outdated or due to bad network configuration

[Jordi Majó]

Hi Eric and Kim,

I've tried the installation process in a different computer, and I get exactly the same error

C:\Users\jordi\mathematics_in_lean>lake exe cache get
info: downloading https://releases.lean-lang.org/lean4/v4.21.0/lean-4.21.0-windows.tar.zst
360.1 MiB / 360.1 MiB (100 %)   1.9 MiB/s ETA:   0 s
info: installing C:\Users\jordi\.elan\toolchains\leanprover--lean4---v4.21.0
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '308445d7985027f538e281e18df29ca16ede2ba3'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'c4aa78186d388e50a436e8362b947bae125a2933'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'd07bd64f1910f1cc5e4cc87b6b9c590080e7a457'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6980f6ca164de593cb77cd03d8eac549cc444156'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '8ff27701d003456fd59f13a9212431239d902aef'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'e9c65db4823976353cd0bb03199a172719efbeb7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '8d2067bf518731a70a255d4a61b5c103922c772e'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '7c6aef5f75a43ebbba763b44d535175a1b04c9e0'
installing leantar 0.1.15
uncaught exception: failure in curl #[https://github.com/digama0/leangz/releases/download/v0.1.15/leantar-v0.1.15-x86_64-pc-windows-msvc.zip, -L, -o, C:\Users\jordi\.cache\mathlib\leantar-0.1.15.exe.zip]:
  % 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) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.

Is this an error that should be reported to Microsoft? it seems like the 'curl' version shipping with W11 at this point in time does not work well, doesn't it?
Or maybe it is the certificate of the leantar repo...

[Gavin Zhao]

Can you download https://github.com/digama0/leangz/releases/download/v0.1.15/leantar-v0.1.15-x86_64-pc-windows-msvc.zip from your browser though?

[Jordi Majó]

Yes I can. It downloads with no problem

[Jordi Majó]

In which directory should leantar.exe go?

[Jordi Majó]

Hello again,

I've upgraded to curl version 8.16.0 and I get the same error.

Any ideas?

C:\Users\jordi>where curl.exe
C:\Windows\System32\curl.exe
C:\Users\jordi\AppData\Local\Microsoft\WinGet\Links\curl.exe

C:\Users\jordi>set PATH=C:\Users\jordi\AppData\Local\Microsoft\WinGet\Links\;%PATH%

C:\Users\jordi>where curl.exe
C:\Users\jordi\AppData\Local\Microsoft\WinGet\Links\curl.exe
C:\Windows\System32\curl.exe

C:\Users\jordi>curl --version
curl 8.16.0 (x86_64-w64-mingw32) libcurl/8.16.0 LibreSSL/4.1.0 zlib/1.3.1.zlib-ng brotli/1.1.0 zstd/1.5.7 WinIDN libpsl/0.21.5 libssh2/1.11.1 nghttp2/1.67.1 ngtcp2/1.16.0 nghttp3/1.12.0
Release-Date: 2025-09-10
Protocols: dict file ftp ftps gopher gophers http https imap imaps ipfs ipns ldap ldaps mqtt pop3 pop3s rtsp scp sftp smb smbs smtp smtps telnet tftp ws wss
Features: alt-svc AsynchDNS brotli CAcert HSTS HTTP2 HTTP3 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM PSL SPNEGO SSL SSLS-EXPORT SSPI threadsafe UnixSockets zstd

C:\Users\jordi>cd mathematics_in_lean

C:\Users\jordi\mathematics_in_lean>lake -v exe cache get
...

ℹ [19/19] Replayed cache
trace: .> c:\Users\jordi\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -o C:\Users\jordi\mathematics_in_lean\.lake\packages\mathlib\.lake\build\bin\cache.exe @C:\Users\jordi\mathematics_in_lean\.lake\packages\mathlib\.lake\build\bin\cache.exe.rsp
installing leantar 0.1.15
uncaught exception: failure in curl #[https://github.com/digama0/leangz/releases/download/v0.1.15/leantar-v0.1.15-x86_64-pc-windows-msvc.zip, -L, -o, C:\Users\jordi\.cache\mathlib\leantar-0.1.15.exe.zip]:
  % 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) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.

Thanks

[Jordi Majó]

Hello again, it seems the problem with the curl revocation of certificates was caused by AVG Internet Security. I disabled the Firewall, Web protection, and Antivirus and it is now downloading with no problem.

[Kevin Buzzard]

Darn it, one of the canonical responses to "I'm on Windows and am having trouble downloading stuff" should be "have you tried disabling your antivirus?". Sorry we didn't suggest this earlier, this is a really common gotcha for new Windows users. I am very unclear about whether this is something which can be fixed at our (I mean the Lean community's) end.

[Kenny Lau]

is it possible to register the things we need with the antivirus softwares?

[Henrik Böving]

A large chunk of these issues are very likely fixable if we add --proxy-native-ca --native-ca to the curl invocations that occur in Cache. These commands are currently only available at curl version 8.2.0 released mid 2023. I just took a look at the curl version check and we currently do seem to support versions quite a bit older than that. In particular on Linux/MacOS we do support just downloading a new, statically linked curl version but we do not on Windows (and even if we had this infra: how do we perform the download if the antivirus is blocking us :D). Thus this change would only make sense if we could confirm that a majority of windows users are operating at a version >= 8.2.0

TLDR: Windows users please post the output of curl --version here to see if a fix is feasible.

[Floris van Doorn]

In Git Bash:

Floris@Dell-E MINGW64 ~/projects/LeanCourse (master)
$ curl --version
curl 7.88.1 (x86_64-w64-mingw32) libcurl/7.88.1 OpenSSL/1.1.1t (Schannel) zlib/1.2.13 brotli/1.0.9 zstd/1.5.4 libidn2/2.3.4 libpsl/0.21.2 (+libidn2/2.3.3) libssh2/1.10.0 nghttp2/1.52.0
Release-Date: 2023-02-20
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz MultiSSL NTLM PSL SPNEGO SSL SSPI threadsafe TLS-SRP UnixSockets zstd

In WSL:

floris@Dell-E:~/projects$ curl --version
curl 8.5.0 (x86_64-pc-linux-gnu) libcurl/8.5.0 OpenSSL/3.0.13 zlib/1.3 brotli/1.1.0 zstd/1.5.5 libidn2/2.3.7 libpsl/0.21.2 (+libidn2/2.3.7) libssh/0.10.6/openssl/zlib nghttp2/1.59.0 librtmp/2.3 OpenLDAP/2.6.7
Release-Date: 2023-12-06, security patched: 8.5.0-2ubuntu10.6
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM PSL SPNEGO SSL threadsafe TLS-SRP UnixSockets zstd

In cmd/Powershell:

C:\Users\Floris>curl --version
curl 8.14.1 (Windows) libcurl/8.14.1 Schannel zlib/1.3.1 WinIDN
Release-Date: 2025-06-09
Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss
Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

I mostly used Git Bash for Lean stuff until now, but I'm slowly transitioning to WSL.

[Floris van Doorn]

So I don't think it's safe to assume that most Windows users use version >= 8.2.0. But maybe not many users use Git Bash anymore, since it's not part of the official instructions for a while now(?)

[Henrik Böving]

My understanding is that we only use the curl that you see in cmd/powershell because that is the one that is guaranteed to ship with Windows (if that's not the case we very much should make it the case)

[Kenny Lau]

windows powershell:

> curl --version
curl : The remote name could not be resolved: '--version'
At line:1 char:1
+ curl --version
+ ~~~~~~~~~~~~~~
    + CategoryInfo          : InvalidOperation: (System.Net.HttpWebRequest:HttpWebRequest) [Invoke-WebRequest], WebExc
   eption
    + FullyQualifiedErrorId : WebCmdletWebResponseException,Microsoft.PowerShell.Commands.InvokeWebRequestCommand

[Henrik Böving]

According to this very trustworthy website if you are in powershell you should do curl.exe --version

[Floris van Doorn]

Henrik Böving said:

My understanding is that we only use the curl that you see in cmd/powershell because that is the one that is guaranteed to ship with Windows (if that's not the case we very much should make it the case)

That makes sense

[Kenny Lau]

> curl.exe --version
curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN
Release-Date: 2025-04-02
Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss
Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

[Markus Himmel]

Windows 10 version 21H2 (which is supported by Lean and is also the version that Windows Server 2022, which is also supported by Lean, is based on) ships with curl 7.83.1.

[Henrik Böving]

Surely everyone will stop using Windows 10 in 14 days anyways :)

[Henrik Böving]

Though more seriously, I guess this could also just be a best effort type of solution where if we notice the version is sufficiently recent we set the flag and otherwise not?

[Henrik Böving]

One other trick we could try is https://learn.microsoft.com/en-us/powershell/module/microsoft.powershell.utility/invoke-webrequest?view=powershell-7.5 which hopefully just generally respects the windows certificate store, I don't know if it supports all the stuff we do with curl in cache though.