Run 109

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

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

git checkout 939b653c0dcd61ae9a4d54cea835821be04cb46d

Note: switching to '939b653c0dcd61ae9a4d54cea835821be04cb46d'.

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 939b653 Align some sorry-backed teorems with their original sources (#1628)

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 (385ms)
✔ [2/5] Built Cache.Lean (412ms)
✔ [6/11] Built Cache.Infra (440ms)
✔ [7/12] Built Cache.IO (1.7s)
✔ [9/26] Built Cache.Hashing (887ms)
✔ [10/26] Built Cache.Requests (2.1s)
✔ [11/26] Built Cache.Cli:c.o (1.8s)
✔ [12/26] Built Cache.Lean:c.o (136ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (346ms)
✔ [16/26] Built Cache.Infra:c.o (184ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (654ms)
✔ [19/26] Built Cache.Marker:c.o (102ms)
✔ [20/26] Built Cache.Query (781ms)
✔ [21/26] Built Cache.Query:c.o (241ms)
✔ [22/26] Built Cache.Warning (743ms)
✔ [23/26] Built Cache.Warning:c.o (230ms)
✔ [24/26] Built Cache.Main (1.6s)
✔ [25/26] Built Cache.Main:c.o (762ms)
✔ [26/26] Built cache:exe (7.4s)

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8546 = 0%, 2 KB/s], Decompressed: 12
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 16 KB/s], Decompressed: 31
Downloaded: 64 file(s) [attempted 64/8546 = 0%, 207 KB/s], Decompressed: 56
Downloaded: 84 file(s) [attempted 84/8546 = 0%, 158 KB/s], Decompressed: 74
Downloaded: 112 file(s) [attempted 112/8546 = 1%, 332 KB/s], Decompressed: 94
Downloaded: 146 file(s) [attempted 146/8546 = 1%, 66 KB/s], Decompressed: 129
Downloaded: 180 file(s) [attempted 180/8546 = 2%, 648 KB/s], Decompressed: 167
Downloaded: 217 file(s) [attempted 217/8546 = 2%, 202 KB/s], Decompressed: 190
Downloaded: 258 file(s) [attempted 258/8546 = 3%, 240 KB/s], Decompressed: 234
Downloaded: 290 file(s) [attempted 290/8546 = 3%, 168 KB/s], Decompressed: 258
Downloaded: 322 file(s) [attempted 322/8546 = 3%, 738 KB/s], Decompressed: 278
Downloaded: 363 file(s) [attempted 363/8546 = 4%, 436 KB/s], Decompressed: 326
Downloaded: 400 file(s) [attempted 400/8546 = 4%, 244 KB/s], Decompressed: 373
Downloaded: 441 file(s) [attempted 441/8546 = 5%, 416 KB/s], Decompressed: 417
Downloaded: 475 file(s) [attempted 475/8546 = 5%, 76 KB/s], Decompressed: 441
Downloaded: 512 file(s) [attempted 512/8546 = 5%, 238 KB/s], Decompressed: 461
Downloaded: 556 file(s) [attempted 556/8546 = 6%, 561 KB/s], Decompressed: 492
Downloaded: 590 file(s) [attempted 590/8546 = 6%, 64 KB/s], Decompressed: 536
Downloaded: 630 file(s) [attempted 630/8546 = 7%, 151 KB/s], Decompressed: 580
Downloaded: 671 file(s) [attempted 671/8546 = 7%, 148 KB/s], Decompressed: 634
Downloaded: 701 file(s) [attempted 701/8546 = 8%, 158 KB/s], Decompressed: 654
Downloaded: 729 file(s) [attempted 729/8546 = 8%, 687 KB/s], Decompressed: 705
Downloaded: 773 file(s) [attempted 773/8546 = 9%, 482 KB/s], Decompressed: 725
Downloaded: 820 file(s) [attempted 820/8546 = 9%, 93 KB/s], Decompressed: 776
Downloaded: 867 file(s) [attempted 867/8546 = 10%, 189 KB/s], Decompressed: 837
Downloaded: 911 file(s) [attempted 911/8546 = 10%, 46 KB/s], Decompressed: 867
Downloaded: 959 file(s) [attempted 959/8546 = 11%, 390 KB/s], Decompressed: 911
Downloaded: 1006 file(s) [attempted 1006/8546 = 11%, 134 KB/s], Decompressed: 959
Downloaded: 1050 file(s) [attempted 1050/8546 = 12%, 877 KB/s], Decompressed: 1006
Downloaded: 1094 file(s) [attempted 1094/8546 = 12%, 212 KB/s], Decompressed: 1006
Downloaded: 1121 file(s) [attempted 1121/8546 = 13%, 1816 KB/s], Decompressed: 1050
Downloaded: 1158 file(s) [attempted 1158/8546 = 13%, 243 KB/s], Decompressed: 1098
Downloaded: 1201 file(s) [attempted 1201/8546 = 14%, 113 KB/s], Decompressed: 1148
Downloaded: 1240 file(s) [attempted 1240/8546 = 14%, 88 KB/s], Decompressed: 1148
Downloaded: 1280 file(s) [attempted 1280/8546 = 14%, 264 KB/s], Decompressed: 1199
Downloaded: 1317 file(s) [attempted 1317/8546 = 15%, 451 KB/s], Decompressed: 1250
Downloaded: 1350 file(s) [attempted 1350/8546 = 15%, 502 KB/s], Decompressed: 1300
Downloaded: 1388 file(s) [attempted 1388/8546 = 16%, 350 KB/s], Decompressed: 1300
Downloaded: 1429 file(s) [attempted 1429/8546 = 16%, 1579 KB/s], Decompressed: 1348
Downloaded: 1470 file(s) [attempted 1470/8546 = 17%, 107 KB/s], Decompressed: 1432
Downloaded: 1507 file(s) [attempted 1507/8546 = 17%, 211 KB/s], Decompressed: 1470
Downloaded: 1534 file(s) [attempted 1534/8546 = 17%, 54 KB/s], Decompressed: 1500
Downloaded: 1578 file(s) [attempted 1578/8546 = 18%, 512 KB/s], Decompressed: 1524
Downloaded: 1618 file(s) [attempted 1618/8546 = 18%, 158 KB/s], Decompressed: 1591
Downloaded: 1659 file(s) [attempted 1659/8546 = 19%, 22 KB/s], Decompressed: 1618
Downloaded: 1700 file(s) [attempted 1700/8546 = 19%, 338 KB/s], Decompressed: 1649
Downloaded: 1740 file(s) [attempted 1740/8546 = 20%, 260 KB/s], Decompressed: 1676
Downloaded: 1774 file(s) [attempted 1774/8546 = 20%, 139 KB/s], Decompressed: 1710
Downloaded: 1811 file(s) [attempted 1811/8546 = 21%, 46 KB/s], Decompressed: 1757
Downloaded: 1855 file(s) [attempted 1855/8546 = 21%, 41 KB/s], Decompressed: 1801
Downloaded: 1892 file(s) [attempted 1892/8546 = 22%, 247 KB/s], Decompressed: 1848
Downloaded: 1930 file(s) [attempted 1930/8546 = 22%, 364 KB/s], Decompressed: 1886
Downloaded: 1967 file(s) [attempted 1967/8546 = 23%, 345 KB/s], Decompressed: 1916
Downloaded: 1997 file(s) [attempted 1997/8546 = 23%, 40 KB/s], Decompressed: 1943
Downloaded: 2041 file(s) [attempted 2041/8546 = 23%, 167 KB/s], Decompressed: 1980
Downloaded: 2085 file(s) [attempted 2085/8546 = 24%, 84 KB/s], Decompressed: 1980
Downloaded: 2126 file(s) [attempted 2126/8546 = 24%, 939 KB/s], Decompressed: 2041
Downloaded: 2163 file(s) [attempted 2163/8546 = 25%, 554 KB/s], Decompressed: 2041
Downloaded: 2200 file(s) [attempted 2200/8546 = 25%, 688 KB/s], Decompressed: 2112
Downloaded: 2238 file(s) [attempted 2238/8546 = 26%, 118 KB/s], Decompressed: 2170
Downloaded: 2271 file(s) [attempted 2271/8546 = 26%, 468 KB/s], Decompressed: 2224
Downloaded: 2315 file(s) [attempted 2315/8546 = 27%, 626 KB/s], Decompressed: 2271
Downloaded: 2356 file(s) [attempted 2356/8546 = 27%, 85 KB/s], Decompressed: 2271
Downloaded: 2393 file(s) [attempted 2393/8546 = 28%, 1014 KB/s], Decompressed: 2315
Downloaded: 2430 file(s) [attempted 2430/8546 = 28%, 296 KB/s], Decompressed: 2363
Downloaded: 2464 file(s) [attempted 2464/8546 = 28%, 693 KB/s], Decompressed: 2410
Downloaded: 2501 file(s) [attempted 2501/8546 = 29%, 153 KB/s], Decompressed: 2410
Downloaded: 2539 file(s) [attempted 2539/8546 = 29%, 82 KB/s], Decompressed: 2457
Downloaded: 2579 file(s) [attempted 2579/8546 = 30%, 212 KB/s], Decompressed: 2505
Downloaded: 2620 file(s) [attempted 2620/8546 = 30%, 107 KB/s], Decompressed: 2542
Downloaded: 2654 file(s) [attempted 2654/8546 = 31%, 1189 KB/s], Decompressed: 2583
Downloaded: 2691 file(s) [attempted 2691/8546 = 31%, 163 KB/s], Decompressed: 2623
Downloaded: 2728 file(s) [attempted 2728/8546 = 31%, 114 KB/s], Decompressed: 2671
Downloaded: 2765 file(s) [attempted 2765/8546 = 32%, 134 KB/s], Decompressed: 2718
Downloaded: 2806 file(s) [attempted 2806/8546 = 32%, 670 KB/s], Decompressed: 2758
Downloaded: 2846 file(s) [attempted 2846/8546 = 33%, 190 KB/s], Decompressed: 2789
Downloaded: 2880 file(s) [attempted 2880/8546 = 33%, 268 KB/s], Decompressed: 2819
Downloaded: 2917 file(s) [attempted 2917/8546 = 34%, 857 KB/s], Decompressed: 2887
Downloaded: 2951 file(s) [attempted 2951/8546 = 34%, 632 KB/s], Decompressed: 2917
Downloaded: 2989 file(s) [attempted 2989/8546 = 34%, 121 KB/s], Decompressed: 2948
Downloaded: 3026 file(s) [attempted 3026/8546 = 35%, 41 KB/s], Decompressed: 2982
Downloaded: 3063 file(s) [attempted 3063/8546 = 35%, 458 KB/s], Decompressed: 3016
Downloaded: 3104 file(s) [attempted 3104/8546 = 36%, 447 KB/s], Decompressed: 3049
Downloaded: 3144 file(s) [attempted 3144/8546 = 36%, 34 KB/s], Decompressed: 3083
Downloaded: 3178 file(s) [attempted 3178/8546 = 37%, 248 KB/s], Decompressed: 3120
Downloaded: 3225 file(s) [attempted 3225/8546 = 37%, 156 KB/s], Decompressed: 3158
Downloaded: 3263 file(s) [attempted 3263/8546 = 38%, 1283 KB/s], Decompressed: 3198
Downloaded: 3303 file(s) [attempted 3303/8546 = 38%, 88 KB/s], Decompressed: 3239
Downloaded: 3347 file(s) [attempted 3347/8546 = 39%, 171 KB/s], Decompressed: 3276
Downloaded: 3381 file(s) [attempted 3381/8546 = 39%, 125 KB/s], Decompressed: 3276
Downloaded: 3415 file(s) [attempted 3415/8546 = 39%, 50 KB/s], Decompressed: 3317
Downloaded: 3459 file(s) [attempted 3459/8546 = 40%, 359 KB/s], Decompressed: 3317
Downloaded: 3499 file(s) [attempted 3499/8546 = 40%, 191 KB/s], Decompressed: 3317
Downloaded: 3540 file(s) [attempted 3540/8546 = 41%, 119 KB/s], Decompressed: 3411
Downloaded: 3577 file(s) [attempted 3577/8546 = 41%, 104 KB/s], Decompressed: 3411
Downloaded: 3614 file(s) [attempted 3614/8546 = 42%, 106 KB/s], Decompressed: 3411
Downloaded: 3655 file(s) [attempted 3655/8546 = 42%, 275 KB/s], Decompressed: 3411
Downloaded: 3695 file(s) [attempted 3695/8546 = 43%, 238 KB/s], Decompressed: 3526
Downloaded: 3729 file(s) [attempted 3729/8546 = 43%, 1682 KB/s], Decompressed: 3526
Downloaded: 3767 file(s) [attempted 3767/8546 = 44%, 493 KB/s], Decompressed: 3526
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 284 KB/s], Decompressed: 3665
Downloaded: 3851 file(s) [attempted 3851/8546 = 45%, 57 KB/s], Decompressed: 3665
Downloaded: 3888 file(s) [attempted 3888/8546 = 45%, 203 KB/s], Decompressed: 3665
Downloaded: 3929 file(s) [attempted 3929/8546 = 45%, 137 KB/s], Decompressed: 3790
Downloaded: 3973 file(s) [attempted 3973/8546 = 46%, 69 KB/s], Decompressed: 3790
Downloaded: 4014 file(s) [attempted 4014/8546 = 46%, 167 KB/s], Decompressed: 3902
Downloaded: 4051 file(s) [attempted 4051/8546 = 47%, 39 KB/s], Decompressed: 3902
Downloaded: 4088 file(s) [attempted 4088/8546 = 47%, 126 KB/s], Decompressed: 4000
Downloaded: 4125 file(s) [attempted 4125/8546 = 48%, 220 KB/s], Decompressed: 4000
Downloaded: 4166 file(s) [attempted 4166/8546 = 48%, 134 KB/s], Decompressed: 4081
Downloaded: 4200 file(s) [attempted 4200/8546 = 49%, 56 KB/s], Decompressed: 4081
Downloaded: 4240 file(s) [attempted 4240/8546 = 49%, 197 KB/s], Decompressed: 4149
Downloaded: 4284 file(s) [attempted 4284/8546 = 50%, 91 KB/s], Decompressed: 4149
Downloaded: 4331 file(s) [attempted 4331/8546 = 50%, 288 KB/s], Decompressed: 4220
Downloaded: 4372 file(s) [attempted 4372/8546 = 51%, 63 KB/s], Decompressed: 4288
Downloaded: 4406 file(s) [attempted 4406/8546 = 51%, 781 KB/s], Decompressed: 4288
Downloaded: 4443 file(s) [attempted 4443/8546 = 51%, 459 KB/s], Decompressed: 4359
Downloaded: 4477 file(s) [attempted 4477/8546 = 52%, 169 KB/s], Decompressed: 4359
Downloaded: 4521 file(s) [attempted 4521/8546 = 52%, 442 KB/s], Decompressed: 4426
Downloaded: 4558 file(s) [attempted 4558/8546 = 53%, 305 KB/s], Decompressed: 4490
Downloaded: 4595 file(s) [attempted 4595/8546 = 53%, 278 KB/s], Decompressed: 4490
Downloaded: 4629 file(s) [attempted 4629/8546 = 54%, 558 KB/s], Decompressed: 4558
Downloaded: 4666 file(s) [attempted 4666/8546 = 54%, 152 KB/s], Decompressed: 4558
Downloaded: 4708 file(s) [attempted 4708/8546 = 55%, 1146 KB/s], Decompressed: 4622
Downloaded: 4744 file(s) [attempted 4744/8546 = 55%, 310 KB/s], Decompressed: 4622
Downloaded: 4781 file(s) [attempted 4781/8546 = 55%, 92 KB/s], Decompressed: 4683
Downloaded: 4819 file(s) [attempted 4819/8546 = 56%, 299 KB/s], Decompressed: 4751
Downloaded: 4856 file(s) [attempted 4856/8546 = 56%, 219 KB/s], Decompressed: 4751
Downloaded: 4900 file(s) [attempted 4900/8546 = 57%, 78 KB/s], Decompressed: 4815
Downloaded: 4940 file(s) [attempted 4940/8546 = 57%, 117 KB/s], Decompressed: 4815
Downloaded: 4974 file(s) [attempted 4974/8546 = 58%, 151 KB/s], Decompressed: 4886
Downloaded: 5011 file(s) [attempted 5011/8546 = 58%, 479 KB/s], Decompressed: 4886
Downloaded: 5052 file(s) [attempted 5052/8546 = 59%, 704 KB/s], Decompressed: 4957
Downloaded: 5096 file(s) [attempted 5096/8546 = 59%, 164 KB/s], Decompressed: 4957
Downloaded: 5133 file(s) [attempted 5133/8546 = 60%, 565 KB/s], Decompressed: 5042
Downloaded: 5174 file(s) [attempted 5174/8546 = 60%, 492 KB/s], Decompressed: 5042
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 272 KB/s], Decompressed: 5042
Downloaded: 5245 file(s) [attempted 5245/8546 = 61%, 103 KB/s], Decompressed: 5120
Downloaded: 5292 file(s) [attempted 5292/8546 = 61%, 946 KB/s], Decompressed: 5120
Downloaded: 5336 file(s) [attempted 5336/8546 = 62%, 685 KB/s], Decompressed: 5214
Downloaded: 5377 file(s) [attempted 5377/8546 = 62%, 1855 KB/s], Decompressed: 5214
Downloaded: 5417 file(s) [attempted 5417/8546 = 63%, 441 KB/s], Decompressed: 5319
Downloaded: 5458 file(s) [attempted 5458/8546 = 63%, 60 KB/s], Decompressed: 5319
Downloaded: 5495 file(s) [attempted 5495/8546 = 64%, 242 KB/s], Decompressed: 5319
Downloaded: 5536 file(s) [attempted 5536/8546 = 64%, 52 KB/s], Decompressed: 5417
Downloaded: 5576 file(s) [attempted 5576/8546 = 65%, 418 KB/s], Decompressed: 5417
Downloaded: 5617 file(s) [attempted 5617/8546 = 65%, 79 KB/s], Decompressed: 5514
Downloaded: 5654 file(s) [attempted 5654/8546 = 66%, 174 KB/s], Decompressed: 5514
Downloaded: 5692 file(s) [attempted 5692/8546 = 66%, 547 KB/s], Decompressed: 5603
Downloaded: 5729 file(s) [attempted 5729/8546 = 67%, 578 KB/s], Decompressed: 5603
Downloaded: 5769 file(s) [attempted 5769/8546 = 67%, 491 KB/s], Decompressed: 5681
Downloaded: 5810 file(s) [attempted 5810/8546 = 67%, 454 KB/s], Decompressed: 5681
Downloaded: 5844 file(s) [attempted 5844/8546 = 68%, 264 KB/s], Decompressed: 5762
Downloaded: 5884 file(s) [attempted 5884/8546 = 68%, 314 KB/s], Decompressed: 5762
Downloaded: 5918 file(s) [attempted 5918/8546 = 69%, 74 KB/s], Decompressed: 5840
Downloaded: 5955 file(s) [attempted 5955/8546 = 69%, 724 KB/s], Decompressed: 5840
Downloaded: 6003 file(s) [attempted 6003/8546 = 70%, 1924 KB/s], Decompressed: 5911
Downloaded: 6047 file(s) [attempted 6047/8546 = 70%, 1596 KB/s], Decompressed: 5965
Downloaded: 6094 file(s) [attempted 6094/8546 = 71%, 44 KB/s], Decompressed: 6026
Downloaded: 6131 file(s) [attempted 6131/8546 = 71%, 295 KB/s], Decompressed: 6026
Downloaded: 6162 file(s) [attempted 6162/8546 = 72%, 1105 KB/s], Decompressed: 6091
Downloaded: 6195 file(s) [attempted 6195/8546 = 72%, 147 KB/s], Decompressed: 6141
Downloaded: 6233 file(s) [attempted 6233/8546 = 72%, 687 KB/s], Decompressed: 6141
Downloaded: 6273 file(s) [attempted 6273/8546 = 73%, 40 KB/s], Decompressed: 6195
Downloaded: 6314 file(s) [attempted 6314/8546 = 73%, 319 KB/s], Decompressed: 6195
Downloaded: 6348 file(s) [attempted 6348/8546 = 74%, 71 KB/s], Decompressed: 6256
Downloaded: 6375 file(s) [attempted 6375/8546 = 74%, 338 KB/s], Decompressed: 6317
Downloaded: 6409 file(s) [attempted 6409/8546 = 74%, 57 KB/s], Decompressed: 6317
Downloaded: 6449 file(s) [attempted 6449/8546 = 75%, 822 KB/s], Decompressed: 6368
Downloaded: 6490 file(s) [attempted 6490/8546 = 75%, 785 KB/s], Decompressed: 6419
Downloaded: 6527 file(s) [attempted 6527/8546 = 76%, 311 KB/s], Decompressed: 6419
Downloaded: 6557 file(s) [attempted 6557/8546 = 76%, 31 KB/s], Decompressed: 6486
Downloaded: 6591 file(s) [attempted 6591/8546 = 77%, 521 KB/s], Decompressed: 6486
Downloaded: 6628 file(s) [attempted 6628/8546 = 77%, 126 KB/s], Decompressed: 6547
Downloaded: 6672 file(s) [attempted 6672/8546 = 78%, 726 KB/s], Decompressed: 6608
Downloaded: 6716 file(s) [attempted 6716/8546 = 78%, 288 KB/s], Decompressed: 6608
Downloaded: 6760 file(s) [attempted 6760/8546 = 79%, 396 KB/s], Decompressed: 6672
Downloaded: 6804 file(s) [attempted 6804/8546 = 79%, 904 KB/s], Decompressed: 6723
Downloaded: 6842 file(s) [attempted 6842/8546 = 80%, 112 KB/s], Decompressed: 6767
Downloaded: 6875 file(s) [attempted 6875/8546 = 80%, 233 KB/s], Decompressed: 6811
Downloaded: 6913 file(s) [attempted 6913/8546 = 80%, 215 KB/s], Decompressed: 6857
Downloaded: 6953 file(s) [attempted 6953/8546 = 81%, 69 KB/s], Decompressed: 6902
Downloaded: 6997 file(s) [attempted 6997/8546 = 81%, 49 KB/s], Decompressed: 6902
Downloaded: 7041 file(s) [attempted 7041/8546 = 82%, 274 KB/s], Decompressed: 6950
Downloaded: 7078 file(s) [attempted 7078/8546 = 82%, 1856 KB/s], Decompressed: 7001
Downloaded: 7116 file(s) [attempted 7116/8546 = 83%, 679 KB/s], Decompressed: 7048
Downloaded: 7149 file(s) [attempted 7149/8546 = 83%, 194 KB/s], Decompressed: 7048
Downloaded: 7187 file(s) [attempted 7187/8546 = 84%, 279 KB/s], Decompressed: 7099
Downloaded: 7220 file(s) [attempted 7220/8546 = 84%, 140 KB/s], Decompressed: 7153
Downloaded: 7264 file(s) [attempted 7264/8546 = 84%, 54 KB/s], Decompressed: 7153
Downloaded: 7308 file(s) [attempted 7308/8546 = 85%, 545 KB/s], Decompressed: 7217
Downloaded: 7352 file(s) [attempted 7352/8546 = 86%, 101 KB/s], Decompressed: 7285
Downloaded: 7388 file(s) [attempted 7388/8546 = 86%, 289 KB/s], Decompressed: 7335
Downloaded: 7423 file(s) [attempted 7423/8546 = 86%, 528 KB/s], Decompressed: 7335
Downloaded: 7454 file(s) [attempted 7454/8546 = 87%, 302 KB/s], Decompressed: 7386
Downloaded: 7491 file(s) [attempted 7491/8546 = 87%, 164 KB/s], Decompressed: 7434
Downloaded: 7528 file(s) [attempted 7528/8546 = 88%, 318 KB/s], Decompressed: 7474
Downloaded: 7565 file(s) [attempted 7565/8546 = 88%, 61 KB/s], Decompressed: 7535
Downloaded: 7603 file(s) [attempted 7603/8546 = 88%, 414 KB/s], Decompressed: 7565
Downloaded: 7637 file(s) [attempted 7637/8546 = 89%, 232 KB/s], Decompressed: 7596
Downloaded: 7677 file(s) [attempted 7677/8546 = 89%, 100 KB/s], Decompressed: 7626
Downloaded: 7714 file(s) [attempted 7714/8546 = 90%, 1190 KB/s], Decompressed: 7664
Downloaded: 7755 file(s) [attempted 7755/8546 = 90%, 358 KB/s], Decompressed: 7701
Downloaded: 7792 file(s) [attempted 7792/8546 = 91%, 78 KB/s], Decompressed: 7745
Downloaded: 7829 file(s) [attempted 7829/8546 = 91%, 90 KB/s], Decompressed: 7745
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 19 KB/s], Decompressed: 7789
Downloaded: 7900 file(s) [attempted 7900/8546 = 92%, 229 KB/s], Decompressed: 7833
Downloaded: 7933 file(s) [attempted 7933/8546 = 92%, 284 KB/s], Decompressed: 7873
Downloaded: 7968 file(s) [attempted 7968/8546 = 93%, 819 KB/s], Decompressed: 7904
Downloaded: 8012 file(s) [attempted 8012/8546 = 93%, 657 KB/s], Decompressed: 7944
Downloaded: 8056 file(s) [attempted 8056/8546 = 94%, 383 KB/s], Decompressed: 7988
Downloaded: 8087 file(s) [attempted 8087/8546 = 94%, 151 KB/s], Decompressed: 8036
Downloaded: 8120 file(s) [attempted 8120/8546 = 95%, 471 KB/s], Decompressed: 8036
Downloaded: 8157 file(s) [attempted 8157/8546 = 95%, 793 KB/s], Decompressed: 8087
Downloaded: 8191 file(s) [attempted 8191/8546 = 95%, 126 KB/s], Decompressed: 8137
Downloaded: 8235 file(s) [attempted 8235/8546 = 96%, 65 KB/s], Decompressed: 8137
Downloaded: 8269 file(s) [attempted 8269/8546 = 96%, 265 KB/s], Decompressed: 8191
Downloaded: 8303 file(s) [attempted 8303/8546 = 97%, 445 KB/s], Decompressed: 8191
Downloaded: 8337 file(s) [attempted 8337/8546 = 97%, 79 KB/s], Decompressed: 8252
Downloaded: 8377 file(s) [attempted 8377/8546 = 98%, 259 KB/s], Decompressed: 8306
Downloaded: 8415 file(s) [attempted 8415/8546 = 98%, 269 KB/s], Decompressed: 8364
Downloaded: 8455 file(s) [attempted 8455/8546 = 98%, 786 KB/s], Decompressed: 8364
Downloaded: 8492 file(s) [attempted 8492/8546 = 99%, 829 KB/s], Decompressed: 8415
Downloaded: 8533 file(s) [attempted 8533/8546 = 99%, 214 KB/s], Decompressed: 8469
Downloaded: 8543 file(s) [attempted 8543/8546 = 99%, 265 KB/s], Decompressed: 8530
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 265 KB/s], Decompressed: 8530

lake build

✔ [2071/2078] Built PrimeNumberTheoremAnd.Auxiliary (30s)
✔ [3001/3012] Built PrimeNumberTheoremAnd.Sobolev (19s)
✔ [3021/3026] Built PrimeNumberTheoremAnd.Fourier (3.8s)
✔ [3022/3027] Built Architect.Basic (5.2s)
✔ [3023/3027] Built Architect.Command (775ms)
✔ [3024/3027] Built Architect.CollectUsed (812ms)
✔ [3025/3027] Built Architect.Content (899ms)
✔ [3026/3031] Built Architect.Attribute (1.6s)
✔ [3027/3032] Built Architect.Tactic (1.2s)
✔ [3028/3032] Built Architect.Output (1.8s)
✔ [3030/3033] Built Architect.Load (811ms)
✔ [3031/3040] Built Architect (658ms)
✔ [3059/3072] Built PrimeNumberTheoremAnd.Defs (11s)
✔ [3544/3554] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (1.8s)
✔ [3548/3555] Built PrimeNumberTheoremAnd.Rectangle (3.4s)
✔ [3550/3555] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (1.9s)
✔ [3552/3560] Built PrimeNumberTheoremAnd.ZetaConj (4.1s)
✔ [3554/3561] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (9.6s)
✔ [3558/3567] Built PrimeNumberTheoremAnd.EulerMaclaurin (2.3s)
✔ [3561/3567] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (7.3s)
✔ [3563/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (2.3s)
✔ [3565/3569] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.3s)
✔ [3566/3588] Built PrimeNumberTheoremAnd.ZetaBounds (18s)
✔ [3570/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (1.5s)
✔ [3573/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (1.8s)
✔ [3575/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (2.9s)
✔ [3576/3588] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (1.6s)
✔ [3577/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (2.1s)
✔ [3578/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (1.8s)
✔ [3579/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (1.6s)
✔ [3580/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (2.7s)
✔ [3582/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (2.4s)
✔ [3584/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (3.7s)
✔ [3586/3596] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.4s)
✔ [3588/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.3s)
✔ [3591/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.5s)
✔ [3594/3601] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.1s)
✔ [3596/3608] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (2.5s)
✔ [3610/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (1.7s)
✔ [3611/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (1.6s)
✔ [3613/3631] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (2.2s)
✔ [3615/3631] Built PrimeNumberTheoremAnd.MellinCalculus (7.7s)
✔ [3616/3631] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (860ms)
✔ [3618/3632] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (1.4s)
✔ [3620/3632] Built PrimeNumberTheoremAnd.SmoothExistence (3.4s)
✔ [3622/3633] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (1.7s)
ℹ [3625/3636] Built PrimeNumberTheoremAnd.MediumPNT (28s)
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 (2.1s)
✔ [3634/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (3.0s)
✔ [3636/3639] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (3.6s)
✔ [3637/3648] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (20s)
✔ [3640/3653] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (1.6s)
✔ [3645/3655] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (3.0s)
✔ [3648/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (3.7s)
✔ [3650/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (5.1s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (16s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
✔ [3653/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (2.9s)
✔ [3654/3656] Built PrimeNumberTheoremAnd.BorelCaratheodory (3.8s)
✔ [3655/3658] Built PrimeNumberTheoremAnd.BrunTitchmarsh (3.7s)
✔ [3777/3784] Built LeanCert.Core.Interval (2.1s)
✔ [3779/3784] Built LeanCert.Core.IntervalRat.Basic (4.0s)
✔ [3780/3784] Built LeanCert.Tactic.IntervalAuto.Types (2.9s)
⚠ [3781/3784] Built PrimeNumberTheoremAnd.Wiener (26s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3782/3784] Built LeanCert.Tactic.IntervalAuto.Norm (2.8s)
✔ [3783/3794] Built PrimeNumberTheoremAnd.Consequences (27s)
✔ [3788/3794] Built LeanCert.Core.Expr (3.5s)
✔ [3789/3795] Built LeanCert.Meta.Numeral (2.8s)
✔ [3790/3795] Built LeanCert.Meta.ToExpr (3.5s)
✔ [3791/3795] Built LeanCert.Tactic.IntervalAuto.Extract (2.3s)
✔ [3792/3795] Built LeanCert.Core.Support (2.1s)
✔ [3793/3796] Built LeanCert.Tactic.IntervalAuto.Parse (4.0s)
✔ [3794/3796] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.4s)
✔ [3795/3797] Built LeanCert.Core.IntervalRat.Transcendental (3.1s)
✔ [3796/3811] Built LeanCert.Core.IntervalRat.LogReduction (3.3s)
✔ [3810/3820] Built LeanCert.Core.DerivativeIntervals (2.1s)
✔ [3812/3822] Built LeanCert.Core.TrigReduction (2.5s)
✔ [3813/3822] Built LeanCert.Core.Taylor (4.3s)
✔ [3814/3823] Built LeanCert.Core.IntervalRat.Taylor (8.9s)
✔ [3815/3823] Built LeanCert.Core.IntervalRat.TrigReduced (2.2s)
✔ [3816/3825] Built LeanCert.Core.IntervalReal (1.9s)
✔ [3817/3826] Built LeanCert.Core.IntervalRealEndpoints (2.8s)
✔ [3818/3826] Built LeanCert.Engine.Eval.Core (4.4s)
✔ [3819/3828] Built LeanCert.Engine.Eval.Extended (2.9s)
✔ [3820/3833] Built LeanCert.Tactic.Bound.Lemmas (2.1s)
✔ [3821/3833] Built LeanCert.Contrib.Sinc (2.9s)
✔ [3822/3833] Built LeanCert.Engine.IntervalEval (1.9s)
✔ [3823/3833] Built LeanCert.Engine.AD.Basic (2.0s)
✔ [3824/3833] Built LeanCert.Engine.AD.Transcendental (3.2s)
✔ [3825/3833] Built LeanCert.Engine.AD.Eval (2.1s)
✔ [3826/3833] Built LeanCert.Engine.AD.Correctness (2.7s)
✔ [3827/3833] Built LeanCert.Engine.AD.Computable (2.6s)
✔ [3828/3834] Built LeanCert.Engine.AD.PartialCorrectness (4.5s)
✔ [3829/3834] Built LeanCert.Engine.AD (1.9s)
✔ [3830/3834] Built LeanCert.Engine.TaylorModel.Core (4.9s)
✔ [3831/3834] Built LeanCert.Meta.ProveSupported (2.0s)
✔ [3832/3836] Built LeanCert.Tactic.IntervalAuto.ProveCommon (3.0s)
✔ [3833/3837] Built LeanCert.Tactic.IntervalAuto.Basic (2.2s)
✔ [3835/3837] Built LeanCert.Engine.TaylorModel.ExpLog (4.7s)
✔ [3836/3849] Built LeanCert.Engine.TaylorModel.Trig (6.1s)
✔ [3845/3853] Built LeanCert.Engine.TaylorModel.Special (2.1s)
✔ [3846/3853] Built LeanCert.Engine.Integrate (3.7s)
✔ [3847/3853] Built LeanCert.Engine.TaylorModel.Hyperbolic (6.8s)
✔ [3848/3856] Built LeanCert.Engine.TaylorModel.Integral (2.6s)
✔ [3849/3856] Built LeanCert.Engine.TaylorModel.Functions (1.9s)
✔ [3850/3856] Built LeanCert.Core.Dyadic (1.9s)
✔ [3851/3856] Built LeanCert.Engine.TaylorModel.Expr (3.3s)
✔ [3852/3856] Built LeanCert.Core.IntervalDyadic (4.8s)
✔ [3853/3860] Built LeanCert.Engine.TaylorModel (1.9s)
✔ [3854/3860] Built LeanCert.Engine.IntervalEvalDyadic (3.1s)
✔ [3855/3861] Built LeanCert.Engine.IntervalEvalRefined (2.8s)
✔ [3856/3861] Built LeanCert.Engine.Affine.Basic (3.0s)
✔ [3857/3861] Built LeanCert.Engine.Optimization.Box (2.2s)
✔ [3858/3864] Built LeanCert.Engine.Affine.Nonlinear (3.4s)
✔ [3859/3864] Built LeanCert.Engine.Affine.Transcendental (2.9s)
✔ [3860/3864] Built LeanCert.Engine.Optimize (3.8s)
✔ [3861/3865] Built LeanCert.Engine.IntervalEvalAffine (3.0s)
✔ [3862/3866] Built LeanCert.Engine.Optimization.Gradient (3.5s)
✔ [3863/3866] Built LeanCert.Engine.RootFinding.Basic (3.2s)
✔ [3864/3867] Built LeanCert.Engine.Optimization.Global (9.0s)
✔ [3865/3868] Built LeanCert.Engine.RootFinding.Bisection (3.3s)
✔ [3866/3870] Built LeanCert.Engine.RootFinding.Newton (3.1s)
✔ [3867/3871] Built LeanCert.Engine.RootFinding.MVTBounds (4.1s)
✔ [3868/3871] Built LeanCert.Engine.RootFinding.Contraction (3.6s)
✔ [3869/3871] Built LeanCert.Meta.ProveContinuous (3.2s)
✔ [3870/3873] Built LeanCert.Engine.RootFinding.Main (1.9s)
✔ [3871/3874] Built LeanCert.Validity.Bounds.Core (2.2s)
✔ [3872/3876] Built LeanCert.Validity.Bounds.WithInv (2.2s)
✔ [3873/3878] Built LeanCert.Validity.Bounds.Smart (2.4s)
✔ [3874/3879] Built LeanCert.Validity.Bounds.Bridge (2.3s)
✔ [3875/3879] Built LeanCert.Validity.Integration (3.4s)
✔ [3876/3881] Built LeanCert.Validity.Bounds.Basic (1.9s)
✔ [3877/3881] Built LeanCert.Validity.DyadicBounds (2.3s)
✔ [3878/3882] Built LeanCert.Validity.Bounds (4.5s)
✔ [3879/3883] Built LeanCert.Engine.Optimization.BoundVerify (2.4s)
✔ [3880/3883] Built LeanCert.Tactic.IntervalAuto.Multivariate (3.9s)
✔ [3881/3884] Built LeanCert.Tactic.IntervalAuto.Bound (21s)
✔ [3882/3885] Built LeanCert.Tactic.IntervalAuto.OptBound (2.7s)
✔ [3883/3886] Built LeanCert.Tactic.IntervalAuto.RootBound (2.8s)
✔ [3884/3889] Built LeanCert.Tactic.IntervalAuto.PointIneq (11s)
✔ [3885/3896] Built LeanCert.Tactic.IntervalAuto.Subdiv (5.9s)
✔ [3886/3899] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.1s)
✔ [3888/3899] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.4s)
✔ [3889/3899] Built PrimeNumberTheoremAnd.HadamardFactorization (1.2s)
✔ [3890/3899] Built PrimeNumberTheoremAnd.HoffsteinLockhart (2.4s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (3.2s)
⚠ [3892/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (2.8s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3893/3900] Built LeanCert.Tactic.IntervalAuto (2.7s)
✔ [3895/3900] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (1.7s)
✔ [3896/3901] Built PrimeNumberTheoremAnd.IEANTN.LogTables (27s)
✔ [3898/3901] Built PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
✔ [3899/3906] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (8.8s)
✔ [3957/3972] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.7s)
✔ [3959/3972] Built LeanCert.Engine.TaylorModel.Log1p (4.1s)
✔ [3961/3972] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (5.8s)
✔ [3962/3972] Built LeanCert.Examples.Li2Base (2.7s)
✔ [3963/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (47s)
✔ [3964/3974] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (18s)
⚠ [3965/3974] Built LeanCert.Examples.Li2Bounds (2.4s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3966/3975] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (2.9s)
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 (7.0s)
✔ [3969/3976] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.2s)
✔ [3970/3977] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.7s)
✔ [3974/3978] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (5.8s)
⚠ [3975/3982] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.6s)
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`
⚠ [4106/4114] Built PrimeNumberTheoremAnd.IEANTN.Buthe (11s)
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 (41s)
✔ [4109/4114] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (2.1s)
⚠ [4110/4114] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (14s)
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/4114] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (81s)
⚠ [4112/4117] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4113/4118] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4114/4118] Built LeanCert.Engine.FinSumDyadic (2.6s)
✔ [4115/4118] Built LeanCert.Examples.BKLNW_a2_base (4.4s)
✔ [4116/4122] Built LeanCert.Engine.WitnessSum (2.3s)
✔ [4117/4146] Built LeanCert.Engine.ReflectiveSum (3.8s)
✔ [4118/4147] Built LeanCert.Tactic.VecUtil (2.1s)
✔ [4119/4147] Built LeanCert.Tactic.FinSumExpand (1.4s)
✔ [4121/4149] Built LeanCert.Examples.BKLNW_a2_reflective (92s)
✔ [4122/4149] Built LeanCert.Examples.BKLNW_a2_bounds (2.8s)
✔ [4123/4150] Built LeanCert.Examples.BKLNW_a2_pow2 (2.6s)
✔ [4125/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (4.7s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.9s)
✔ [4131/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4132/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (10s)
✔ [4133/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (61s)
✔ [4134/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (33s)
✔ [4135/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (33s)
✔ [4136/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (33s)
✔ [4137/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (34s)
✔ [4138/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (34s)
✔ [4139/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (33s)
✔ [4140/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (34s)
✔ [4141/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (34s)
✔ [4142/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (35s)
✔ [4143/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (34s)
✔ [4144/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (33s)
✔ [4145/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.5s)
✔ [4146/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.6s)
✔ [4147/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (19s)
✔ [4148/4161] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (45s)
✔ [4149/4161] Built LeanCert.Engine.Chebyshev.Psi (2.6s)
✔ [4150/4161] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.9s)
✔ [4151/4161] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (2.6s)
✔ [4152/4163] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (58s)
⚠ [4153/4165] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (12s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4154/4165] Built LeanCert.Engine.ChebyshevPsi (1.9s)
⚠ [4155/4165] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
✔ [4156/4165] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (38s)
✔ [4159/4165] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (18s)
⚠ [4160/4165] Built PrimeNumberTheoremAnd.IEANTN.Dusart (17s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
✔ [4161/4170] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (3.9s)
✔ [4163/4170] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (18s)
✔ [4164/4170] Built LeanCert.Engine.Chebyshev.Theta (4.8s)
✔ [4165/4170] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (45s)
✔ [4167/4170] Built LeanCert.Engine.ChebyshevTheta (1.0s)
ℹ [4168/4170] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (18s)
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4169/4175] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (54s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
✔ [4170/4176] Built LeanCert.Cert.Interval (2.4s)
✔ [4171/4177] Built LeanCert.ANT.Step (2.6s)
✔ [4172/4178] Built LeanCert.ANT.Abel (2.7s)
✔ [4173/4178] Built LeanCert.ANT.Asymp.Env (2.0s)
✔ [4174/4178] Built LeanCert.ANT.Asymp.Hyperbola (2.6s)
✔ [4175/4197] Built LeanCert.ANT.Asymp.Stieltjes (2.6s)
✔ [4176/4197] Built LeanCert.ANT.Asymp.Pointwise (2.6s)
✔ [4177/4197] Built LeanCert.ANT.Asymp.Checkers (2.5s)
✔ [4178/4202] Built LeanCert.Engine.Table (565ms)
✔ [4179/4202] Built LeanCert.ANT.Asymp.Inequality (2.4s)
✔ [4180/4202] Built LeanCert.Validity.AffineBounds (2.7s)
✔ [4181/4202] Built PrimeNumberTheoremAnd.Tactic.Simprocs (1.5s)
✔ [4183/4202] Built LeanCert.ANT.Asymp (2.2s)
✔ [4184/4202] Built LeanCert.Validity.AffineCover (2.1s)
✔ [4185/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (17s)
✔ [4186/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4187/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (22s)
✔ [4188/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (22s)
✔ [4189/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (22s)
✔ [4190/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (22s)
✔ [4191/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (22s)
✔ [4192/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (22s)
✔ [4193/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (22s)
✔ [4194/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (22s)
✔ [4195/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (22s)
✔ [4196/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (22s)
✔ [4197/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (22s)
✔ [4198/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4199/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (22s)
✔ [4200/4205] Built PrimeCert.Interval (2.5s)
✔ [4201/4205] Built PrimeCert.Meta.PrimeCert (2.2s)
⚠ [4202/4205] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (4.0s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4203/4206] Built PrimeCert.Meta.SmallPrime (1.3s)
⚠ [4204/4207] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (6.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4205/4208] Built PrimeCert.PredMod (417ms)
✔ [4206/4210] Built PrimeCert.PowMod (1.5s)
✔ [4209/4221] Built PrimeCert.Pocklington (2.6s)
✔ [4211/4221] Built PrimeCert.SmallPrimes (2.1s)
✔ [4212/4223] Built PrimeCert.Pocklington3 (4.4s)
✔ [4213/4223] Built PrimeCert.Wieferich (2.2s)
✔ [4214/4226] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (11s)
✔ [4216/4226] Built PrimeCert (1.7s)
✔ [4218/4226] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax (2.2s)
✔ [4219/4226] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (6.3s)
✔ [4220/4260] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (6.1s)
✔ [4221/4260] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (3.3s)
✔ [4222/4262] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.1s)
✔ [4224/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound (1.4s)
✔ [4225/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory (2.1s)
✔ [4226/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (1.7s)
✔ [4227/4262] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation (1.6s)
✔ [4228/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic (1.5s)
✔ [4229/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric (1.4s)
✔ [4230/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds (1.7s)
✔ [4231/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds (3.1s)
✔ [4232/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux (1.8s)
✔ [4233/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (1.7s)
✔ [4234/4262] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta (2.3s)
✔ [4235/4262] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex (2.8s)
✔ [4236/4262] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn (1.5s)
✔ [4237/4262] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring (1.3s)
✔ [4238/4262] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (1.6s)
✔ [4239/4262] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (1.8s)
⚠ [4240/4277] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
✔ [4243/4277] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly (7.5s)
✔ [4244/4277] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi (1.7s)
✔ [4245/4277] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds (5.1s)
✔ [4246/4277] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (1.9s)
⚠ [4247/4277] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4249/4277] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (16s)
✔ [4250/4277] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy (1.3s)
✔ [4251/4277] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (2.6s)
⚠ [4252/4277] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (5.2s)
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4254/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (2.1s)
✔ [4256/4284] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
✔ [4257/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth (3.6s)
✔ [4258/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel (2.9s)
✔ [4259/4284] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
⚠ [4260/4284] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.5s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4261/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues (2.2s)
✔ [4262/4284] Built PrimeNumberTheoremAnd.LaplaceInversion (9.6s)
✔ [4263/4284] Built PrimeNumberTheoremAnd.IEANTN.Lcm (29s)
✔ [4265/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral (1.6s)
✔ [4266/4284] Built PrimeNumberTheoremAnd.PerronFormula (6.8s)
✔ [4267/4284] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
✔ [4268/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound (4.9s)
✔ [4269/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum (2.6s)
✔ [4271/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound (10s)
✔ [4272/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound (2.5s)
✔ [4273/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation (2.6s)
✔ [4274/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition (1.5s)
✔ [4275/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth (4.6s)
✔ [4276/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity (2.4s)
✔ [4277/4284] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order (2.2s)
✔ [4278/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound (1.7s)
✔ [4279/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder (13s)
✔ [4280/4284] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard (3.1s)
✔ [4281/4284] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (4.5s)
⚠ [4282/4284] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4283/4284] Built PrimeNumberTheoremAnd (3.8s)
Build completed successfully (4284 jobs).

lake build :blueprint

✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (2.5s)
✔ [17/35] Built Architect.Basic:c.o (979ms)
✔ [18/35] Built Architect.Command:c.o (287ms)
✔ [19/35] Built Architect.Content:c.o (221ms)
✔ [20/35] Built Architect.Attribute:c.o (946ms)
✔ [21/35] Built Architect.CollectUsed:c.o (160ms)
✔ [22/35] Built Architect.Tactic:c.o (833ms)
✔ [23/35] Built Architect.Output:c.o (2.2s)
✔ [24/35] Built Architect.Load:c.o (167ms)
✔ [25/35] Built Architect:c.o (69ms)
✔ [27/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (497ms)
✔ [31/35] Built Cli:c.o (93ms)
✔ [32/35] Built Main (1.6s)
✔ [33/35] Built Main:c.o (261ms)
✔ [34/35] Built extract_blueprint:exe (9.0s)
✔ [2103/2110] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (2.3s)
✔ [3034/3043] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.6s)
✔ [3055/3064] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.6s)
✔ [3084/3097] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (11s)
✔ [3574/3584] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (2.0s)
✔ [3575/3584] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.5s)
✔ [3581/3594] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (15s)
✔ [3582/3594] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.3s)
✔ [3586/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (11s)
✔ [3589/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMaclaurin:blueprint (2.5s)
✔ [3596/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (13s)
✔ [3598/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.4s)
✔ [3599/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (1.7s)
✔ [3602/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (63s)
✔ [3610/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (1.0s)
✔ [3611/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.3s)
✔ [3614/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (2.6s)
✔ [3616/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.5s)
✔ [3617/3640] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.5s)
✔ [3619/3640] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.5s)
✔ [3623/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.5s)
✔ [3624/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.6s)
✔ [3627/3646] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.5s)
✔ [3630/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.5s)
✔ [3635/3651] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.5s)
✔ [3639/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.5s)
✔ [3643/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.6s)
✔ [3648/3656] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.6s)
✔ [3651/3658] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.4s)
✔ [3666/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (1.9s)
✔ [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 (23s)
✔ [3676/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (967ms)
✔ [3680/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (1.0s)
✔ [3681/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (4.6s)
ℹ [3682/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3686/3701] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (58s)
✔ [3693/3712] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (2.6s)
✔ [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 (2.5s)
✔ [3704/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.7s)
✔ [3707/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.2s)
✔ [3712/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.4s)
⚠ [3715/3727] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
✔ [3716/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.4s)
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (58s)
✔ [3721/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3723/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.9s)
✔ [3724/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (2.3s)
✔ [3726/3731] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.6s)
⚠ [3848/3857] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3851/3857] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (37s)
✔ [3854/3868] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (14s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3967/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (3.0s)
✔ [3968/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.3s)
✔ [3969/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (2.0s)
✔ [3970/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (3.1s)
✔ [3971/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.3s)
✔ [3976/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (4.0s)
✔ [3979/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.0s)
✔ [3981/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.8s)
✔ [3982/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (45s)
✔ [4038/4050] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.8s)
⚠ [4047/4066] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [4049/4066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.1s)
✔ [4050/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [4051/4068] 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`
✔ [4053/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.4s)
✔ [4057/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.7s)
✔ [4059/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.3s)
✔ [4060/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.9s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.2s)
⚠ [4065/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`
✔ [4068/4078] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [4069/4078] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.8s)
⚠ [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 (6.6s)
✔ [4203/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (2.4s)
⚠ [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 (5.3s)
⚠ [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/4224] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (21s)
✔ [4210/4224] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4211/4224] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.0s)
⚠ [4212/4224] 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`
✔ [4215/4273] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4228/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.4s)
✔ [4231/4292] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.6s)
✔ [4253/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.5s)
✔ [4254/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.7s)
✔ [4255/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.5s)
✔ [4256/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.5s)
✔ [4257/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.7s)
✔ [4258/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (4.1s)
✔ [4259/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.7s)
✔ [4260/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.7s)
✔ [4261/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.7s)
✔ [4262/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.6s)
✔ [4263/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.6s)
✔ [4264/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.7s)
✔ [4265/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.7s)
✔ [4266/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.7s)
✔ [4267/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.6s)
✔ [4268/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.7s)
✔ [4269/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.5s)
✔ [4270/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4271/4295] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4273/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.9s)
✔ [4274/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.9s)
⚠ [4275/4295] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
✔ [4279/4299] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (20s)
✔ [4281/4299] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (4.0s)
⚠ [4282/4299] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
✔ [4283/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (6.4s)
✔ [4287/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4288/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4289/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.5s)
✔ [4294/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.7s)
✔ [4296/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
ℹ [4297/4306] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4298/4308] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (12s)
✔ [4299/4308] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.1s)
⚠ [4300/4308] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
✔ [4302/4352] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (33s)
✔ [4318/4354] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.3s)
✔ [4319/4355] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.5s)
✔ [4336/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.4s)
✔ [4337/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.4s)
✔ [4338/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.6s)
✔ [4339/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.5s)
✔ [4340/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.4s)
✔ [4341/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.4s)
✔ [4342/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.4s)
✔ [4343/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.5s)
✔ [4344/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.5s)
✔ [4345/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.4s)
✔ [4346/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.5s)
✔ [4347/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.5s)
✔ [4348/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.5s)
✔ [4349/4357] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.6s)
⚠ [4350/4357] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4352/4360] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.4s)
⚠ [4353/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4356/4380] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.9s)
✔ [4367/4385] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.6s)
✔ [4372/4453] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.1s)
✔ [4374/4453] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers:blueprint (3.2s)
✔ [4376/4453] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax:blueprint (2.4s)
✔ [4394/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (3.2s)
✔ [4395/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.7s)
⚠ [4396/4482] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
✔ [4398/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound:blueprint (2.1s)
✔ [4399/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory:blueprint (2.5s)
✔ [4401/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.1s)
✔ [4402/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation:blueprint (2.6s)
✔ [4405/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic:blueprint (1.9s)
✔ [4406/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric:blueprint (1.7s)
✔ [4407/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds:blueprint (2.4s)
✔ [4408/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds:blueprint (2.3s)
✔ [4409/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux:blueprint (2.3s)
✔ [4411/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (1.7s)
✔ [4412/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta:blueprint (2.5s)
✔ [4413/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex:blueprint (1.7s)
✔ [4414/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn:blueprint (2.1s)
✔ [4416/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring:blueprint (1.2s)
✔ [4417/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic:blueprint (2.1s)
✔ [4418/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.3s)
⚠ [4423/4492] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4426/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (46s)
⚠ [4427/4493] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4429/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly:blueprint (2.3s)
✔ [4431/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi:blueprint (2.4s)
✔ [4432/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds:blueprint (2.3s)
✔ [4433/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals:blueprint (2.2s)
✔ [4436/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (2.2s)
✔ [4437/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy:blueprint (1.4s)
✔ [4439/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.2s)
✔ [4440/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (43s)
✔ [4441/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (2.1s)
✔ [4445/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4447/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.1s)
⚠ [4448/4493] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4450/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth:blueprint (2.3s)
✔ [4451/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel:blueprint (2.6s)
✔ [4455/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues:blueprint (2.5s)
✔ [4456/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.4s)
✔ [4458/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral:blueprint (2.1s)
✔ [4459/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4460/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.2s)
✔ [4461/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound:blueprint (2.3s)
✔ [4464/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum:blueprint (2.6s)
✔ [4466/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4467/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.3s)
✔ [4468/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4470/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound:blueprint (2.2s)
✔ [4471/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound:blueprint (2.2s)
✔ [4473/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation:blueprint (2.6s)
✔ [4475/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition:blueprint (1.9s)
✔ [4476/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth:blueprint (2.3s)
✔ [4478/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity:blueprint (2.6s)
✔ [4480/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order:blueprint (2.3s)
✔ [4481/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound:blueprint (2.7s)
✔ [4483/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder:blueprint (2.8s)
✔ [4485/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard:blueprint (2.7s)
✔ [4487/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (3.9s)
⚠ [4488/4493] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4489/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (44s)
✔ [4491/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (4.0s)
ℹ [4492/4494] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (119ms)
info: Blueprint indexing
Build completed successfully (4494 jobs).

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":5,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":501225,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":5,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":677,"diagnostic_count":487,"duration_ms":71275,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":478768,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":677,"diagnostic_count":487,"duration_ms":65,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3907142,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3907142,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2162,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":494683,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":168548,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":168548,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":5301,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":480346,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":7,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":396654,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":396654,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":19101,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":479027,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":21,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1486947,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1486947,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":24429,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":483433,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":12,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1805467,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1805467,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":4929,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":480025,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":255256,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":255256,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":264,"diagnostic_count":135,"duration_ms":23736,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":483264,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":264,"diagnostic_count":135,"duration_ms":10,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":7,"module_payload_kind":"fragment","ok":true,"payload_bytes":1281745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":7,"module_payload_kind":"fragment","ok":true,"payload_bytes":1281745,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":9199}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11545,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":10736,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6256feeb54a2efea416755a232293ffbbfbf2fbb386d2033fd8cd4ef4f9dc046
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":4037210,"ok":true}