Verification run

Run 98

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 4af1d5421f85 toolchain lean-v4-31-0 prover lean took 4h 3m · finished 3w ago

lake build failed with exit code none (process did not exit cleanly) (toolchain lean-v4-31-0, command: elan run leanprover/lean4:v4.31.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

$ git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-558-source
exit_code=Some(0) duration_ms=1122
stderr:
Cloning into '/var/lib/apodeixis/repos/job-558-source'...


$ git checkout 4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb
exit_code=Some(0) duration_ms=29
stderr:
Note: switching to '4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 4af1d54 Remove upstreamed lemmas and attributes (#1621)

Resolved source revision: 4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb

Detected prover: lean
Detected requested toolchain: lean-v4-31-0
Materialized Lean semantic helper assets
Prepared source: revision=4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb provenance={"branch":"main","checked_out_revision":"4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-31-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored 8 Lean dependency package snapshot(s)
Prepared 8 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction

$ lake exe cache get
exit_code=Some(0) duration_ms=163671
stdout:
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 file(s)

stderr:
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'db127794c79fdeb86f6b0cf6ff2c804026fbaff1'
info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision 'f699a3e5d3efb381b9ddfb61a1ca51be25f456bd'
info: leancert: cloning https://github.com/alerad/leancert.git
info: leancert: checking out revision '33a9d1762b284fe1914d481d6a8158520e14708e'
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision 'f38c848196b0467e7b9dcc3d129a866b4051c23c'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fc38104235ab6cf8a448a74405aa258804ef4e36'
✔ [1/5] Built Cache.Cli (929ms)
✔ [3/11] Built Cache.Lean (535ms)
✔ [6/11] Built Cache.Infra (618ms)
✔ [7/12] Built Cache.IO (1.8s)
✔ [9/26] Built Cache.Hashing (1.0s)
✔ [10/26] Built Cache.Requests (2.2s)
✔ [11/26] Built Cache.Cli:c.o (1.3s)
✔ [12/26] Built Cache.Lean:c.o (140ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (368ms)
✔ [16/26] Built Cache.Infra:c.o (177ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (801ms)
✔ [19/26] Built Cache.Marker:c.o (108ms)
✔ [20/26] Built Cache.Query (829ms)
✔ [21/26] Built Cache.Query:c.o (232ms)
✔ [22/26] Built Cache.Warning (854ms)
✔ [23/26] Built Cache.Warning:c.o (223ms)
✔ [24/26] Built Cache.Main (1.7s)
✔ [25/26] Built Cache.Main:c.o (753ms)
✔ [26/26] Built cache:exe (5.8s)

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 12 KB/s], Decompressed: 0
Downloaded: 19 file(s) [attempted 19/8546 = 0%, 3 KB/s], Decompressed: 14
Downloaded: 43 file(s) [attempted 43/8546 = 0%, 20 KB/s], Decompressed: 37
Downloaded: 64 file(s) [attempted 64/8546 = 0%, 195 KB/s], Decompressed: 54
Downloaded: 91 file(s) [attempted 91/8546 = 1%, 427 KB/s], Decompressed: 74
Downloaded: 115 file(s) [attempted 115/8546 = 1%, 112 KB/s], Decompressed: 92
Downloaded: 150 file(s) [attempted 150/8546 = 1%, 127 KB/s], Decompressed: 109
Downloaded: 189 file(s) [attempted 189/8546 = 2%, 739 KB/s], Decompressed: 156
Downloaded: 221 file(s) [attempted 221/8546 = 2%, 443 KB/s], Decompressed: 183
Downloaded: 255 file(s) [attempted 255/8546 = 2%, 116 KB/s], Decompressed: 217
Downloaded: 292 file(s) [attempted 292/8546 = 3%, 96 KB/s], Decompressed: 217
Downloaded: 332 file(s) [attempted 332/8546 = 3%, 689 KB/s], Decompressed: 251
Downloaded: 371 file(s) [attempted 371/8546 = 4%, 86 KB/s], Decompressed: 251
Downloaded: 410 file(s) [attempted 410/8546 = 4%, 78 KB/s], Decompressed: 312
Downloaded: 444 file(s) [attempted 444/8546 = 5%, 79 KB/s], Decompressed: 312
Downloaded: 481 file(s) [attempted 481/8546 = 5%, 254 KB/s], Decompressed: 373
Downloaded: 515 file(s) [attempted 515/8546 = 6%, 222 KB/s], Decompressed: 373
Downloaded: 559 file(s) [attempted 559/8546 = 6%, 280 KB/s], Decompressed: 448
Downloaded: 603 file(s) [attempted 603/8546 = 7%, 260 KB/s], Decompressed: 448
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 137 KB/s], Decompressed: 448
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 61 KB/s], Decompressed: 539
Downloaded: 715 file(s) [attempted 715/8546 = 8%, 422 KB/s], Decompressed: 539
Downloaded: 756 file(s) [attempted 756/8546 = 8%, 423 KB/s], Decompressed: 539
Downloaded: 796 file(s) [attempted 796/8546 = 9%, 340 KB/s], Decompressed: 657
Downloaded: 837 file(s) [attempted 837/8546 = 9%, 823 KB/s], Decompressed: 657
Downloaded: 871 file(s) [attempted 871/8546 = 10%, 541 KB/s], Decompressed: 657
Downloaded: 911 file(s) [attempted 911/8546 = 10%, 191 KB/s], Decompressed: 657
Downloaded: 954 file(s) [attempted 954/8546 = 11%, 165 KB/s], Decompressed: 796
Downloaded: 989 file(s) [attempted 989/8546 = 11%, 711 KB/s], Decompressed: 796
Downloaded: 1033 file(s) [attempted 1033/8546 = 12%, 166 KB/s], Decompressed: 796
Downloaded: 1060 file(s) [attempted 1060/8546 = 12%, 159 KB/s], Decompressed: 796
Downloaded: 1101 file(s) [attempted 1101/8546 = 12%, 61 KB/s], Decompressed: 796
Downloaded: 1148 file(s) [attempted 1148/8546 = 13%, 273 KB/s], Decompressed: 796
Downloaded: 1199 file(s) [attempted 1199/8546 = 14%, 151 KB/s], Decompressed: 952
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 1134 KB/s], Decompressed: 952
Downloaded: 1291 file(s) [attempted 1291/8546 = 15%, 1086 KB/s], Decompressed: 952
Downloaded: 1335 file(s) [attempted 1335/8546 = 15%, 733 KB/s], Decompressed: 952
Downloaded: 1365 file(s) [attempted 1365/8546 = 15%, 131 KB/s], Decompressed: 952
Downloaded: 1399 file(s) [attempted 1399/8546 = 16%, 179 KB/s], Decompressed: 952
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 649 KB/s], Decompressed: 952
Downloaded: 1490 file(s) [attempted 1490/8546 = 17%, 130 KB/s], Decompressed: 1179
Downloaded: 1531 file(s) [attempted 1531/8546 = 17%, 71 KB/s], Decompressed: 1179
Downloaded: 1554 file(s) [attempted 1554/8546 = 18%, 343 KB/s], Decompressed: 1179
Downloaded: 1598 file(s) [attempted 1598/8546 = 18%, 397 KB/s], Decompressed: 1179
Downloaded: 1642 file(s) [attempted 1642/8546 = 19%, 644 KB/s], Decompressed: 1179
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 113 KB/s], Decompressed: 1179
Downloaded: 1713 file(s) [attempted 1713/8546 = 20%, 411 KB/s], Decompressed: 1179
Downloaded: 1754 file(s) [attempted 1754/8546 = 20%, 181 KB/s], Decompressed: 1179
Downloaded: 1801 file(s) [attempted 1801/8546 = 21%, 69 KB/s], Decompressed: 1179
Downloaded: 1849 file(s) [attempted 1849/8546 = 21%, 1006 KB/s], Decompressed: 1490
Downloaded: 1889 file(s) [attempted 1889/8546 = 22%, 202 KB/s], Decompressed: 1490
Downloaded: 1933 file(s) [attempted 1933/8546 = 22%, 674 KB/s], Decompressed: 1490
Downloaded: 1964 file(s) [attempted 1964/8546 = 22%, 409 KB/s], Decompressed: 1490
Downloaded: 2001 file(s) [attempted 2001/8546 = 23%, 73 KB/s], Decompressed: 1490
Downloaded: 2048 file(s) [attempted 2048/8546 = 23%, 119 KB/s], Decompressed: 1490
Downloaded: 2096 file(s) [attempted 2096/8546 = 24%, 235 KB/s], Decompressed: 1490
Downloaded: 2136 file(s) [attempted 2136/8546 = 24%, 1149 KB/s], Decompressed: 1490
Downloaded: 2177 file(s) [attempted 2177/8546 = 25%, 111 KB/s], Decompressed: 1811
Downloaded: 2207 file(s) [attempted 2207/8546 = 25%, 931 KB/s], Decompressed: 1811
Downloaded: 2244 file(s) [attempted 2244/8546 = 26%, 249 KB/s], Decompressed: 1811
Downloaded: 2288 file(s) [attempted 2288/8546 = 26%, 473 KB/s], Decompressed: 1811
Downloaded: 2322 file(s) [attempted 2322/8546 = 27%, 190 KB/s], Decompressed: 1811
Downloaded: 2363 file(s) [attempted 2363/8546 = 27%, 351 KB/s], Decompressed: 1811
Downloaded: 2403 file(s) [attempted 2403/8546 = 28%, 434 KB/s], Decompressed: 1811
Downloaded: 2444 file(s) [attempted 2444/8546 = 28%, 903 KB/s], Decompressed: 1811
Downloaded: 2485 file(s) [attempted 2485/8546 = 29%, 62 KB/s], Decompressed: 1811
Downloaded: 2522 file(s) [attempted 2522/8546 = 29%, 329 KB/s], Decompressed: 1811
Downloaded: 2559 file(s) [attempted 2559/8546 = 29%, 566 KB/s], Decompressed: 1811
Downloaded: 2600 file(s) [attempted 2600/8546 = 30%, 160 KB/s], Decompressed: 1811
Downloaded: 2637 file(s) [attempted 2637/8546 = 30%, 388 KB/s], Decompressed: 2167
Downloaded: 2677 file(s) [attempted 2677/8546 = 31%, 247 KB/s], Decompressed: 2167
Downloaded: 2718 file(s) [attempted 2718/8546 = 31%, 55 KB/s], Decompressed: 2167
Downloaded: 2755 file(s) [attempted 2755/8546 = 32%, 152 KB/s], Decompressed: 2167
Downloaded: 2796 file(s) [attempted 2796/8546 = 32%, 81 KB/s], Decompressed: 2167
Downloaded: 2840 file(s) [attempted 2840/8546 = 33%, 82 KB/s], Decompressed: 2167
Downloaded: 2877 file(s) [attempted 2877/8546 = 33%, 251 KB/s], Decompressed: 2167
Downloaded: 2918 file(s) [attempted 2918/8546 = 34%, 822 KB/s], Decompressed: 2167
Downloaded: 2955 file(s) [attempted 2955/8546 = 34%, 723 KB/s], Decompressed: 2167
Downloaded: 2995 file(s) [attempted 2995/8546 = 35%, 37 KB/s], Decompressed: 2167
Downloaded: 3039 file(s) [attempted 3039/8546 = 35%, 233 KB/s], Decompressed: 2167
Downloaded: 3067 file(s) [attempted 3067/8546 = 35%, 270 KB/s], Decompressed: 2167
Downloaded: 3114 file(s) [attempted 3114/8546 = 36%, 494 KB/s], Decompressed: 2167
Downloaded: 3165 file(s) [attempted 3165/8546 = 37%, 1689 KB/s], Decompressed: 2167
Downloaded: 3215 file(s) [attempted 3215/8546 = 37%, 191 KB/s], Decompressed: 2634
Downloaded: 3263 file(s) [attempted 3263/8546 = 38%, 258 KB/s], Decompressed: 2634
Downloaded: 3293 file(s) [attempted 3293/8546 = 38%, 309 KB/s], Decompressed: 2634
Downloaded: 3334 file(s) [attempted 3334/8546 = 39%, 153 KB/s], Decompressed: 2634
Downloaded: 3364 file(s) [attempted 3364/8546 = 39%, 708 KB/s], Decompressed: 2634
Downloaded: 3401 file(s) [attempted 3401/8546 = 39%, 41 KB/s], Decompressed: 2634
Downloaded: 3449 file(s) [attempted 3449/8546 = 40%, 178 KB/s], Decompressed: 2634
Downloaded: 3489 file(s) [attempted 3489/8546 = 40%, 206 KB/s], Decompressed: 2634
Downloaded: 3533 file(s) [attempted 3533/8546 = 41%, 264 KB/s], Decompressed: 2634
Downloaded: 3567 file(s) [attempted 3567/8546 = 41%, 66 KB/s], Decompressed: 2634
Downloaded: 3604 file(s) [attempted 3604/8546 = 42%, 717 KB/s], Decompressed: 2634
Downloaded: 3652 file(s) [attempted 3652/8546 = 42%, 227 KB/s], Decompressed: 2634
Downloaded: 3696 file(s) [attempted 3696/8546 = 43%, 234 KB/s], Decompressed: 2634
Downloaded: 3740 file(s) [attempted 3740/8546 = 43%, 1801 KB/s], Decompressed: 2634
Downloaded: 3777 file(s) [attempted 3777/8546 = 44%, 92 KB/s], Decompressed: 2634
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 99 KB/s], Decompressed: 2634
Downloaded: 3848 file(s) [attempted 3848/8546 = 45%, 359 KB/s], Decompressed: 3178
Downloaded: 3892 file(s) [attempted 3892/8546 = 45%, 725 KB/s], Decompressed: 3178
Downloaded: 3939 file(s) [attempted 3939/8546 = 46%, 158 KB/s], Decompressed: 3178
Downloaded: 3976 file(s) [attempted 3976/8546 = 46%, 22 KB/s], Decompressed: 3178
Downloaded: 4010 file(s) [attempted 4010/8546 = 46%, 310 KB/s], Decompressed: 3178
Downloaded: 4048 file(s) [attempted 4048/8546 = 47%, 881 KB/s], Decompressed: 3178
Downloaded: 4092 file(s) [attempted 4092/8546 = 47%, 1413 KB/s], Decompressed: 3178
Downloaded: 4139 file(s) [attempted 4139/8546 = 48%, 3619 KB/s], Decompressed: 3178
Downloaded: 4173 file(s) [attempted 4173/8546 = 48%, 274 KB/s], Decompressed: 3178
Downloaded: 4213 file(s) [attempted 4213/8546 = 49%, 296 KB/s], Decompressed: 3178
Downloaded: 4254 file(s) [attempted 4254/8546 = 49%, 437 KB/s], Decompressed: 3178
Downloaded: 4294 file(s) [attempted 4294/8546 = 50%, 609 KB/s], Decompressed: 3178
Downloaded: 4342 file(s) [attempted 4342/8546 = 50%, 161 KB/s], Decompressed: 3178
Downloaded: 4380 file(s) [attempted 4380/8546 = 51%, 205 KB/s], Decompressed: 3178
Downloaded: 4409 file(s) [attempted 4409/8546 = 51%, 379 KB/s], Decompressed: 3178
Downloaded: 4453 file(s) [attempted 4453/8546 = 52%, 74 KB/s], Decompressed: 3178
Downloaded: 4497 file(s) [attempted 4497/8546 = 52%, 36 KB/s], Decompressed: 3178
Downloaded: 4541 file(s) [attempted 4541/8546 = 53%, 225 KB/s], Decompressed: 3178
Downloaded: 4572 file(s) [attempted 4572/8546 = 53%, 53 KB/s], Decompressed: 3178
Downloaded: 4609 file(s) [attempted 4609/8546 = 53%, 34 KB/s], Decompressed: 3178
Downloaded: 4650 file(s) [attempted 4650/8546 = 54%, 23 KB/s], Decompressed: 3814
Downloaded: 4694 file(s) [attempted 4694/8546 = 54%, 58 KB/s], Decompressed: 3814
Downloaded: 4741 file(s) [attempted 4741/8546 = 55%, 1046 KB/s], Decompressed: 3814
Downloaded: 4775 file(s) [attempted 4775/8546 = 55%, 374 KB/s], Decompressed: 3814
Downloaded: 4810 file(s) [attempted 4810/8546 = 56%, 361 KB/s], Decompressed: 3814
Downloaded: 4849 file(s) [attempted 4849/8546 = 56%, 383 KB/s], Decompressed: 3814
Downloaded: 4893 file(s) [attempted 4893/8546 = 57%, 262 KB/s], Decompressed: 3814
Downloaded: 4937 file(s) [attempted 4937/8546 = 57%, 121 KB/s], Decompressed: 3814
Downloaded: 4974 file(s) [attempted 4974/8546 = 58%, 436 KB/s], Decompressed: 3814
Downloaded: 5012 file(s) [attempted 5012/8546 = 58%, 381 KB/s], Decompressed: 3814
Downloaded: 5052 file(s) [attempted 5052/8546 = 59%, 239 KB/s], Decompressed: 3814
Downloaded: 5093 file(s) [attempted 5093/8546 = 59%, 418 KB/s], Decompressed: 3814
Downloaded: 5133 file(s) [attempted 5133/8546 = 60%, 107 KB/s], Decompressed: 3814
Downloaded: 5167 file(s) [attempted 5167/8546 = 60%, 216 KB/s], Decompressed: 3814
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 220 KB/s], Decompressed: 3814
Downloaded: 5248 file(s) [attempted 5248/8546 = 61%, 231 KB/s], Decompressed: 3814
Downloaded: 5289 file(s) [attempted 5289/8546 = 61%, 102 KB/s], Decompressed: 3814
Downloaded: 5323 file(s) [attempted 5323/8546 = 62%, 436 KB/s], Decompressed: 3814
Downloaded: 5360 file(s) [attempted 5360/8546 = 62%, 284 KB/s], Decompressed: 3814
Downloaded: 5401 file(s) [attempted 5401/8546 = 63%, 245 KB/s], Decompressed: 3814
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 56 KB/s], Decompressed: 3814
Downloaded: 5485 file(s) [attempted 5485/8546 = 64%, 280 KB/s], Decompressed: 3814
Downloaded: 5516 file(s) [attempted 5516/8546 = 64%, 257 KB/s], Decompressed: 3814
Downloaded: 5556 file(s) [attempted 5556/8546 = 65%, 225 KB/s], Decompressed: 3814
Downloaded: 5600 file(s) [attempted 5600/8546 = 65%, 125 KB/s], Decompressed: 4619
Downloaded: 5645 file(s) [attempted 5645/8546 = 66%, 153 KB/s], Decompressed: 4619
Downloaded: 5685 file(s) [attempted 5685/8546 = 66%, 285 KB/s], Decompressed: 4619
Downloaded: 5715 file(s) [attempted 5715/8546 = 66%, 521 KB/s], Decompressed: 4619
Downloaded: 5759 file(s) [attempted 5759/8546 = 67%, 601 KB/s], Decompressed: 4619
Downloaded: 5800 file(s) [attempted 5800/8546 = 67%, 94 KB/s], Decompressed: 4619
Downloaded: 5847 file(s) [attempted 5847/8546 = 68%, 139 KB/s], Decompressed: 4619
Downloaded: 5895 file(s) [attempted 5895/8546 = 68%, 103 KB/s], Decompressed: 4619
Downloaded: 5928 file(s) [attempted 5928/8546 = 69%, 101 KB/s], Decompressed: 4619
Downloaded: 5959 file(s) [attempted 5959/8546 = 69%, 96 KB/s], Decompressed: 4619
Downloaded: 5999 file(s) [attempted 5999/8546 = 70%, 144 KB/s], Decompressed: 4619
Downloaded: 6040 file(s) [attempted 6040/8546 = 70%, 200 KB/s], Decompressed: 4619
Downloaded: 6077 file(s) [attempted 6077/8546 = 71%, 63 KB/s], Decompressed: 4619
Downloaded: 6114 file(s) [attempted 6114/8546 = 71%, 37 KB/s], Decompressed: 4619
Downloaded: 6148 file(s) [attempted 6148/8546 = 71%, 107 KB/s], Decompressed: 4619
Downloaded: 6192 file(s) [attempted 6192/8546 = 72%, 1765 KB/s], Decompressed: 4619
Downloaded: 6236 file(s) [attempted 6236/8546 = 72%, 58 KB/s], Decompressed: 4619
Downloaded: 6270 file(s) [attempted 6270/8546 = 73%, 101 KB/s], Decompressed: 4619
Downloaded: 6311 file(s) [attempted 6311/8546 = 73%, 63 KB/s], Decompressed: 4619
Downloaded: 6344 file(s) [attempted 6344/8546 = 74%, 271 KB/s], Decompressed: 4619
Downloaded: 6388 file(s) [attempted 6388/8546 = 74%, 1387 KB/s], Decompressed: 4619
Downloaded: 6429 file(s) [attempted 6429/8546 = 75%, 1318 KB/s], Decompressed: 4619
Downloaded: 6466 file(s) [attempted 6466/8546 = 75%, 94 KB/s], Decompressed: 4619
Downloaded: 6504 file(s) [attempted 6504/8546 = 76%, 125 KB/s], Decompressed: 4619
Downloaded: 6544 file(s) [attempted 6544/8546 = 76%, 50 KB/s], Decompressed: 4619
Downloaded: 6591 file(s) [attempted 6591/8546 = 77%, 243 KB/s], Decompressed: 4619
Downloaded: 6642 file(s) [attempted 6642/8546 = 77%, 130 KB/s], Decompressed: 4619
Downloaded: 6693 file(s) [attempted 6693/8546 = 78%, 1003 KB/s], Decompressed: 5566
Downloaded: 6740 file(s) [attempted 6740/8546 = 78%, 77 KB/s], Decompressed: 5566
Downloaded: 6784 file(s) [attempted 6784/8546 = 79%, 49 KB/s], Decompressed: 5566
Downloaded: 6818 file(s) [attempted 6818/8546 = 79%, 678 KB/s], Decompressed: 5566
Downloaded: 6852 file(s) [attempted 6852/8546 = 80%, 83 KB/s], Decompressed: 5566
Downloaded: 6892 file(s) [attempted 6892/8546 = 80%, 227 KB/s], Decompressed: 5566
Downloaded: 6940 file(s) [attempted 6940/8546 = 81%, 147 KB/s], Decompressed: 5566
Downloaded: 6987 file(s) [attempted 6987/8546 = 81%, 187 KB/s], Decompressed: 5566
Downloaded: 7031 file(s) [attempted 7031/8546 = 82%, 83 KB/s], Decompressed: 5566
Downloaded: 7062 file(s) [attempted 7062/8546 = 82%, 150 KB/s], Decompressed: 5566
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 201 KB/s], Decompressed: 5566
Downloaded: 7139 file(s) [attempted 7139/8546 = 83%, 238 KB/s], Decompressed: 5566
Downloaded: 7187 file(s) [attempted 7187/8546 = 84%, 380 KB/s], Decompressed: 5566
Downloaded: 7221 file(s) [attempted 7221/8546 = 84%, 108 KB/s], Decompressed: 5566
Downloaded: 7258 file(s) [attempted 7258/8546 = 84%, 896 KB/s], Decompressed: 5566
Downloaded: 7298 file(s) [attempted 7298/8546 = 85%, 315 KB/s], Decompressed: 5566
Downloaded: 7339 file(s) [attempted 7339/8546 = 85%, 601 KB/s], Decompressed: 5566
Downloaded: 7386 file(s) [attempted 7386/8546 = 86%, 348 KB/s], Decompressed: 5566
Downloaded: 7427 file(s) [attempted 7427/8546 = 86%, 307 KB/s], Decompressed: 5566
Downloaded: 7464 file(s) [attempted 7464/8546 = 87%, 441 KB/s], Decompressed: 5566
Downloaded: 7501 file(s) [attempted 7501/8546 = 87%, 368 KB/s], Decompressed: 5566
Downloaded: 7542 file(s) [attempted 7542/8546 = 88%, 83 KB/s], Decompressed: 5566
Downloaded: 7579 file(s) [attempted 7579/8546 = 88%, 148 KB/s], Decompressed: 5566
Downloaded: 7623 file(s) [attempted 7623/8546 = 89%, 151 KB/s], Decompressed: 5566
Downloaded: 7660 file(s) [attempted 7660/8546 = 89%, 155 KB/s], Decompressed: 5566
Downloaded: 7702 file(s) [attempted 7702/8546 = 90%, 50 KB/s], Decompressed: 5566
Downloaded: 7731 file(s) [attempted 7731/8546 = 90%, 381 KB/s], Decompressed: 5566
Downloaded: 7775 file(s) [attempted 7775/8546 = 90%, 959 KB/s], Decompressed: 5566
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 128 KB/s], Decompressed: 5566
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 1663 KB/s], Decompressed: 5566
Downloaded: 7901 file(s) [attempted 7901/8546 = 92%, 1037 KB/s], Decompressed: 5566
Downloaded: 7938 file(s) [attempted 7938/8546 = 92%, 42 KB/s], Decompressed: 5566
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 1025 KB/s], Decompressed: 5566
Downloaded: 8022 file(s) [attempted 8022/8546 = 93%, 253 KB/s], Decompressed: 5566
Downloaded: 8063 file(s) [attempted 8063/8546 = 94%, 830 KB/s], Decompressed: 5566
Downloaded: 8097 file(s) [attempted 8097/8546 = 94%, 144 KB/s], Decompressed: 6686
Downloaded: 8141 file(s) [attempted 8141/8546 = 95%, 162 KB/s], Decompressed: 6686
Downloaded: 8181 file(s) [attempted 8181/8546 = 95%, 706 KB/s], Decompressed: 6686
Downloaded: 8219 file(s) [attempted 8219/8546 = 96%, 982 KB/s], Decompressed: 6686
Downloaded: 8263 file(s) [attempted 8263/8546 = 96%, 51 KB/s], Decompressed: 6686
Downloaded: 8300 file(s) [attempted 8300/8546 = 97%, 403 KB/s], Decompressed: 6686
Downloaded: 8337 file(s) [attempted 8337/8546 = 97%, 299 KB/s], Decompressed: 6686
Downloaded: 8367 file(s) [attempted 8367/8546 = 97%, 81 KB/s], Decompressed: 6686
Downloaded: 8411 file(s) [attempted 8411/8546 = 98%, 317 KB/s], Decompressed: 6686
Downloaded: 8452 file(s) [attempted 8452/8546 = 98%, 848 KB/s], Decompressed: 6686
Downloaded: 8489 file(s) [attempted 8489/8546 = 99%, 48 KB/s], Decompressed: 6686
Downloaded: 8530 file(s) [attempted 8530/8546 = 99%, 850 KB/s], Decompressed: 6686
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 850 KB/s], Decompressed: 6686


$ lake build
exit_code=None duration_ms=7200014
stdout:
✔ [2071/2074] Built PrimeNumberTheoremAnd.Auxiliary (41s)
✔ [3002/3008] Built PrimeNumberTheoremAnd.Sobolev (76s)
✔ [3021/3022] Built PrimeNumberTheoremAnd.Fourier (116s)
✔ [3022/3027] Built Architect.Basic (8.3s)
✔ [3023/3027] Built Architect.Command (903ms)
✔ [3024/3027] Built Architect.CollectUsed (951ms)
✔ [3025/3027] Built Architect.Content (945ms)
✔ [3026/3031] Built Architect.Attribute (1.6s)
✔ [3027/3032] Built Architect.Tactic (1.3s)
✔ [3028/3032] Built Architect.Output (1.9s)
✔ [3030/3033] Built Architect.Load (861ms)
✔ [3031/3040] Built Architect (827ms)
✔ [3059/3060] Built PrimeNumberTheoremAnd.Defs (141s)
✔ [3544/3554] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (32s)
✔ [3546/3554] Built PrimeNumberTheoremAnd.Rectangle (16s)
✔ [3550/3555] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.3s)
✔ [3552/3560] Built PrimeNumberTheoremAnd.ZetaConj (134s)
✔ [3554/3561] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (177s)
✔ [3557/3562] Built PrimeNumberTheoremAnd.EulerMaclaurin (7.3s)
✔ [3561/3567] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (102s)
✔ [3563/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (8.8s)
✔ [3565/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.6s)
✔ [3566/3569] Built PrimeNumberTheoremAnd.ZetaBounds (209s)
✔ [3570/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (8.2s)
✔ [3572/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.8s)
✔ [3575/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (3.4s)
✔ [3576/3588] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (1.9s)
✔ [3577/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (2.7s)
✔ [3578/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (2.2s)
✔ [3579/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (2.0s)
✔ [3580/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (3.1s)
✔ [3582/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (2.6s)
✔ [3584/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (3.9s)
✔ [3586/3596] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.5s)
✔ [3588/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.5s)
✔ [3591/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.7s)
✔ [3594/3601] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.3s)
✔ [3596/3605] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (2.7s)
✔ [3610/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (1.8s)
✔ [3611/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (1.8s)
✔ [3613/3631] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (2.5s)
✔ [3615/3631] Built PrimeNumberTheoremAnd.MellinCalculus (64s)
✔ [3616/3631] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.9s)
✔ [3618/3632] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (3.2s)
✔ [3620/3632] Built PrimeNumberTheoremAnd.SmoothExistence (6.2s)
✔ [3622/3633] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (1.9s)
ℹ [3624/3633] Built PrimeNumberTheoremAnd.MediumPNT (133s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3632/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (11s)
✔ [3634/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (4.2s)
✔ [3636/3639] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (3.9s)
✔ [3637/3639] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (159s)
✔ [3640/3653] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (18s)
✔ [3645/3655] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (19s)
✔ [3648/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (4.7s)
✔ [3650/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (5.5s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (128s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3653/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (31s)
✔ [3654/3656] Built PrimeNumberTheoremAnd.BorelCaratheodory (92s)
✔ [3655/3656] Built PrimeNumberTheoremAnd.BrunTitchmarsh (21s)
✔ [3778/3784] Built LeanCert.Core.Interval (2.7s)
⚠ [3779/3784] Built PrimeNumberTheoremAnd.Wiener (118s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3780/3784] Built LeanCert.Core.IntervalRat.Basic (39s)
✔ [3781/3784] Built PrimeNumberTheoremAnd.Consequences (141s)
✔ [3782/3784] Built LeanCert.Tactic.IntervalAuto.Types (44s)
✔ [3783/3794] Built LeanCert.Tactic.IntervalAuto.Norm (4.2s)
✔ [3788/3794] Built LeanCert.Core.Expr (6.3s)
✔ [3789/3795] Built LeanCert.Meta.Numeral (3.2s)
✔ [3790/3795] Built LeanCert.Meta.ToExpr (4.1s)
✔ [3791/3795] Built LeanCert.Tactic.IntervalAuto.Extract (2.7s)
✔ [3792/3795] Built LeanCert.Core.Support (2.4s)
✔ [3793/3796] Built LeanCert.Tactic.IntervalAuto.Parse (4.3s)
✔ [3794/3796] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.8s)
✔ [3795/3797] Built LeanCert.Core.IntervalRat.Transcendental (3.6s)
✔ [3796/3799] Built LeanCert.Core.IntervalRat.LogReduction (3.8s)
✔ [3808/3816] Built LeanCert.Core.DerivativeIntervals (2.4s)
✔ [3812/3822] Built LeanCert.Core.TrigReduction (2.7s)
✔ [3813/3822] Built LeanCert.Core.Taylor (5.0s)
✔ [3814/3823] Built LeanCert.Core.IntervalRat.Taylor (9.5s)
✔ [3815/3823] Built LeanCert.Core.IntervalRat.TrigReduced (2.6s)
✔ [3816/3824] Built LeanCert.Core.IntervalReal (2.2s)
✔ [3817/3825] Built LeanCert.Core.IntervalRealEndpoints (3.1s)
✔ [3818/3826] Built LeanCert.Engine.Eval.Core (4.8s)
✔ [3819/3826] Built LeanCert.Engine.Eval.Extended (3.1s)
✔ [3820/3828] Built LeanCert.Tactic.Bound.Lemmas (2.7s)
✔ [3821/3833] Built LeanCert.Engine.IntervalEval (2.3s)
✔ [3822/3833] Built LeanCert.Contrib.Sinc (3.3s)
✔ [3823/3833] Built LeanCert.Engine.AD.Basic (2.4s)
✔ [3824/3833] Built LeanCert.Engine.AD.Transcendental (3.3s)
✔ [3825/3833] Built LeanCert.Engine.AD.Eval (2.3s)
✔ [3826/3833] Built LeanCert.Engine.AD.Correctness (2.8s)
✔ [3827/3833] Built LeanCert.Engine.AD.Computable (2.9s)
✔ [3828/3833] Built LeanCert.Engine.AD.PartialCorrectness (4.8s)
✔ [3829/3833] Built LeanCert.Engine.AD (2.2s)
✔ [3830/3834] Built LeanCert.Meta.ProveSupported (13s)
✔ [3831/3834] Built LeanCert.Engine.TaylorModel.Core (5.4s)
✔ [3832/3834] Built LeanCert.Tactic.IntervalAuto.ProveCommon (4.6s)
✔ [3833/3837] Built LeanCert.Tactic.IntervalAuto.Basic (2.9s)
✔ [3835/3837] Built LeanCert.Engine.TaylorModel.ExpLog (5.2s)
✔ [3836/3838] Built LeanCert.Engine.TaylorModel.Trig (6.3s)
✔ [3845/3853] Built LeanCert.Engine.TaylorModel.Special (2.5s)
✔ [3846/3853] Built LeanCert.Engine.Integrate (4.2s)
✔ [3847/3853] Built LeanCert.Engine.TaylorModel.Hyperbolic (7.8s)
✔ [3848/3856] Built LeanCert.Engine.TaylorModel.Integral (2.9s)
✔ [3849/3856] Built LeanCert.Engine.TaylorModel.Functions (2.4s)
✔ [3850/3856] Built LeanCert.Core.Dyadic (2.2s)
✔ [3851/3856] Built LeanCert.Engine.TaylorModel.Expr (3.5s)
✔ [3852/3856] Built LeanCert.Core.IntervalDyadic (5.3s)
✔ [3853/3860] Built LeanCert.Engine.TaylorModel (2.3s)
✔ [3854/3860] Built LeanCert.Engine.IntervalEvalDyadic (3.3s)
✔ [3855/3861] Built LeanCert.Engine.IntervalEvalRefined (3.0s)
✔ [3856/3861] Built LeanCert.Engine.Affine.Basic (4.2s)
✔ [3857/3861] Built LeanCert.Engine.Optimization.Box (2.5s)
✔ [3858/3864] Built LeanCert.Engine.Affine.Nonlinear (3.6s)
✔ [3859/3864] Built LeanCert.Engine.Affine.Transcendental (3.0s)
✔ [3860/3864] Built LeanCert.Engine.Optimize (4.2s)
✔ [3861/3865] Built LeanCert.Engine.IntervalEvalAffine (3.3s)
✔ [3862/3866] Built LeanCert.Engine.Optimization.Gradient (3.7s)
✔ [3863/3866] Built LeanCert.Engine.RootFinding.Basic (3.4s)
✔ [3864/3867] Built LeanCert.Engine.Optimization.Global (10s)
✔ [3865/3868] Built LeanCert.Engine.RootFinding.Bisection (3.5s)
✔ [3866/3870] Built LeanCert.Engine.RootFinding.Newton (3.3s)
✔ [3867/3871] Built LeanCert.Engine.RootFinding.MVTBounds (4.2s)
✔ [3868/3871] Built LeanCert.Engine.RootFinding.Contraction (3.8s)
✔ [3869/3871] Built LeanCert.Meta.ProveContinuous (11s)
✔ [3870/3873] Built LeanCert.Engine.RootFinding.Main (2.3s)
✔ [3871/3874] Built LeanCert.Validity.Bounds.Core (2.4s)
✔ [3872/3876] Built LeanCert.Validity.Bounds.WithInv (2.4s)
✔ [3873/3878] Built LeanCert.Validity.Bounds.Smart (2.5s)
✔ [3874/3879] Built LeanCert.Validity.Bounds.Bridge (2.5s)
✔ [3875/3879] Built LeanCert.Validity.Integration (3.7s)
✔ [3876/3881] Built LeanCert.Validity.Bounds.Basic (2.2s)
✔ [3877/3881] Built LeanCert.Validity.DyadicBounds (2.5s)
✔ [3878/3882] Built LeanCert.Validity.Bounds (5.6s)
✔ [3879/3883] Built LeanCert.Engine.Optimization.BoundVerify (2.7s)
✔ [3880/3883] Built LeanCert.Tactic.IntervalAuto.Multivariate (4.4s)
✔ [3881/3884] Built LeanCert.Tactic.IntervalAuto.Bound (21s)
✔ [3882/3885] Built LeanCert.Tactic.IntervalAuto.OptBound (3.2s)
✔ [3883/3886] Built LeanCert.Tactic.IntervalAuto.RootBound (3.1s)
✔ [3884/3889] Built LeanCert.Tactic.IntervalAuto.PointIneq (12s)
✔ [3885/3896] Built LeanCert.Tactic.IntervalAuto.Subdiv (6.3s)
✔ [3886/3899] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.5s)
✔ [3888/3899] Built PrimeNumberTheoremAnd.GeneralMeromorphic (3.4s)
✔ [3889/3899] Built PrimeNumberTheoremAnd.HadamardFactorization (1.3s)
✔ [3890/3899] Built PrimeNumberTheoremAnd.HoffsteinLockhart (9.5s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (22s)
⚠ [3892/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (7.1s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3893/3900] Built LeanCert.Tactic.IntervalAuto (4.7s)
✔ [3895/3900] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (3.5s)
✔ [3896/3901] Built PrimeNumberTheoremAnd.IEANTN.LogTables (31s)
✔ [3898/3901] Built PrimeNumberTheoremAnd.IEANTN.Mertens (56s)
✔ [3899/3901] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (15s)
✔ [3957/3972] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (3.1s)
✔ [3959/3972] Built LeanCert.Engine.TaylorModel.Log1p (4.5s)
✔ [3961/3972] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (6.0s)
✔ [3962/3972] Built LeanCert.Examples.Li2Base (2.0s)
✔ [3963/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (60s)
✔ [3964/3974] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (43s)
⚠ [3965/3974] Built LeanCert.Examples.Li2Bounds (2.0s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3966/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (68s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3968/3976] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (10s)
✔ [3969/3976] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.2s)
✔ [3970/3977] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (4.0s)
✔ [3974/3978] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (8.1s)
⚠ [3975/3978] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (8.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [4107/4114] Built PrimeNumberTheoremAnd.IEANTN.Buthe (15s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4108/4114] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (47s)
✔ [4109/4117] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (28s)
⚠ [4110/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (159s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4111/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (175s)
⚠ [4112/4118] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (149s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4113/4118] Built LeanCert.Engine.FinSumDyadic (33s)
⚠ [4114/4118] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (178s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4115/4118] Built LeanCert.Examples.BKLNW_a2_base (54s)
✔ [4116/4122] Built LeanCert.Engine.WitnessSum (5.1s)
✔ [4117/4146] Built LeanCert.Engine.ReflectiveSum (4.5s)
✔ [4118/4147] Built LeanCert.Tactic.VecUtil (2.5s)
✔ [4119/4147] Built LeanCert.Tactic.FinSumExpand (1.7s)
✔ [4121/4149] Built LeanCert.Examples.BKLNW_a2_reflective (94s)
✔ [4122/4149] Built LeanCert.Examples.BKLNW_a2_bounds (3.2s)
✔ [4123/4150] Built LeanCert.Examples.BKLNW_a2_pow2 (3.2s)
✔ [4125/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (139s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (171s)
✔ [4131/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (172s)
✔ [4132/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (169s)
✔ [4133/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (212s)
✔ [4134/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (186s)
✔ [4135/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (199s)
✔ [4136/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (195s)
✔ [4137/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (196s)
✔ [4138/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (178s)
✔ [4139/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (194s)
✔ [4140/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (226s)
✔ [4141/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (231s)
✔ [4142/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (225s)
✔ [4143/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (239s)
✔ [4144/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (217s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-558-runtime-lean_checker-223748-1782159678716904616-1

$ lake build :blueprint
exit_code=None duration_ms=7200008
stdout:
✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (1.8s)
✔ [17/35] Built Architect.Basic:c.o (907ms)
✔ [18/35] Built Architect.Command:c.o (265ms)
✔ [19/35] Built Architect.Content:c.o (228ms)
✔ [20/35] Built Architect.Attribute:c.o (942ms)
✔ [21/35] Built Architect.CollectUsed:c.o (160ms)
✔ [22/35] Built Architect.Tactic:c.o (796ms)
✔ [23/35] Built Architect.Output:c.o (2.3s)
✔ [24/35] Built Architect.Load:c.o (170ms)
✔ [25/35] Built Architect:c.o (76ms)
✔ [27/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (504ms)
✔ [31/35] Built Cli:c.o (77ms)
✔ [32/35] Built Main (12s)
✔ [33/35] Built Main:c.o (260ms)
✔ [34/35] Built extract_blueprint:exe (6.2s)
✔ [2103/2106] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (55s)
✔ [3034/3041] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (24s)
✔ [3055/3066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (3.3s)
✔ [3084/3085] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (42s)
✔ [3576/3592] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (4.5s)
✔ [3577/3592] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (3.2s)
✔ [3581/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (19s)
✔ [3582/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.4s)
✔ [3586/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (61s)
✔ [3589/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMaclaurin:blueprint (5.5s)
✔ [3596/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (14s)
✔ [3599/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.4s)
✔ [3600/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (1.8s)
✔ [3601/3633] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (64s)
✔ [3610/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (3.9s)
✔ [3611/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (3.3s)
✔ [3613/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (2.7s)
✔ [3616/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.6s)
✔ [3618/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.7s)
✔ [3619/3640] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.5s)
✔ [3622/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.5s)
✔ [3623/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.5s)
✔ [3626/3645] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.4s)
✔ [3630/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.4s)
✔ [3634/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.4s)
✔ [3639/3653] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.5s)
✔ [3642/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.5s)
✔ [3647/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.5s)
✔ [3650/3658] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.5s)
✔ [3666/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (1.0s)
✔ [3667/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic:blueprint (2.4s)
✔ [3668/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic:blueprint (1.0s)
✔ [3673/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog:blueprint (1.9s)
✔ [3675/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (34s)
✔ [3676/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (923ms)
✔ [3679/3698] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (1.0s)
✔ [3680/3698] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (5.7s)
ℹ [3681/3698] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3684/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (94s)
✔ [3693/3707] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (5.9s)
✔ [3696/3715] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth:blueprint (2.5s)
✔ [3701/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (3.3s)
✔ [3704/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.8s)
✔ [3707/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (8.2s)
✔ [3712/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (3.5s)
⚠ [3715/3727] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3716/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.6s)
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (60s)
✔ [3721/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3723/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (13s)
✔ [3724/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (3.2s)
✔ [3726/3731] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (3.6s)
⚠ [3850/3857] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3853/3857] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (67s)
✔ [3855/3866] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (21s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3969/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (3.7s)
✔ [3970/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.3s)
✔ [3971/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (3.8s)
✔ [3972/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (5.6s)
✔ [3973/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.3s)
✔ [3977/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.2s)
✔ [3978/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (5.2s)
✔ [3981/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (6.6s)
✔ [3982/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (53s)
✔ [4041/4064] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (3.2s)
✔ [4048/4066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.1s)
✔ [4049/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (121s)
⚠ [4050/4067] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [4051/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [4054/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (32s)
✔ [4057/4069] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (159s)
✔ [4061/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (104s)
⚠ [4062/4070] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [4063/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (14s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (69s)
✔ [4068/4072] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (203s)
✔ [4069/4072] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (235s)
⚠ [4198/4213] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4202/4216] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (180s)
✔ [4203/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (4.8s)
⚠ [4204/4217] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4205/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (97s)
⚠ [4206/4217] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4209/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (251s)
✔ [4210/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (206s)
✔ [4211/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (165s)
⚠ [4213/4268] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4216/4272] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (252s)
✔ [4228/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (213s)
✔ [4231/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (187s)
✔ [4243/4290] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (209s)
✔ [4247/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (210s)
✔ [4248/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (202s)
✔ [4249/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (214s)
✔ [4250/4290] Built LeanCert.Engine.Chebyshev.Psi (34s)
✔ [4251/4290] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (139s)
✔ [4252/4292] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (74s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-558-runtime-blueprint_build-223748-1782166889510705715-2

blueprint_build failed; continuing (non-fatal phase).

Command runs

git_clone exit 0 duration 1s · created 6/23/2026, 12:21:40 AM

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-558-source

Cloning into '/var/lib/apodeixis/repos/job-558-source'...

git_checkout exit 0 duration 29 ms · created 6/23/2026, 12:21:40 AM

git checkout 4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb

Note: switching to '4af1d5421f85cf50a50df17d4dbc3faf1e09dfeb'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 4af1d54 Remove upstreamed lemmas and attributes (#1621)

lake_cache exit 0 duration 2m 44s · created 6/23/2026, 12:21:40 AM

lake exe cache get

Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 file(s)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'db127794c79fdeb86f6b0cf6ff2c804026fbaff1'
info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision 'f699a3e5d3efb381b9ddfb61a1ca51be25f456bd'
info: leancert: cloning https://github.com/alerad/leancert.git
info: leancert: checking out revision '33a9d1762b284fe1914d481d6a8158520e14708e'
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision 'f38c848196b0467e7b9dcc3d129a866b4051c23c'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fc38104235ab6cf8a448a74405aa258804ef4e36'
✔ [1/5] Built Cache.Cli (929ms)
✔ [3/11] Built Cache.Lean (535ms)
✔ [6/11] Built Cache.Infra (618ms)
✔ [7/12] Built Cache.IO (1.8s)
✔ [9/26] Built Cache.Hashing (1.0s)
✔ [10/26] Built Cache.Requests (2.2s)
✔ [11/26] Built Cache.Cli:c.o (1.3s)
✔ [12/26] Built Cache.Lean:c.o (140ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (368ms)
✔ [16/26] Built Cache.Infra:c.o (177ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (801ms)
✔ [19/26] Built Cache.Marker:c.o (108ms)
✔ [20/26] Built Cache.Query (829ms)
✔ [21/26] Built Cache.Query:c.o (232ms)
✔ [22/26] Built Cache.Warning (854ms)
✔ [23/26] Built Cache.Warning:c.o (223ms)
✔ [24/26] Built Cache.Main (1.7s)
✔ [25/26] Built Cache.Main:c.o (753ms)
✔ [26/26] Built cache:exe (5.8s)

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 12 KB/s], Decompressed: 0
Downloaded: 19 file(s) [attempted 19/8546 = 0%, 3 KB/s], Decompressed: 14
Downloaded: 43 file(s) [attempted 43/8546 = 0%, 20 KB/s], Decompressed: 37
Downloaded: 64 file(s) [attempted 64/8546 = 0%, 195 KB/s], Decompressed: 54
Downloaded: 91 file(s) [attempted 91/8546 = 1%, 427 KB/s], Decompressed: 74
Downloaded: 115 file(s) [attempted 115/8546 = 1%, 112 KB/s], Decompressed: 92
Downloaded: 150 file(s) [attempted 150/8546 = 1%, 127 KB/s], Decompressed: 109
Downloaded: 189 file(s) [attempted 189/8546 = 2%, 739 KB/s], Decompressed: 156
Downloaded: 221 file(s) [attempted 221/8546 = 2%, 443 KB/s], Decompressed: 183
Downloaded: 255 file(s) [attempted 255/8546 = 2%, 116 KB/s], Decompressed: 217
Downloaded: 292 file(s) [attempted 292/8546 = 3%, 96 KB/s], Decompressed: 217
Downloaded: 332 file(s) [attempted 332/8546 = 3%, 689 KB/s], Decompressed: 251
Downloaded: 371 file(s) [attempted 371/8546 = 4%, 86 KB/s], Decompressed: 251
Downloaded: 410 file(s) [attempted 410/8546 = 4%, 78 KB/s], Decompressed: 312
Downloaded: 444 file(s) [attempted 444/8546 = 5%, 79 KB/s], Decompressed: 312
Downloaded: 481 file(s) [attempted 481/8546 = 5%, 254 KB/s], Decompressed: 373
Downloaded: 515 file(s) [attempted 515/8546 = 6%, 222 KB/s], Decompressed: 373
Downloaded: 559 file(s) [attempted 559/8546 = 6%, 280 KB/s], Decompressed: 448
Downloaded: 603 file(s) [attempted 603/8546 = 7%, 260 KB/s], Decompressed: 448
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 137 KB/s], Decompressed: 448
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 61 KB/s], Decompressed: 539
Downloaded: 715 file(s) [attempted 715/8546 = 8%, 422 KB/s], Decompressed: 539
Downloaded: 756 file(s) [attempted 756/8546 = 8%, 423 KB/s], Decompressed: 539
Downloaded: 796 file(s) [attempted 796/8546 = 9%, 340 KB/s], Decompressed: 657
Downloaded: 837 file(s) [attempted 837/8546 = 9%, 823 KB/s], Decompressed: 657
Downloaded: 871 file(s) [attempted 871/8546 = 10%, 541 KB/s], Decompressed: 657
Downloaded: 911 file(s) [attempted 911/8546 = 10%, 191 KB/s], Decompressed: 657
Downloaded: 954 file(s) [attempted 954/8546 = 11%, 165 KB/s], Decompressed: 796
Downloaded: 989 file(s) [attempted 989/8546 = 11%, 711 KB/s], Decompressed: 796
Downloaded: 1033 file(s) [attempted 1033/8546 = 12%, 166 KB/s], Decompressed: 796
Downloaded: 1060 file(s) [attempted 1060/8546 = 12%, 159 KB/s], Decompressed: 796
Downloaded: 1101 file(s) [attempted 1101/8546 = 12%, 61 KB/s], Decompressed: 796
Downloaded: 1148 file(s) [attempted 1148/8546 = 13%, 273 KB/s], Decompressed: 796
Downloaded: 1199 file(s) [attempted 1199/8546 = 14%, 151 KB/s], Decompressed: 952
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 1134 KB/s], Decompressed: 952
Downloaded: 1291 file(s) [attempted 1291/8546 = 15%, 1086 KB/s], Decompressed: 952
Downloaded: 1335 file(s) [attempted 1335/8546 = 15%, 733 KB/s], Decompressed: 952
Downloaded: 1365 file(s) [attempted 1365/8546 = 15%, 131 KB/s], Decompressed: 952
Downloaded: 1399 file(s) [attempted 1399/8546 = 16%, 179 KB/s], Decompressed: 952
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 649 KB/s], Decompressed: 952
Downloaded: 1490 file(s) [attempted 1490/8546 = 17%, 130 KB/s], Decompressed: 1179
Downloaded: 1531 file(s) [attempted 1531/8546 = 17%, 71 KB/s], Decompressed: 1179
Downloaded: 1554 file(s) [attempted 1554/8546 = 18%, 343 KB/s], Decompressed: 1179
Downloaded: 1598 file(s) [attempted 1598/8546 = 18%, 397 KB/s], Decompressed: 1179
Downloaded: 1642 file(s) [attempted 1642/8546 = 19%, 644 KB/s], Decompressed: 1179
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 113 KB/s], Decompressed: 1179
Downloaded: 1713 file(s) [attempted 1713/8546 = 20%, 411 KB/s], Decompressed: 1179
Downloaded: 1754 file(s) [attempted 1754/8546 = 20%, 181 KB/s], Decompressed: 1179
Downloaded: 1801 file(s) [attempted 1801/8546 = 21%, 69 KB/s], Decompressed: 1179
Downloaded: 1849 file(s) [attempted 1849/8546 = 21%, 1006 KB/s], Decompressed: 1490
Downloaded: 1889 file(s) [attempted 1889/8546 = 22%, 202 KB/s], Decompressed: 1490
Downloaded: 1933 file(s) [attempted 1933/8546 = 22%, 674 KB/s], Decompressed: 1490
Downloaded: 1964 file(s) [attempted 1964/8546 = 22%, 409 KB/s], Decompressed: 1490
Downloaded: 2001 file(s) [attempted 2001/8546 = 23%, 73 KB/s], Decompressed: 1490
Downloaded: 2048 file(s) [attempted 2048/8546 = 23%, 119 KB/s], Decompressed: 1490
Downloaded: 2096 file(s) [attempted 2096/8546 = 24%, 235 KB/s], Decompressed: 1490
Downloaded: 2136 file(s) [attempted 2136/8546 = 24%, 1149 KB/s], Decompressed: 1490
Downloaded: 2177 file(s) [attempted 2177/8546 = 25%, 111 KB/s], Decompressed: 1811
Downloaded: 2207 file(s) [attempted 2207/8546 = 25%, 931 KB/s], Decompressed: 1811
Downloaded: 2244 file(s) [attempted 2244/8546 = 26%, 249 KB/s], Decompressed: 1811
Downloaded: 2288 file(s) [attempted 2288/8546 = 26%, 473 KB/s], Decompressed: 1811
Downloaded: 2322 file(s) [attempted 2322/8546 = 27%, 190 KB/s], Decompressed: 1811
Downloaded: 2363 file(s) [attempted 2363/8546 = 27%, 351 KB/s], Decompressed: 1811
Downloaded: 2403 file(s) [attempted 2403/8546 = 28%, 434 KB/s], Decompressed: 1811
Downloaded: 2444 file(s) [attempted 2444/8546 = 28%, 903 KB/s], Decompressed: 1811
Downloaded: 2485 file(s) [attempted 2485/8546 = 29%, 62 KB/s], Decompressed: 1811
Downloaded: 2522 file(s) [attempted 2522/8546 = 29%, 329 KB/s], Decompressed: 1811
Downloaded: 2559 file(s) [attempted 2559/8546 = 29%, 566 KB/s], Decompressed: 1811
Downloaded: 2600 file(s) [attempted 2600/8546 = 30%, 160 KB/s], Decompressed: 1811
Downloaded: 2637 file(s) [attempted 2637/8546 = 30%, 388 KB/s], Decompressed: 2167
Downloaded: 2677 file(s) [attempted 2677/8546 = 31%, 247 KB/s], Decompressed: 2167
Downloaded: 2718 file(s) [attempted 2718/8546 = 31%, 55 KB/s], Decompressed: 2167
Downloaded: 2755 file(s) [attempted 2755/8546 = 32%, 152 KB/s], Decompressed: 2167
Downloaded: 2796 file(s) [attempted 2796/8546 = 32%, 81 KB/s], Decompressed: 2167
Downloaded: 2840 file(s) [attempted 2840/8546 = 33%, 82 KB/s], Decompressed: 2167
Downloaded: 2877 file(s) [attempted 2877/8546 = 33%, 251 KB/s], Decompressed: 2167
Downloaded: 2918 file(s) [attempted 2918/8546 = 34%, 822 KB/s], Decompressed: 2167
Downloaded: 2955 file(s) [attempted 2955/8546 = 34%, 723 KB/s], Decompressed: 2167
Downloaded: 2995 file(s) [attempted 2995/8546 = 35%, 37 KB/s], Decompressed: 2167
Downloaded: 3039 file(s) [attempted 3039/8546 = 35%, 233 KB/s], Decompressed: 2167
Downloaded: 3067 file(s) [attempted 3067/8546 = 35%, 270 KB/s], Decompressed: 2167
Downloaded: 3114 file(s) [attempted 3114/8546 = 36%, 494 KB/s], Decompressed: 2167
Downloaded: 3165 file(s) [attempted 3165/8546 = 37%, 1689 KB/s], Decompressed: 2167
Downloaded: 3215 file(s) [attempted 3215/8546 = 37%, 191 KB/s], Decompressed: 2634
Downloaded: 3263 file(s) [attempted 3263/8546 = 38%, 258 KB/s], Decompressed: 2634
Downloaded: 3293 file(s) [attempted 3293/8546 = 38%, 309 KB/s], Decompressed: 2634
Downloaded: 3334 file(s) [attempted 3334/8546 = 39%, 153 KB/s], Decompressed: 2634
Downloaded: 3364 file(s) [attempted 3364/8546 = 39%, 708 KB/s], Decompressed: 2634
Downloaded: 3401 file(s) [attempted 3401/8546 = 39%, 41 KB/s], Decompressed: 2634
Downloaded: 3449 file(s) [attempted 3449/8546 = 40%, 178 KB/s], Decompressed: 2634
Downloaded: 3489 file(s) [attempted 3489/8546 = 40%, 206 KB/s], Decompressed: 2634
Downloaded: 3533 file(s) [attempted 3533/8546 = 41%, 264 KB/s], Decompressed: 2634
Downloaded: 3567 file(s) [attempted 3567/8546 = 41%, 66 KB/s], Decompressed: 2634
Downloaded: 3604 file(s) [attempted 3604/8546 = 42%, 717 KB/s], Decompressed: 2634
Downloaded: 3652 file(s) [attempted 3652/8546 = 42%, 227 KB/s], Decompressed: 2634
Downloaded: 3696 file(s) [attempted 3696/8546 = 43%, 234 KB/s], Decompressed: 2634
Downloaded: 3740 file(s) [attempted 3740/8546 = 43%, 1801 KB/s], Decompressed: 2634
Downloaded: 3777 file(s) [attempted 3777/8546 = 44%, 92 KB/s], Decompressed: 2634
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 99 KB/s], Decompressed: 2634
Downloaded: 3848 file(s) [attempted 3848/8546 = 45%, 359 KB/s], Decompressed: 3178
Downloaded: 3892 file(s) [attempted 3892/8546 = 45%, 725 KB/s], Decompressed: 3178
Downloaded: 3939 file(s) [attempted 3939/8546 = 46%, 158 KB/s], Decompressed: 3178
Downloaded: 3976 file(s) [attempted 3976/8546 = 46%, 22 KB/s], Decompressed: 3178
Downloaded: 4010 file(s) [attempted 4010/8546 = 46%, 310 KB/s], Decompressed: 3178
Downloaded: 4048 file(s) [attempted 4048/8546 = 47%, 881 KB/s], Decompressed: 3178
Downloaded: 4092 file(s) [attempted 4092/8546 = 47%, 1413 KB/s], Decompressed: 3178
Downloaded: 4139 file(s) [attempted 4139/8546 = 48%, 3619 KB/s], Decompressed: 3178
Downloaded: 4173 file(s) [attempted 4173/8546 = 48%, 274 KB/s], Decompressed: 3178
Downloaded: 4213 file(s) [attempted 4213/8546 = 49%, 296 KB/s], Decompressed: 3178
Downloaded: 4254 file(s) [attempted 4254/8546 = 49%, 437 KB/s], Decompressed: 3178
Downloaded: 4294 file(s) [attempted 4294/8546 = 50%, 609 KB/s], Decompressed: 3178
Downloaded: 4342 file(s) [attempted 4342/8546 = 50%, 161 KB/s], Decompressed: 3178
Downloaded: 4380 file(s) [attempted 4380/8546 = 51%, 205 KB/s], Decompressed: 3178
Downloaded: 4409 file(s) [attempted 4409/8546 = 51%, 379 KB/s], Decompressed: 3178
Downloaded: 4453 file(s) [attempted 4453/8546 = 52%, 74 KB/s], Decompressed: 3178
Downloaded: 4497 file(s) [attempted 4497/8546 = 52%, 36 KB/s], Decompressed: 3178
Downloaded: 4541 file(s) [attempted 4541/8546 = 53%, 225 KB/s], Decompressed: 3178
Downloaded: 4572 file(s) [attempted 4572/8546 = 53%, 53 KB/s], Decompressed: 3178
Downloaded: 4609 file(s) [attempted 4609/8546 = 53%, 34 KB/s], Decompressed: 3178
Downloaded: 4650 file(s) [attempted 4650/8546 = 54%, 23 KB/s], Decompressed: 3814
Downloaded: 4694 file(s) [attempted 4694/8546 = 54%, 58 KB/s], Decompressed: 3814
Downloaded: 4741 file(s) [attempted 4741/8546 = 55%, 1046 KB/s], Decompressed: 3814
Downloaded: 4775 file(s) [attempted 4775/8546 = 55%, 374 KB/s], Decompressed: 3814
Downloaded: 4810 file(s) [attempted 4810/8546 = 56%, 361 KB/s], Decompressed: 3814
Downloaded: 4849 file(s) [attempted 4849/8546 = 56%, 383 KB/s], Decompressed: 3814
Downloaded: 4893 file(s) [attempted 4893/8546 = 57%, 262 KB/s], Decompressed: 3814
Downloaded: 4937 file(s) [attempted 4937/8546 = 57%, 121 KB/s], Decompressed: 3814
Downloaded: 4974 file(s) [attempted 4974/8546 = 58%, 436 KB/s], Decompressed: 3814
Downloaded: 5012 file(s) [attempted 5012/8546 = 58%, 381 KB/s], Decompressed: 3814
Downloaded: 5052 file(s) [attempted 5052/8546 = 59%, 239 KB/s], Decompressed: 3814
Downloaded: 5093 file(s) [attempted 5093/8546 = 59%, 418 KB/s], Decompressed: 3814
Downloaded: 5133 file(s) [attempted 5133/8546 = 60%, 107 KB/s], Decompressed: 3814
Downloaded: 5167 file(s) [attempted 5167/8546 = 60%, 216 KB/s], Decompressed: 3814
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 220 KB/s], Decompressed: 3814
Downloaded: 5248 file(s) [attempted 5248/8546 = 61%, 231 KB/s], Decompressed: 3814
Downloaded: 5289 file(s) [attempted 5289/8546 = 61%, 102 KB/s], Decompressed: 3814
Downloaded: 5323 file(s) [attempted 5323/8546 = 62%, 436 KB/s], Decompressed: 3814
Downloaded: 5360 file(s) [attempted 5360/8546 = 62%, 284 KB/s], Decompressed: 3814
Downloaded: 5401 file(s) [attempted 5401/8546 = 63%, 245 KB/s], Decompressed: 3814
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 56 KB/s], Decompressed: 3814
Downloaded: 5485 file(s) [attempted 5485/8546 = 64%, 280 KB/s], Decompressed: 3814
Downloaded: 5516 file(s) [attempted 5516/8546 = 64%, 257 KB/s], Decompressed: 3814
Downloaded: 5556 file(s) [attempted 5556/8546 = 65%, 225 KB/s], Decompressed: 3814
Downloaded: 5600 file(s) [attempted 5600/8546 = 65%, 125 KB/s], Decompressed: 4619
Downloaded: 5645 file(s) [attempted 5645/8546 = 66%, 153 KB/s], Decompressed: 4619
Downloaded: 5685 file(s) [attempted 5685/8546 = 66%, 285 KB/s], Decompressed: 4619
Downloaded: 5715 file(s) [attempted 5715/8546 = 66%, 521 KB/s], Decompressed: 4619
Downloaded: 5759 file(s) [attempted 5759/8546 = 67%, 601 KB/s], Decompressed: 4619
Downloaded: 5800 file(s) [attempted 5800/8546 = 67%, 94 KB/s], Decompressed: 4619
Downloaded: 5847 file(s) [attempted 5847/8546 = 68%, 139 KB/s], Decompressed: 4619
Downloaded: 5895 file(s) [attempted 5895/8546 = 68%, 103 KB/s], Decompressed: 4619
Downloaded: 5928 file(s) [attempted 5928/8546 = 69%, 101 KB/s], Decompressed: 4619
Downloaded: 5959 file(s) [attempted 5959/8546 = 69%, 96 KB/s], Decompressed: 4619
Downloaded: 5999 file(s) [attempted 5999/8546 = 70%, 144 KB/s], Decompressed: 4619
Downloaded: 6040 file(s) [attempted 6040/8546 = 70%, 200 KB/s], Decompressed: 4619
Downloaded: 6077 file(s) [attempted 6077/8546 = 71%, 63 KB/s], Decompressed: 4619
Downloaded: 6114 file(s) [attempted 6114/8546 = 71%, 37 KB/s], Decompressed: 4619
Downloaded: 6148 file(s) [attempted 6148/8546 = 71%, 107 KB/s], Decompressed: 4619
Downloaded: 6192 file(s) [attempted 6192/8546 = 72%, 1765 KB/s], Decompressed: 4619
Downloaded: 6236 file(s) [attempted 6236/8546 = 72%, 58 KB/s], Decompressed: 4619
Downloaded: 6270 file(s) [attempted 6270/8546 = 73%, 101 KB/s], Decompressed: 4619
Downloaded: 6311 file(s) [attempted 6311/8546 = 73%, 63 KB/s], Decompressed: 4619
Downloaded: 6344 file(s) [attempted 6344/8546 = 74%, 271 KB/s], Decompressed: 4619
Downloaded: 6388 file(s) [attempted 6388/8546 = 74%, 1387 KB/s], Decompressed: 4619
Downloaded: 6429 file(s) [attempted 6429/8546 = 75%, 1318 KB/s], Decompressed: 4619
Downloaded: 6466 file(s) [attempted 6466/8546 = 75%, 94 KB/s], Decompressed: 4619
Downloaded: 6504 file(s) [attempted 6504/8546 = 76%, 125 KB/s], Decompressed: 4619
Downloaded: 6544 file(s) [attempted 6544/8546 = 76%, 50 KB/s], Decompressed: 4619
Downloaded: 6591 file(s) [attempted 6591/8546 = 77%, 243 KB/s], Decompressed: 4619
Downloaded: 6642 file(s) [attempted 6642/8546 = 77%, 130 KB/s], Decompressed: 4619
Downloaded: 6693 file(s) [attempted 6693/8546 = 78%, 1003 KB/s], Decompressed: 5566
Downloaded: 6740 file(s) [attempted 6740/8546 = 78%, 77 KB/s], Decompressed: 5566
Downloaded: 6784 file(s) [attempted 6784/8546 = 79%, 49 KB/s], Decompressed: 5566
Downloaded: 6818 file(s) [attempted 6818/8546 = 79%, 678 KB/s], Decompressed: 5566
Downloaded: 6852 file(s) [attempted 6852/8546 = 80%, 83 KB/s], Decompressed: 5566
Downloaded: 6892 file(s) [attempted 6892/8546 = 80%, 227 KB/s], Decompressed: 5566
Downloaded: 6940 file(s) [attempted 6940/8546 = 81%, 147 KB/s], Decompressed: 5566
Downloaded: 6987 file(s) [attempted 6987/8546 = 81%, 187 KB/s], Decompressed: 5566
Downloaded: 7031 file(s) [attempted 7031/8546 = 82%, 83 KB/s], Decompressed: 5566
Downloaded: 7062 file(s) [attempted 7062/8546 = 82%, 150 KB/s], Decompressed: 5566
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 201 KB/s], Decompressed: 5566
Downloaded: 7139 file(s) [attempted 7139/8546 = 83%, 238 KB/s], Decompressed: 5566
Downloaded: 7187 file(s) [attempted 7187/8546 = 84%, 380 KB/s], Decompressed: 5566
Downloaded: 7221 file(s) [attempted 7221/8546 = 84%, 108 KB/s], Decompressed: 5566
Downloaded: 7258 file(s) [attempted 7258/8546 = 84%, 896 KB/s], Decompressed: 5566
Downloaded: 7298 file(s) [attempted 7298/8546 = 85%, 315 KB/s], Decompressed: 5566
Downloaded: 7339 file(s) [attempted 7339/8546 = 85%, 601 KB/s], Decompressed: 5566
Downloaded: 7386 file(s) [attempted 7386/8546 = 86%, 348 KB/s], Decompressed: 5566
Downloaded: 7427 file(s) [attempted 7427/8546 = 86%, 307 KB/s], Decompressed: 5566
Downloaded: 7464 file(s) [attempted 7464/8546 = 87%, 441 KB/s], Decompressed: 5566
Downloaded: 7501 file(s) [attempted 7501/8546 = 87%, 368 KB/s], Decompressed: 5566
Downloaded: 7542 file(s) [attempted 7542/8546 = 88%, 83 KB/s], Decompressed: 5566
Downloaded: 7579 file(s) [attempted 7579/8546 = 88%, 148 KB/s], Decompressed: 5566
Downloaded: 7623 file(s) [attempted 7623/8546 = 89%, 151 KB/s], Decompressed: 5566
Downloaded: 7660 file(s) [attempted 7660/8546 = 89%, 155 KB/s], Decompressed: 5566
Downloaded: 7702 file(s) [attempted 7702/8546 = 90%, 50 KB/s], Decompressed: 5566
Downloaded: 7731 file(s) [attempted 7731/8546 = 90%, 381 KB/s], Decompressed: 5566
Downloaded: 7775 file(s) [attempted 7775/8546 = 90%, 959 KB/s], Decompressed: 5566
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 128 KB/s], Decompressed: 5566
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 1663 KB/s], Decompressed: 5566
Downloaded: 7901 file(s) [attempted 7901/8546 = 92%, 1037 KB/s], Decompressed: 5566
Downloaded: 7938 file(s) [attempted 7938/8546 = 92%, 42 KB/s], Decompressed: 5566
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 1025 KB/s], Decompressed: 5566
Downloaded: 8022 file(s) [attempted 8022/8546 = 93%, 253 KB/s], Decompressed: 5566
Downloaded: 8063 file(s) [attempted 8063/8546 = 94%, 830 KB/s], Decompressed: 5566
Downloaded: 8097 file(s) [attempted 8097/8546 = 94%, 144 KB/s], Decompressed: 6686
Downloaded: 8141 file(s) [attempted 8141/8546 = 95%, 162 KB/s], Decompressed: 6686
Downloaded: 8181 file(s) [attempted 8181/8546 = 95%, 706 KB/s], Decompressed: 6686
Downloaded: 8219 file(s) [attempted 8219/8546 = 96%, 982 KB/s], Decompressed: 6686
Downloaded: 8263 file(s) [attempted 8263/8546 = 96%, 51 KB/s], Decompressed: 6686
Downloaded: 8300 file(s) [attempted 8300/8546 = 97%, 403 KB/s], Decompressed: 6686
Downloaded: 8337 file(s) [attempted 8337/8546 = 97%, 299 KB/s], Decompressed: 6686
Downloaded: 8367 file(s) [attempted 8367/8546 = 97%, 81 KB/s], Decompressed: 6686
Downloaded: 8411 file(s) [attempted 8411/8546 = 98%, 317 KB/s], Decompressed: 6686
Downloaded: 8452 file(s) [attempted 8452/8546 = 98%, 848 KB/s], Decompressed: 6686
Downloaded: 8489 file(s) [attempted 8489/8546 = 99%, 48 KB/s], Decompressed: 6686
Downloaded: 8530 file(s) [attempted 8530/8546 = 99%, 850 KB/s], Decompressed: 6686
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 850 KB/s], Decompressed: 6686

lean_checker exit - duration 2h 0m · created 6/23/2026, 12:21:40 AM

lake build

✔ [2071/2074] Built PrimeNumberTheoremAnd.Auxiliary (41s)
✔ [3002/3008] Built PrimeNumberTheoremAnd.Sobolev (76s)
✔ [3021/3022] Built PrimeNumberTheoremAnd.Fourier (116s)
✔ [3022/3027] Built Architect.Basic (8.3s)
✔ [3023/3027] Built Architect.Command (903ms)
✔ [3024/3027] Built Architect.CollectUsed (951ms)
✔ [3025/3027] Built Architect.Content (945ms)
✔ [3026/3031] Built Architect.Attribute (1.6s)
✔ [3027/3032] Built Architect.Tactic (1.3s)
✔ [3028/3032] Built Architect.Output (1.9s)
✔ [3030/3033] Built Architect.Load (861ms)
✔ [3031/3040] Built Architect (827ms)
✔ [3059/3060] Built PrimeNumberTheoremAnd.Defs (141s)
✔ [3544/3554] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (32s)
✔ [3546/3554] Built PrimeNumberTheoremAnd.Rectangle (16s)
✔ [3550/3555] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.3s)
✔ [3552/3560] Built PrimeNumberTheoremAnd.ZetaConj (134s)
✔ [3554/3561] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (177s)
✔ [3557/3562] Built PrimeNumberTheoremAnd.EulerMaclaurin (7.3s)
✔ [3561/3567] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (102s)
✔ [3563/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (8.8s)
✔ [3565/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.6s)
✔ [3566/3569] Built PrimeNumberTheoremAnd.ZetaBounds (209s)
✔ [3570/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (8.2s)
✔ [3572/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.8s)
✔ [3575/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (3.4s)
✔ [3576/3588] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (1.9s)
✔ [3577/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (2.7s)
✔ [3578/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (2.2s)
✔ [3579/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (2.0s)
✔ [3580/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (3.1s)
✔ [3582/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (2.6s)
✔ [3584/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (3.9s)
✔ [3586/3596] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.5s)
✔ [3588/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.5s)
✔ [3591/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.7s)
✔ [3594/3601] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.3s)
✔ [3596/3605] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (2.7s)
✔ [3610/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (1.8s)
✔ [3611/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (1.8s)
✔ [3613/3631] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (2.5s)
✔ [3615/3631] Built PrimeNumberTheoremAnd.MellinCalculus (64s)
✔ [3616/3631] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.9s)
✔ [3618/3632] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (3.2s)
✔ [3620/3632] Built PrimeNumberTheoremAnd.SmoothExistence (6.2s)
✔ [3622/3633] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (1.9s)
ℹ [3624/3633] Built PrimeNumberTheoremAnd.MediumPNT (133s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3632/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (11s)
✔ [3634/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (4.2s)
✔ [3636/3639] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (3.9s)
✔ [3637/3639] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (159s)
✔ [3640/3653] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (18s)
✔ [3645/3655] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (19s)
✔ [3648/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (4.7s)
✔ [3650/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (5.5s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (128s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3653/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (31s)
✔ [3654/3656] Built PrimeNumberTheoremAnd.BorelCaratheodory (92s)
✔ [3655/3656] Built PrimeNumberTheoremAnd.BrunTitchmarsh (21s)
✔ [3778/3784] Built LeanCert.Core.Interval (2.7s)
⚠ [3779/3784] Built PrimeNumberTheoremAnd.Wiener (118s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3780/3784] Built LeanCert.Core.IntervalRat.Basic (39s)
✔ [3781/3784] Built PrimeNumberTheoremAnd.Consequences (141s)
✔ [3782/3784] Built LeanCert.Tactic.IntervalAuto.Types (44s)
✔ [3783/3794] Built LeanCert.Tactic.IntervalAuto.Norm (4.2s)
✔ [3788/3794] Built LeanCert.Core.Expr (6.3s)
✔ [3789/3795] Built LeanCert.Meta.Numeral (3.2s)
✔ [3790/3795] Built LeanCert.Meta.ToExpr (4.1s)
✔ [3791/3795] Built LeanCert.Tactic.IntervalAuto.Extract (2.7s)
✔ [3792/3795] Built LeanCert.Core.Support (2.4s)
✔ [3793/3796] Built LeanCert.Tactic.IntervalAuto.Parse (4.3s)
✔ [3794/3796] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.8s)
✔ [3795/3797] Built LeanCert.Core.IntervalRat.Transcendental (3.6s)
✔ [3796/3799] Built LeanCert.Core.IntervalRat.LogReduction (3.8s)
✔ [3808/3816] Built LeanCert.Core.DerivativeIntervals (2.4s)
✔ [3812/3822] Built LeanCert.Core.TrigReduction (2.7s)
✔ [3813/3822] Built LeanCert.Core.Taylor (5.0s)
✔ [3814/3823] Built LeanCert.Core.IntervalRat.Taylor (9.5s)
✔ [3815/3823] Built LeanCert.Core.IntervalRat.TrigReduced (2.6s)
✔ [3816/3824] Built LeanCert.Core.IntervalReal (2.2s)
✔ [3817/3825] Built LeanCert.Core.IntervalRealEndpoints (3.1s)
✔ [3818/3826] Built LeanCert.Engine.Eval.Core (4.8s)
✔ [3819/3826] Built LeanCert.Engine.Eval.Extended (3.1s)
✔ [3820/3828] Built LeanCert.Tactic.Bound.Lemmas (2.7s)
✔ [3821/3833] Built LeanCert.Engine.IntervalEval (2.3s)
✔ [3822/3833] Built LeanCert.Contrib.Sinc (3.3s)
✔ [3823/3833] Built LeanCert.Engine.AD.Basic (2.4s)
✔ [3824/3833] Built LeanCert.Engine.AD.Transcendental (3.3s)
✔ [3825/3833] Built LeanCert.Engine.AD.Eval (2.3s)
✔ [3826/3833] Built LeanCert.Engine.AD.Correctness (2.8s)
✔ [3827/3833] Built LeanCert.Engine.AD.Computable (2.9s)
✔ [3828/3833] Built LeanCert.Engine.AD.PartialCorrectness (4.8s)
✔ [3829/3833] Built LeanCert.Engine.AD (2.2s)
✔ [3830/3834] Built LeanCert.Meta.ProveSupported (13s)
✔ [3831/3834] Built LeanCert.Engine.TaylorModel.Core (5.4s)
✔ [3832/3834] Built LeanCert.Tactic.IntervalAuto.ProveCommon (4.6s)
✔ [3833/3837] Built LeanCert.Tactic.IntervalAuto.Basic (2.9s)
✔ [3835/3837] Built LeanCert.Engine.TaylorModel.ExpLog (5.2s)
✔ [3836/3838] Built LeanCert.Engine.TaylorModel.Trig (6.3s)
✔ [3845/3853] Built LeanCert.Engine.TaylorModel.Special (2.5s)
✔ [3846/3853] Built LeanCert.Engine.Integrate (4.2s)
✔ [3847/3853] Built LeanCert.Engine.TaylorModel.Hyperbolic (7.8s)
✔ [3848/3856] Built LeanCert.Engine.TaylorModel.Integral (2.9s)
✔ [3849/3856] Built LeanCert.Engine.TaylorModel.Functions (2.4s)
✔ [3850/3856] Built LeanCert.Core.Dyadic (2.2s)
✔ [3851/3856] Built LeanCert.Engine.TaylorModel.Expr (3.5s)
✔ [3852/3856] Built LeanCert.Core.IntervalDyadic (5.3s)
✔ [3853/3860] Built LeanCert.Engine.TaylorModel (2.3s)
✔ [3854/3860] Built LeanCert.Engine.IntervalEvalDyadic (3.3s)
✔ [3855/3861] Built LeanCert.Engine.IntervalEvalRefined (3.0s)
✔ [3856/3861] Built LeanCert.Engine.Affine.Basic (4.2s)
✔ [3857/3861] Built LeanCert.Engine.Optimization.Box (2.5s)
✔ [3858/3864] Built LeanCert.Engine.Affine.Nonlinear (3.6s)
✔ [3859/3864] Built LeanCert.Engine.Affine.Transcendental (3.0s)
✔ [3860/3864] Built LeanCert.Engine.Optimize (4.2s)
✔ [3861/3865] Built LeanCert.Engine.IntervalEvalAffine (3.3s)
✔ [3862/3866] Built LeanCert.Engine.Optimization.Gradient (3.7s)
✔ [3863/3866] Built LeanCert.Engine.RootFinding.Basic (3.4s)
✔ [3864/3867] Built LeanCert.Engine.Optimization.Global (10s)
✔ [3865/3868] Built LeanCert.Engine.RootFinding.Bisection (3.5s)
✔ [3866/3870] Built LeanCert.Engine.RootFinding.Newton (3.3s)
✔ [3867/3871] Built LeanCert.Engine.RootFinding.MVTBounds (4.2s)
✔ [3868/3871] Built LeanCert.Engine.RootFinding.Contraction (3.8s)
✔ [3869/3871] Built LeanCert.Meta.ProveContinuous (11s)
✔ [3870/3873] Built LeanCert.Engine.RootFinding.Main (2.3s)
✔ [3871/3874] Built LeanCert.Validity.Bounds.Core (2.4s)
✔ [3872/3876] Built LeanCert.Validity.Bounds.WithInv (2.4s)
✔ [3873/3878] Built LeanCert.Validity.Bounds.Smart (2.5s)
✔ [3874/3879] Built LeanCert.Validity.Bounds.Bridge (2.5s)
✔ [3875/3879] Built LeanCert.Validity.Integration (3.7s)
✔ [3876/3881] Built LeanCert.Validity.Bounds.Basic (2.2s)
✔ [3877/3881] Built LeanCert.Validity.DyadicBounds (2.5s)
✔ [3878/3882] Built LeanCert.Validity.Bounds (5.6s)
✔ [3879/3883] Built LeanCert.Engine.Optimization.BoundVerify (2.7s)
✔ [3880/3883] Built LeanCert.Tactic.IntervalAuto.Multivariate (4.4s)
✔ [3881/3884] Built LeanCert.Tactic.IntervalAuto.Bound (21s)
✔ [3882/3885] Built LeanCert.Tactic.IntervalAuto.OptBound (3.2s)
✔ [3883/3886] Built LeanCert.Tactic.IntervalAuto.RootBound (3.1s)
✔ [3884/3889] Built LeanCert.Tactic.IntervalAuto.PointIneq (12s)
✔ [3885/3896] Built LeanCert.Tactic.IntervalAuto.Subdiv (6.3s)
✔ [3886/3899] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.5s)
✔ [3888/3899] Built PrimeNumberTheoremAnd.GeneralMeromorphic (3.4s)
✔ [3889/3899] Built PrimeNumberTheoremAnd.HadamardFactorization (1.3s)
✔ [3890/3899] Built PrimeNumberTheoremAnd.HoffsteinLockhart (9.5s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (22s)
⚠ [3892/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (7.1s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3893/3900] Built LeanCert.Tactic.IntervalAuto (4.7s)
✔ [3895/3900] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (3.5s)
✔ [3896/3901] Built PrimeNumberTheoremAnd.IEANTN.LogTables (31s)
✔ [3898/3901] Built PrimeNumberTheoremAnd.IEANTN.Mertens (56s)
✔ [3899/3901] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (15s)
✔ [3957/3972] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (3.1s)
✔ [3959/3972] Built LeanCert.Engine.TaylorModel.Log1p (4.5s)
✔ [3961/3972] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (6.0s)
✔ [3962/3972] Built LeanCert.Examples.Li2Base (2.0s)
✔ [3963/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (60s)
✔ [3964/3974] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (43s)
⚠ [3965/3974] Built LeanCert.Examples.Li2Bounds (2.0s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3966/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (68s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3968/3976] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (10s)
✔ [3969/3976] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.2s)
✔ [3970/3977] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (4.0s)
✔ [3974/3978] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (8.1s)
⚠ [3975/3978] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (8.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [4107/4114] Built PrimeNumberTheoremAnd.IEANTN.Buthe (15s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4108/4114] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (47s)
✔ [4109/4117] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (28s)
⚠ [4110/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (159s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4111/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (175s)
⚠ [4112/4118] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (149s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4113/4118] Built LeanCert.Engine.FinSumDyadic (33s)
⚠ [4114/4118] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (178s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4115/4118] Built LeanCert.Examples.BKLNW_a2_base (54s)
✔ [4116/4122] Built LeanCert.Engine.WitnessSum (5.1s)
✔ [4117/4146] Built LeanCert.Engine.ReflectiveSum (4.5s)
✔ [4118/4147] Built LeanCert.Tactic.VecUtil (2.5s)
✔ [4119/4147] Built LeanCert.Tactic.FinSumExpand (1.7s)
✔ [4121/4149] Built LeanCert.Examples.BKLNW_a2_reflective (94s)
✔ [4122/4149] Built LeanCert.Examples.BKLNW_a2_bounds (3.2s)
✔ [4123/4150] Built LeanCert.Examples.BKLNW_a2_pow2 (3.2s)
✔ [4125/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (139s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (171s)
✔ [4131/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (172s)
✔ [4132/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (169s)
✔ [4133/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (212s)
✔ [4134/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (186s)
✔ [4135/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (199s)
✔ [4136/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (195s)
✔ [4137/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (196s)
✔ [4138/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (178s)
✔ [4139/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (194s)
✔ [4140/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (226s)
✔ [4141/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (231s)
✔ [4142/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (225s)
✔ [4143/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (239s)
✔ [4144/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (217s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-558-runtime-lean_checker-223748-1782159678716904616-1

blueprint_build exit - duration 2h 0m · created 6/23/2026, 12:21:40 AM

lake build :blueprint

✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (1.8s)
✔ [17/35] Built Architect.Basic:c.o (907ms)
✔ [18/35] Built Architect.Command:c.o (265ms)
✔ [19/35] Built Architect.Content:c.o (228ms)
✔ [20/35] Built Architect.Attribute:c.o (942ms)
✔ [21/35] Built Architect.CollectUsed:c.o (160ms)
✔ [22/35] Built Architect.Tactic:c.o (796ms)
✔ [23/35] Built Architect.Output:c.o (2.3s)
✔ [24/35] Built Architect.Load:c.o (170ms)
✔ [25/35] Built Architect:c.o (76ms)
✔ [27/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (504ms)
✔ [31/35] Built Cli:c.o (77ms)
✔ [32/35] Built Main (12s)
✔ [33/35] Built Main:c.o (260ms)
✔ [34/35] Built extract_blueprint:exe (6.2s)
✔ [2103/2106] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (55s)
✔ [3034/3041] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (24s)
✔ [3055/3066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (3.3s)
✔ [3084/3085] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (42s)
✔ [3576/3592] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (4.5s)
✔ [3577/3592] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (3.2s)
✔ [3581/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (19s)
✔ [3582/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.4s)
✔ [3586/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (61s)
✔ [3589/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMaclaurin:blueprint (5.5s)
✔ [3596/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (14s)
✔ [3599/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.4s)
✔ [3600/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (1.8s)
✔ [3601/3633] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (64s)
✔ [3610/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (3.9s)
✔ [3611/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (3.3s)
✔ [3613/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (2.7s)
✔ [3616/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.6s)
✔ [3618/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.7s)
✔ [3619/3640] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.5s)
✔ [3622/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.5s)
✔ [3623/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.5s)
✔ [3626/3645] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.4s)
✔ [3630/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.4s)
✔ [3634/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.4s)
✔ [3639/3653] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.5s)
✔ [3642/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.5s)
✔ [3647/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.5s)
✔ [3650/3658] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.5s)
✔ [3666/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (1.0s)
✔ [3667/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic:blueprint (2.4s)
✔ [3668/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic:blueprint (1.0s)
✔ [3673/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog:blueprint (1.9s)
✔ [3675/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (34s)
✔ [3676/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (923ms)
✔ [3679/3698] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (1.0s)
✔ [3680/3698] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (5.7s)
ℹ [3681/3698] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3684/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (94s)
✔ [3693/3707] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (5.9s)
✔ [3696/3715] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth:blueprint (2.5s)
✔ [3701/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (3.3s)
✔ [3704/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.8s)
✔ [3707/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (8.2s)
✔ [3712/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (3.5s)
⚠ [3715/3727] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3716/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.6s)
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (60s)
✔ [3721/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3723/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (13s)
✔ [3724/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (3.2s)
✔ [3726/3731] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (3.6s)
⚠ [3850/3857] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3853/3857] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (67s)
✔ [3855/3866] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (21s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3969/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (3.7s)
✔ [3970/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.3s)
✔ [3971/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (3.8s)
✔ [3972/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (5.6s)
✔ [3973/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.3s)
✔ [3977/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.2s)
✔ [3978/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (5.2s)
✔ [3981/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (6.6s)
✔ [3982/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (53s)
✔ [4041/4064] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (3.2s)
✔ [4048/4066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.1s)
✔ [4049/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (121s)
⚠ [4050/4067] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [4051/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [4054/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (32s)
✔ [4057/4069] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (159s)
✔ [4061/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (104s)
⚠ [4062/4070] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [4063/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (14s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (69s)
✔ [4068/4072] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (203s)
✔ [4069/4072] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (235s)
⚠ [4198/4213] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4202/4216] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (180s)
✔ [4203/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (4.8s)
⚠ [4204/4217] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4205/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (97s)
⚠ [4206/4217] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4209/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (251s)
✔ [4210/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (206s)
✔ [4211/4221] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (165s)
⚠ [4213/4268] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4216/4272] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (252s)
✔ [4228/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (213s)
✔ [4231/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (187s)
✔ [4243/4290] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (209s)
✔ [4247/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (210s)
✔ [4248/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (202s)
✔ [4249/4290] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (214s)
✔ [4250/4290] Built LeanCert.Engine.Chebyshev.Psi (34s)
✔ [4251/4290] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (139s)
✔ [4252/4292] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (74s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-558-runtime-blueprint_build-223748-1782166889510705715-2