C:\Users\leanj>git clone https://github.com/leanprover-community/mathematics_in_lean.git
Cloning into 'mathematics_in_lean'...
remote: Enumerating objects: 3014, done.
remote: Counting objects: 100% (1487/1487), done.
remote: Compressing objects: 100% (274/274), done.
remote: Total 3014 (delta 1348), reused 1213 (delta 1213), pack-reused 1527 (from 2)
Receiving objects: 100% (3014/3014), 54.31 MiB | 15.76 MiB/s, done.
Resolving deltas: 100% (2092/2092), done.
Updating files: 100% (200/200), done.

C:\Users\leanj>cd mathematics_in_lean

C:\Users\leanj\mathematics_in_lean>lake -v exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
trace: .> git clone https://github.com/leanprover-community/mathlib4 C:\Users\leanj\mathematics_in_lean\.lake/packages\mathlib
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\mathlib'...
Updating files: 100% (7477/7477), done.
info: mathlib: checking out revision '308445d7985027f538e281e18df29ca16ede2ba3'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\mathlib> git checkout --detach 308445d7985027f538e281e18df29ca16ede2ba3 --
trace: stderr:
HEAD is now at 308445d798 chore: bump toolchain to v4.21.0 (#26532)
info: plausible: cloning https://github.com/leanprover-community/plausible
trace: .> git clone https://github.com/leanprover-community/plausible C:\Users\leanj\mathematics_in_lean\.lake/packages\plausible
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\plausible'...
info: plausible: checking out revision 'c4aa78186d388e50a436e8362b947bae125a2933'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\plausible> git checkout --detach c4aa78186d388e50a436e8362b947bae125a2933 --
trace: stderr:
HEAD is now at c4aa781 Merge pull request #29 from leanprover-community/bump_to_v4.21.0
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
trace: .> git clone https://github.com/leanprover-community/LeanSearchClient C:\Users\leanj\mathematics_in_lean\.lake/packages\LeanSearchClient
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\LeanSearchClient'...
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\LeanSearchClient> git checkout --detach 6c62474116f525d2814f0157bb468bf3a4f9f120 --
trace: stderr:
HEAD is now at 6c62474 feat: let users specify urls through environment variables (#20)
info: importGraph: cloning https://github.com/leanprover-community/import-graph
trace: .> git clone https://github.com/leanprover-community/import-graph C:\Users\leanj\mathematics_in_lean\.lake/packages\importGraph
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\importGraph'...
info: importGraph: checking out revision 'd07bd64f1910f1cc5e4cc87b6b9c590080e7a457'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\importGraph> git checkout --detach d07bd64f1910f1cc5e4cc87b6b9c590080e7a457 --
trace: stderr:
HEAD is now at d07bd64 Merge pull request #74 from leanprover-community/bump_to_v4.21.0
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
trace: .> git clone https://github.com/leanprover-community/ProofWidgets4 C:\Users\leanj\mathematics_in_lean\.lake/packages\proofwidgets
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\proofwidgets'...
info: proofwidgets: checking out revision '6980f6ca164de593cb77cd03d8eac549cc444156'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\proofwidgets> git checkout --detach 6980f6ca164de593cb77cd03d8eac549cc444156 --
trace: stderr:
HEAD is now at 6980f6c chore: bump toolchain to v4.21.0-rc2 (#122)
info: aesop: cloning https://github.com/leanprover-community/aesop
trace: .> git clone https://github.com/leanprover-community/aesop C:\Users\leanj\mathematics_in_lean\.lake/packages\aesop
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\aesop'...
info: aesop: checking out revision '8ff27701d003456fd59f13a9212431239d902aef'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\aesop> git checkout --detach 8ff27701d003456fd59f13a9212431239d902aef --
trace: stderr:
HEAD is now at 8ff2770 chore: bump toolchain to v4.21.0 (#237)
info: Qq: cloning https://github.com/leanprover-community/quote4
trace: .> git clone https://github.com/leanprover-community/quote4 C:\Users\leanj\mathematics_in_lean\.lake/packages\Qq
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\Qq'...
info: Qq: checking out revision 'e9c65db4823976353cd0bb03199a172719efbeb7'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\Qq> git checkout --detach e9c65db4823976353cd0bb03199a172719efbeb7 --
trace: stderr:
HEAD is now at e9c65db chore: bump toolchain to v4.21.0 (#89)
info: batteries: cloning https://github.com/leanprover-community/batteries
trace: .> git clone https://github.com/leanprover-community/batteries C:\Users\leanj\mathematics_in_lean\.lake/packages\batteries
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\batteries'...
info: batteries: checking out revision '8d2067bf518731a70a255d4a61b5c103922c772e'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\batteries> git checkout --detach 8d2067bf518731a70a255d4a61b5c103922c772e --
trace: stderr:
HEAD is now at 8d2067bf chore: bump toolchain to v4.21.0 (#1297)
info: Cli: cloning https://github.com/leanprover/lean4-cli
trace: .> git clone https://github.com/leanprover/lean4-cli C:\Users\leanj\mathematics_in_lean\.lake/packages\Cli
trace: stderr:
Cloning into 'C:\Users\leanj\mathematics_in_lean\.lake/packages\Cli'...
info: Cli: checking out revision '7c6aef5f75a43ebbba763b44d535175a1b04c9e0'
trace: C:\Users\leanj\mathematics_in_lean\.lake/packages\Cli> git checkout --detach 7c6aef5f75a43ebbba763b44d535175a1b04c9e0 --
trace: stderr:
HEAD is now at 7c6aef5 Merge pull request #43 from leanprover/bump_to_v4.21.0
✖ [2/20] (Optional) Fetching batteries:optBarrel
trace: .> curl -s -S -f -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build.barrel -L https://reservoir.lean-lang.org/api/v1/packages/leanprover-community/batteries/barrel?rev=8d2067bf518731a70a255d4a61b5c103922c772e&toolchain=leanprover%2Flean4%3Av4.21.0 -H X-Reservoir-Api-Version:1.0.0 -H X-Lake-Registry-Api-Version:0.1.0
trace: stderr:
curl: (35) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.
error: external command 'curl' exited with code 35
ℹ [3/20] Ran batteries:extraDep
trace: building from source; failed to fetch Reservoir build (see 'batteries:optBarrel' for details)
ℹ [4/20] Built Cache.Lean
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\Cache\Lean.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Lean.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Lean.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Lean.c --json
ℹ [5/20] Built Batteries.Data.String.Basic
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe -Dlinter.missingDocs=true C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\Batteries\Data\String\Basic.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Basic.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Basic.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Basic.c --json
ℹ [6/20] Built Batteries.Data.Array.Match
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe -Dlinter.missingDocs=true C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\Batteries\Data\Array\Match.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\Array\Match.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\Array\Match.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\Array\Match.c --json
ℹ [7/20] Built Batteries.Data.String.Matcher
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe -Dlinter.missingDocs=true C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\Batteries\Data\String\Matcher.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Matcher.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Matcher.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Matcher.c --json
ℹ [8/20] Built Cache.IO
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\Cache\IO.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\IO.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\IO.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\IO.c --json
ℹ [9/20] Built Batteries.Data.String.Basic:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Basic.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Basic.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [10/20] Built Cache.Lean:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Lean.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Lean.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [11/20] Built Batteries.Data.Array.Match:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\Array\Match.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\Array\Match.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [12/20] Built Batteries.Data.String.Matcher:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Matcher.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Matcher.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [13/20] Built Cache.Hashing
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\Cache\Hashing.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Hashing.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Hashing.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Hashing.c --json
ℹ [14/20] Built Cache.IO:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\IO.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [15/20] Built Cache.Hashing:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Hashing.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [16/20] Built Cache.Requests
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\Cache\Requests.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Requests.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Requests.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Requests.c --json
ℹ [17/20] Built Cache.Main
trace: .> LEAN_PATH=C:\Users\leanj\mathematics_in_lean\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\leanj\mathematics_in_lean\.lake\build\lib\lean c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lean.exe C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\Cache\Main.lean -R C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Main.olean -i C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Main.ilean -c C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Main.c --json
ℹ [18/20] Built Cache.Requests:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Requests.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [19/20] Built Cache.Main:c.o (without exports)
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -c -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\ir\Cache\Main.c -I c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0 -nostdinc -isystem c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG
ℹ [20/20] Built cache
trace: .> c:\Users\leanj\.elan\toolchains\leanprover--lean4---v4.21.0\bin\clang.exe -o C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\bin\cache.exe @C:\Users\leanj\mathematics_in_lean\.lake\packages\mathlib\.lake\build\bin\cache.exe.rsp
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.