Run 132

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

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

git checkout 89de9d582380041e04812bf5d64fb37a1c5eb560

Note: switching to '89de9d582380041e04812bf5d64fb37a1c5eb560'.

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 89de9d5 Fix BKLNW Table 11 typo (#1633)

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)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8546 = 0%, 5 KB/s], Decompressed: 11
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 15 KB/s], Decompressed: 38
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 159 KB/s], Decompressed: 64
Downloaded: 95 file(s) [attempted 95/8546 = 1%, 329 KB/s], Decompressed: 88
Downloaded: 122 file(s) [attempted 122/8546 = 1%, 143 KB/s], Decompressed: 119
Downloaded: 156 file(s) [attempted 156/8546 = 1%, 345 KB/s], Decompressed: 149
Downloaded: 194 file(s) [attempted 194/8546 = 2%, 552 KB/s], Decompressed: 193
Downloaded: 227 file(s) [attempted 227/8546 = 2%, 519 KB/s], Decompressed: 221
Downloaded: 265 file(s) [attempted 265/8546 = 3%, 114 KB/s], Decompressed: 258
Downloaded: 305 file(s) [attempted 305/8546 = 3%, 712 KB/s], Decompressed: 302
Downloaded: 349 file(s) [attempted 349/8546 = 4%, 95 KB/s], Decompressed: 346
Downloaded: 393 file(s) [attempted 393/8546 = 4%, 137 KB/s], Decompressed: 390
Downloaded: 437 file(s) [attempted 437/8546 = 5%, 592 KB/s], Decompressed: 431
Downloaded: 471 file(s) [attempted 471/8546 = 5%, 1114 KB/s], Decompressed: 464
Downloaded: 508 file(s) [attempted 508/8546 = 5%, 174 KB/s], Decompressed: 505
Downloaded: 552 file(s) [attempted 552/8546 = 6%, 343 KB/s], Decompressed: 546
Downloaded: 590 file(s) [attempted 590/8546 = 6%, 70 KB/s], Decompressed: 580
Downloaded: 630 file(s) [attempted 630/8546 = 7%, 77 KB/s], Decompressed: 627
Downloaded: 668 file(s) [attempted 668/8546 = 7%, 339 KB/s], Decompressed: 664
Downloaded: 708 file(s) [attempted 708/8546 = 8%, 66 KB/s], Decompressed: 701
Downloaded: 749 file(s) [attempted 749/8546 = 8%, 284 KB/s], Decompressed: 745
Downloaded: 788 file(s) [attempted 788/8546 = 9%, 123 KB/s], Decompressed: 779
Downloaded: 823 file(s) [attempted 823/8546 = 9%, 81 KB/s], Decompressed: 813
Downloaded: 867 file(s) [attempted 867/8546 = 10%, 124 KB/s], Decompressed: 861
Downloaded: 911 file(s) [attempted 911/8546 = 10%, 67 KB/s], Decompressed: 905
Downloaded: 955 file(s) [attempted 955/8546 = 11%, 166 KB/s], Decompressed: 949
Downloaded: 993 file(s) [attempted 993/8546 = 11%, 497 KB/s], Decompressed: 976
Downloaded: 1026 file(s) [attempted 1026/8546 = 12%, 209 KB/s], Decompressed: 1020
Downloaded: 1071 file(s) [attempted 1071/8546 = 12%, 102 KB/s], Decompressed: 1067
Downloaded: 1114 file(s) [attempted 1114/8546 = 13%, 243 KB/s], Decompressed: 1108
Downloaded: 1155 file(s) [attempted 1155/8546 = 13%, 66 KB/s], Decompressed: 1148
Downloaded: 1192 file(s) [attempted 1192/8546 = 13%, 605 KB/s], Decompressed: 1185
Downloaded: 1233 file(s) [attempted 1233/8546 = 14%, 98 KB/s], Decompressed: 1229
Downloaded: 1277 file(s) [attempted 1277/8546 = 14%, 695 KB/s], Decompressed: 1273
Downloaded: 1317 file(s) [attempted 1317/8546 = 15%, 192 KB/s], Decompressed: 1311
Downloaded: 1358 file(s) [attempted 1358/8546 = 15%, 177 KB/s], Decompressed: 1351
Downloaded: 1399 file(s) [attempted 1399/8546 = 16%, 393 KB/s], Decompressed: 1393
Downloaded: 1436 file(s) [attempted 1436/8546 = 16%, 183 KB/s], Decompressed: 1426
Downloaded: 1473 file(s) [attempted 1473/8546 = 17%, 43 KB/s], Decompressed: 1470
Downloaded: 1517 file(s) [attempted 1517/8546 = 17%, 162 KB/s], Decompressed: 1514
Downloaded: 1554 file(s) [attempted 1554/8546 = 18%, 421 KB/s], Decompressed: 1551
Downloaded: 1598 file(s) [attempted 1598/8546 = 18%, 987 KB/s], Decompressed: 1591
Downloaded: 1639 file(s) [attempted 1639/8546 = 19%, 83 KB/s], Decompressed: 1635
Downloaded: 1676 file(s) [attempted 1676/8546 = 19%, 154 KB/s], Decompressed: 1673
Downloaded: 1713 file(s) [attempted 1713/8546 = 20%, 114 KB/s], Decompressed: 1706
Downloaded: 1757 file(s) [attempted 1757/8546 = 20%, 26 KB/s], Decompressed: 1754
Downloaded: 1804 file(s) [attempted 1804/8546 = 21%, 785 KB/s], Decompressed: 1801
Downloaded: 1845 file(s) [attempted 1845/8546 = 21%, 1073 KB/s], Decompressed: 1842
Downloaded: 1882 file(s) [attempted 1882/8546 = 22%, 285 KB/s], Decompressed: 1876
Downloaded: 1918 file(s) [attempted 1918/8546 = 22%, 732 KB/s], Decompressed: 1909
Downloaded: 1953 file(s) [attempted 1953/8546 = 22%, 1402 KB/s], Decompressed: 1950
Downloaded: 1997 file(s) [attempted 1997/8546 = 23%, 477 KB/s], Decompressed: 1994
Downloaded: 2045 file(s) [attempted 2045/8546 = 23%, 520 KB/s], Decompressed: 2038
Downloaded: 2082 file(s) [attempted 2082/8546 = 24%, 333 KB/s], Decompressed: 2079
Downloaded: 2119 file(s) [attempted 2119/8546 = 24%, 303 KB/s], Decompressed: 2116
Downloaded: 2161 file(s) [attempted 2161/8546 = 25%, 312 KB/s], Decompressed: 2150
Downloaded: 2197 file(s) [attempted 2197/8546 = 25%, 467 KB/s], Decompressed: 2190
Downloaded: 2241 file(s) [attempted 2241/8546 = 26%, 372 KB/s], Decompressed: 2234
Downloaded: 2277 file(s) [attempted 2277/8546 = 26%, 48 KB/s], Decompressed: 2268
Downloaded: 2315 file(s) [attempted 2315/8546 = 27%, 129 KB/s], Decompressed: 2309
Downloaded: 2359 file(s) [attempted 2359/8546 = 27%, 48 KB/s], Decompressed: 2356
Downloaded: 2403 file(s) [attempted 2403/8546 = 28%, 100 KB/s], Decompressed: 2393
Downloaded: 2440 file(s) [attempted 2440/8546 = 28%, 317 KB/s], Decompressed: 2437
Downloaded: 2481 file(s) [attempted 2481/8546 = 29%, 174 KB/s], Decompressed: 2474
Downloaded: 2518 file(s) [attempted 2518/8546 = 29%, 122 KB/s], Decompressed: 2511
Downloaded: 2562 file(s) [attempted 2562/8546 = 29%, 334 KB/s], Decompressed: 2555
Downloaded: 2606 file(s) [attempted 2606/8546 = 30%, 62 KB/s], Decompressed: 2599
Downloaded: 2643 file(s) [attempted 2643/8546 = 30%, 166 KB/s], Decompressed: 2633
Downloaded: 2683 file(s) [attempted 2683/8546 = 31%, 1748 KB/s], Decompressed: 2677
Downloaded: 2722 file(s) [attempted 2722/8546 = 31%, 35 KB/s], Decompressed: 2718
Downloaded: 2765 file(s) [attempted 2765/8546 = 32%, 101 KB/s], Decompressed: 2758
Downloaded: 2802 file(s) [attempted 2802/8546 = 32%, 287 KB/s], Decompressed: 2792
Downloaded: 2836 file(s) [attempted 2836/8546 = 33%, 103 KB/s], Decompressed: 2833
Downloaded: 2880 file(s) [attempted 2880/8546 = 33%, 186 KB/s], Decompressed: 2870
Downloaded: 2914 file(s) [attempted 2914/8546 = 34%, 311 KB/s], Decompressed: 2907
Downloaded: 2958 file(s) [attempted 2958/8546 = 34%, 718 KB/s], Decompressed: 2951
Downloaded: 2999 file(s) [attempted 2999/8546 = 35%, 278 KB/s], Decompressed: 2995
Downloaded: 3036 file(s) [attempted 3036/8546 = 35%, 1213 KB/s], Decompressed: 3032
Downloaded: 3076 file(s) [attempted 3076/8546 = 35%, 394 KB/s], Decompressed: 3071
Downloaded: 3113 file(s) [attempted 3113/8546 = 36%, 582 KB/s], Decompressed: 3107
Downloaded: 3154 file(s) [attempted 3154/8546 = 36%, 103 KB/s], Decompressed: 3150
Downloaded: 3195 file(s) [attempted 3195/8546 = 37%, 71 KB/s], Decompressed: 3178
Downloaded: 3235 file(s) [attempted 3235/8546 = 37%, 502 KB/s], Decompressed: 3225
Downloaded: 3273 file(s) [attempted 3273/8546 = 38%, 227 KB/s], Decompressed: 3266
Downloaded: 3313 file(s) [attempted 3313/8546 = 38%, 189 KB/s], Decompressed: 3306
Downloaded: 3350 file(s) [attempted 3350/8546 = 39%, 216 KB/s], Decompressed: 3344
Downloaded: 3394 file(s) [attempted 3394/8546 = 39%, 123 KB/s], Decompressed: 3391
Downloaded: 3438 file(s) [attempted 3438/8546 = 40%, 1003 KB/s], Decompressed: 3432
Downloaded: 3480 file(s) [attempted 3480/8546 = 40%, 183 KB/s], Decompressed: 3476
Downloaded: 3516 file(s) [attempted 3516/8546 = 41%, 1051 KB/s], Decompressed: 3513
Downloaded: 3553 file(s) [attempted 3553/8546 = 41%, 125 KB/s], Decompressed: 3547
Downloaded: 3593 file(s) [attempted 3593/8546 = 42%, 23 KB/s], Decompressed: 3587
Downloaded: 3638 file(s) [attempted 3638/8546 = 42%, 39 KB/s], Decompressed: 3631
Downloaded: 3679 file(s) [attempted 3679/8546 = 43%, 129 KB/s], Decompressed: 3668
Downloaded: 3719 file(s) [attempted 3719/8546 = 43%, 197 KB/s], Decompressed: 3712
Downloaded: 3756 file(s) [attempted 3756/8546 = 43%, 408 KB/s], Decompressed: 3746
Downloaded: 3794 file(s) [attempted 3794/8546 = 44%, 109 KB/s], Decompressed: 3790
Downloaded: 3838 file(s) [attempted 3838/8546 = 44%, 50 KB/s], Decompressed: 3834
Downloaded: 3878 file(s) [attempted 3878/8546 = 45%, 755 KB/s], Decompressed: 3875
Downloaded: 3919 file(s) [attempted 3919/8546 = 45%, 429 KB/s], Decompressed: 3912
Downloaded: 3946 file(s) [attempted 3946/8546 = 46%, 127 KB/s], Decompressed: 3942
Downloaded: 3990 file(s) [attempted 3990/8546 = 46%, 196 KB/s], Decompressed: 3986
Downloaded: 4037 file(s) [attempted 4037/8546 = 47%, 302 KB/s], Decompressed: 4030
Downloaded: 4084 file(s) [attempted 4084/8546 = 47%, 57 KB/s], Decompressed: 4078
Downloaded: 4128 file(s) [attempted 4128/8546 = 48%, 52 KB/s], Decompressed: 4125
Downloaded: 4166 file(s) [attempted 4166/8546 = 48%, 117 KB/s], Decompressed: 4159
Downloaded: 4203 file(s) [attempted 4203/8546 = 49%, 192 KB/s], Decompressed: 4201
Downloaded: 4240 file(s) [attempted 4240/8546 = 49%, 198 KB/s], Decompressed: 4233
Downloaded: 4281 file(s) [attempted 4281/8546 = 50%, 500 KB/s], Decompressed: 4277
Downloaded: 4325 file(s) [attempted 4325/8546 = 50%, 379 KB/s], Decompressed: 4321
Downloaded: 4365 file(s) [attempted 4365/8546 = 51%, 190 KB/s], Decompressed: 4358
Downloaded: 4402 file(s) [attempted 4402/8546 = 51%, 391 KB/s], Decompressed: 4399
Downloaded: 4443 file(s) [attempted 4443/8546 = 51%, 736 KB/s], Decompressed: 4440
Downloaded: 4484 file(s) [attempted 4484/8546 = 52%, 557 KB/s], Decompressed: 4477
Downloaded: 4525 file(s) [attempted 4525/8546 = 52%, 1555 KB/s], Decompressed: 4517
Downloaded: 4561 file(s) [attempted 4561/8546 = 53%, 291 KB/s], Decompressed: 4528
Downloaded: 4605 file(s) [attempted 4605/8546 = 53%, 111 KB/s], Decompressed: 4602
Downloaded: 4644 file(s) [attempted 4644/8546 = 54%, 93 KB/s], Decompressed: 4639
Downloaded: 4683 file(s) [attempted 4683/8546 = 54%, 319 KB/s], Decompressed: 4680
Downloaded: 4715 file(s) [attempted 4715/8546 = 55%, 239 KB/s], Decompressed: 4707
Downloaded: 4758 file(s) [attempted 4758/8546 = 55%, 327 KB/s], Decompressed: 4741
Downloaded: 4791 file(s) [attempted 4791/8546 = 56%, 272 KB/s], Decompressed: 4785
Downloaded: 4839 file(s) [attempted 4839/8546 = 56%, 1007 KB/s], Decompressed: 4835
Downloaded: 4886 file(s) [attempted 4886/8546 = 57%, 239 KB/s], Decompressed: 4879
Downloaded: 4927 file(s) [attempted 4927/8546 = 57%, 35 KB/s], Decompressed: 4917
Downloaded: 4964 file(s) [attempted 4964/8546 = 58%, 722 KB/s], Decompressed: 4961
Downloaded: 5010 file(s) [attempted 5010/8546 = 58%, 187 KB/s], Decompressed: 4991
Downloaded: 5043 file(s) [attempted 5043/8546 = 59%, 52 KB/s], Decompressed: 5035
Downloaded: 5086 file(s) [attempted 5086/8546 = 59%, 60 KB/s], Decompressed: 5082
Downloaded: 5126 file(s) [attempted 5126/8546 = 59%, 63 KB/s], Decompressed: 5123
Downloaded: 5164 file(s) [attempted 5164/8546 = 60%, 153 KB/s], Decompressed: 5160
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 119 KB/s], Decompressed: 5197
Downloaded: 5252 file(s) [attempted 5252/8546 = 61%, 37 KB/s], Decompressed: 5245
Downloaded: 5292 file(s) [attempted 5292/8546 = 61%, 852 KB/s], Decompressed: 5285
Downloaded: 5331 file(s) [attempted 5331/8546 = 62%, 132 KB/s], Decompressed: 5323
Downloaded: 5370 file(s) [attempted 5370/8546 = 62%, 1082 KB/s], Decompressed: 5363
Downloaded: 5408 file(s) [attempted 5408/8546 = 63%, 85 KB/s], Decompressed: 5404
Downloaded: 5451 file(s) [attempted 5451/8546 = 63%, 210 KB/s], Decompressed: 5444
Downloaded: 5492 file(s) [attempted 5492/8546 = 64%, 402 KB/s], Decompressed: 5485
Downloaded: 5533 file(s) [attempted 5533/8546 = 64%, 280 KB/s], Decompressed: 5522
Downloaded: 5566 file(s) [attempted 5566/8546 = 65%, 296 KB/s], Decompressed: 5559
Downloaded: 5609 file(s) [attempted 5609/8546 = 65%, 227 KB/s], Decompressed: 5600
Downloaded: 5647 file(s) [attempted 5647/8546 = 66%, 324 KB/s], Decompressed: 5641
Downloaded: 5688 file(s) [attempted 5688/8546 = 66%, 1357 KB/s], Decompressed: 5685
Downloaded: 5732 file(s) [attempted 5732/8546 = 67%, 71 KB/s], Decompressed: 5722
Downloaded: 5772 file(s) [attempted 5772/8546 = 67%, 179 KB/s], Decompressed: 5759
Downloaded: 5806 file(s) [attempted 5806/8546 = 67%, 37 KB/s], Decompressed: 5803
Downloaded: 5850 file(s) [attempted 5850/8546 = 68%, 902 KB/s], Decompressed: 5844
Downloaded: 5894 file(s) [attempted 5894/8546 = 68%, 1474 KB/s], Decompressed: 5888
Downloaded: 5938 file(s) [attempted 5938/8546 = 69%, 1247 KB/s], Decompressed: 5935
Downloaded: 5979 file(s) [attempted 5979/8546 = 69%, 261 KB/s], Decompressed: 5965
Downloaded: 6023 file(s) [attempted 6023/8546 = 70%, 137 KB/s], Decompressed: 6019
Downloaded: 6057 file(s) [attempted 6057/8546 = 70%, 533 KB/s], Decompressed: 6050
Downloaded: 6097 file(s) [attempted 6097/8546 = 71%, 44 KB/s], Decompressed: 6090
Downloaded: 6141 file(s) [attempted 6141/8546 = 71%, 106 KB/s], Decompressed: 6134
Downloaded: 6181 file(s) [attempted 6181/8546 = 72%, 432 KB/s], Decompressed: 6175
Downloaded: 6222 file(s) [attempted 6222/8546 = 72%, 190 KB/s], Decompressed: 6219
Downloaded: 6261 file(s) [attempted 6261/8546 = 73%, 326 KB/s], Decompressed: 6249
Downloaded: 6297 file(s) [attempted 6297/8546 = 73%, 672 KB/s], Decompressed: 6293
Downloaded: 6337 file(s) [attempted 6337/8546 = 74%, 89 KB/s], Decompressed: 6334
Downloaded: 6380 file(s) [attempted 6380/8546 = 74%, 515 KB/s], Decompressed: 6375
Downloaded: 6415 file(s) [attempted 6415/8546 = 75%, 828 KB/s], Decompressed: 6412
Downloaded: 6452 file(s) [attempted 6452/8546 = 75%, 286 KB/s], Decompressed: 6449
Downloaded: 6495 file(s) [attempted 6495/8546 = 76%, 762 KB/s], Decompressed: 6486
Downloaded: 6537 file(s) [attempted 6537/8546 = 76%, 134 KB/s], Decompressed: 6530
Downloaded: 6574 file(s) [attempted 6574/8546 = 76%, 100 KB/s], Decompressed: 6567
Downloaded: 6612 file(s) [attempted 6612/8546 = 77%, 59 KB/s], Decompressed: 6608
Downloaded: 6652 file(s) [attempted 6652/8546 = 77%, 478 KB/s], Decompressed: 6645
Downloaded: 6689 file(s) [attempted 6689/8546 = 78%, 138 KB/s], Decompressed: 6686
Downloaded: 6730 file(s) [attempted 6730/8546 = 78%, 1083 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8546 = 79%, 123 KB/s], Decompressed: 6770
Downloaded: 6814 file(s) [attempted 6814/8546 = 79%, 168 KB/s], Decompressed: 6811
Downloaded: 6855 file(s) [attempted 6855/8546 = 80%, 24 KB/s], Decompressed: 6848
Downloaded: 6894 file(s) [attempted 6894/8546 = 80%, 229 KB/s], Decompressed: 6882
Downloaded: 6933 file(s) [attempted 6933/8546 = 81%, 176 KB/s], Decompressed: 6929
Downloaded: 6977 file(s) [attempted 6977/8546 = 81%, 487 KB/s], Decompressed: 6970
Downloaded: 7014 file(s) [attempted 7014/8546 = 82%, 247 KB/s], Decompressed: 7000
Downloaded: 7053 file(s) [attempted 7053/8546 = 82%, 705 KB/s], Decompressed: 7048
Downloaded: 7088 file(s) [attempted 7088/8546 = 82%, 127 KB/s], Decompressed: 7085
Downloaded: 7132 file(s) [attempted 7132/8546 = 83%, 33 KB/s], Decompressed: 7129
Downloaded: 7171 file(s) [attempted 7171/8546 = 83%, 533 KB/s], Decompressed: 7156
Downloaded: 7203 file(s) [attempted 7203/8546 = 84%, 224 KB/s], Decompressed: 7197
Downloaded: 7247 file(s) [attempted 7247/8546 = 84%, 982 KB/s], Decompressed: 7241
Downloaded: 7288 file(s) [attempted 7288/8546 = 85%, 163 KB/s], Decompressed: 7281
Downloaded: 7332 file(s) [attempted 7332/8546 = 85%, 63 KB/s], Decompressed: 7322
Downloaded: 7373 file(s) [attempted 7373/8546 = 86%, 36 KB/s], Decompressed: 7366
Downloaded: 7407 file(s) [attempted 7407/8546 = 86%, 80 KB/s], Decompressed: 7403
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 301 KB/s], Decompressed: 7447
Downloaded: 7491 file(s) [attempted 7491/8546 = 87%, 126 KB/s], Decompressed: 7484
Downloaded: 7528 file(s) [attempted 7528/8546 = 88%, 114 KB/s], Decompressed: 7521
Downloaded: 7575 file(s) [attempted 7575/8546 = 88%, 136 KB/s], Decompressed: 7572
Downloaded: 7623 file(s) [attempted 7623/8546 = 89%, 168 KB/s], Decompressed: 7616
Downloaded: 7663 file(s) [attempted 7663/8546 = 89%, 1538 KB/s], Decompressed: 7660
Downloaded: 7707 file(s) [attempted 7707/8546 = 90%, 1298 KB/s], Decompressed: 7701
Downloaded: 7738 file(s) [attempted 7738/8546 = 90%, 75 KB/s], Decompressed: 7731
Downloaded: 7758 file(s) [attempted 7758/8546 = 90%, 996 KB/s], Decompressed: 7755
Downloaded: 7782 file(s) [attempted 7782/8546 = 91%, 126 KB/s], Decompressed: 7778
Downloaded: 7802 file(s) [attempted 7802/8546 = 91%, 318 KB/s], Decompressed: 7799
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 169 KB/s], Decompressed: 7816
Downloaded: 7863 file(s) [attempted 7863/8546 = 92%, 318 KB/s], Decompressed: 7860
Downloaded: 7910 file(s) [attempted 7910/8546 = 92%, 806 KB/s], Decompressed: 7907
Downloaded: 7954 file(s) [attempted 7954/8546 = 93%, 154 KB/s], Decompressed: 7931
Downloaded: 7970 file(s) [attempted 7970/8546 = 93%, 92 KB/s], Decompressed: 7965
Downloaded: 8015 file(s) [attempted 8015/8546 = 93%, 357 KB/s], Decompressed: 8012
Downloaded: 8063 file(s) [attempted 8063/8546 = 94%, 944 KB/s], Decompressed: 8059
Downloaded: 8107 file(s) [attempted 8107/8546 = 94%, 234 KB/s], Decompressed: 8103
Downloaded: 8154 file(s) [attempted 8154/8546 = 95%, 792 KB/s], Decompressed: 8151
Downloaded: 8198 file(s) [attempted 8198/8546 = 95%, 645 KB/s], Decompressed: 8184
Downloaded: 8225 file(s) [attempted 8225/8546 = 96%, 162 KB/s], Decompressed: 8222
Downloaded: 8269 file(s) [attempted 8269/8546 = 96%, 49 KB/s], Decompressed: 8266
Downloaded: 8307 file(s) [attempted 8307/8546 = 97%, 80 KB/s], Decompressed: 8303
Downloaded: 8350 file(s) [attempted 8350/8546 = 97%, 866 KB/s], Decompressed: 8347
Downloaded: 8394 file(s) [attempted 8394/8546 = 98%, 361 KB/s], Decompressed: 8387
Downloaded: 8438 file(s) [attempted 8438/8546 = 98%, 79 KB/s], Decompressed: 8435
Downloaded: 8477 file(s) [attempted 8477/8546 = 99%, 891 KB/s], Decompressed: 8472
Downloaded: 8518 file(s) [attempted 8518/8546 = 99%, 180 KB/s], Decompressed: 8509
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 262 KB/s], Decompressed: 8543
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 262 KB/s], Decompressed: 8543

lake build

✔ [3021/3027] Built PrimeNumberTheoremAnd.Fourier (45s)
✔ [3059/3072] Built PrimeNumberTheoremAnd.Defs (15s)
✔ [3553/3561] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (8.0s)
✔ [3566/3585] Built PrimeNumberTheoremAnd.ZetaBounds (18s)
ℹ [3623/3633] Built PrimeNumberTheoremAnd.MediumPNT (28s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3637/3648] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (20s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (15s)
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`
✔ [3654/3667] Built PrimeNumberTheoremAnd.BorelCaratheodory (3.5s)
⚠ [3779/3784] Built PrimeNumberTheoremAnd.Wiener (25s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3781/3795] Built PrimeNumberTheoremAnd.Consequences (26s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (3.0s)
⚠ [3895/3906] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (2.6s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3963/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (46s)
⚠ [3964/3974] Replayed LeanCert.Examples.Li2Bounds
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.8s)
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.7s)
✔ [3970/3977] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.6s)
✔ [3974/3978] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (7.0s)
⚠ [3975/3984] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.3s)
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 (10s)
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`
⚠ [4110/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (16s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4111/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (77s)
⚠ [4112/4118] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4114/4147] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (26s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4125/4151] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (4.0s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.8s)
✔ [4131/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (16s)
✔ [4132/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (10s)
✔ [4133/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (60s)
✔ [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 (33s)
✔ [4138/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (32s)
✔ [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 (33s)
✔ [4141/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (32s)
✔ [4142/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (32s)
✔ [4143/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (32s)
✔ [4144/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (32s)
✔ [4145/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.4s)
✔ [4146/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.9s)
✔ [4147/4161] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
✔ [4148/4161] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (44s)
✔ [4150/4161] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (4.1s)
✔ [4151/4161] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (2.6s)
✔ [4152/4163] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (57s)
⚠ [4153/4165] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (11s)
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`
⚠ [4155/4165] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (20s)
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 (37s)
✔ [4158/4165] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (18s)
⚠ [4160/4168] Built PrimeNumberTheoremAnd.IEANTN.Dusart (16s)
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.6s)
✔ [4164/4170] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
✔ [4165/4170] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (44s)
ℹ [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/4178] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (55s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
✔ [4185/4202] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (17s)
✔ [4186/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4187/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (21s)
✔ [4188/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (21s)
✔ [4189/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (21s)
✔ [4190/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (21s)
✔ [4191/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (22s)
✔ [4192/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (21s)
✔ [4193/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (22s)
✔ [4194/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (21s)
✔ [4195/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (22s)
✔ [4196/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (22s)
✔ [4197/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (21s)
✔ [4198/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4199/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (21s)
⚠ [4201/4205] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (3.9s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4203/4210] 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`
✔ [4215/4226] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (11s)
✔ [4220/4260] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (6.1s)
✔ [4221/4260] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (3.2s)
✔ [4222/4262] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.0s)
⚠ [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`
⚠ [4248/4285] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.5s)
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`
⚠ [4253/4285] 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`
✔ [4258/4285] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
✔ [4259/4285] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (53s)
⚠ [4260/4285] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.4s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4263/4285] Built PrimeNumberTheoremAnd.IEANTN.Lcm (28s)
✔ [4266/4285] Built PrimeNumberTheoremAnd.PerronFormula (6.6s)
✔ [4267/4285] Built PrimeNumberTheoremAnd.RectangleArgumentPrinciple (3.1s)
✔ [4272/4285] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.6s)
✔ [4282/4285] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (4.6s)
⚠ [4283/4285] 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`
✔ [4284/4285] Built PrimeNumberTheoremAnd (3.1s)
Build completed successfully (4285 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (4.5s)
✔ [32/35] Built Cli.Extensions:c.o (490ms)
✔ [33/35] Built Cli:c.o (62ms)
✔ [3055/3066] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (3.9s)
✔ [3084/3097] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (11s)
✔ [3586/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (12s)
✔ [3601/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (62s)
ℹ [3682/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3687/3701] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (57s)
✔ [3707/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (2.9s)
⚠ [3710/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`
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (55s)
✔ [3723/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.7s)
⚠ [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 (35s)
✔ [3854/3868] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (13s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3971/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (2.9s)
✔ [3972/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.0s)
⚠ [4045/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [4050/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (26s)
⚠ [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`
✔ [4057/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.4s)
✔ [4060/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.7s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.0s)
⚠ [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/4074] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [4069/4074] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.5s)
⚠ [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/4217] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4205/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.4s)
⚠ [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`
✔ [4210/4268] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4211/4268] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4212/4268] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.7s)
⚠ [4213/4268] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4216/4271] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4227/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.1s)
✔ [4231/4292] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.3s)
✔ [4253/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.1s)
✔ [4254/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.2s)
✔ [4255/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.2s)
✔ [4256/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.2s)
✔ [4257/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.2s)
✔ [4258/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.2s)
✔ [4259/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.2s)
✔ [4260/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.2s)
✔ [4261/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.1s)
✔ [4262/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.2s)
✔ [4263/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.2s)
✔ [4264/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.3s)
✔ [4265/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.1s)
✔ [4266/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.2s)
✔ [4267/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.2s)
✔ [4268/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.2s)
✔ [4269/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.2s)
✔ [4271/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (50s)
⚠ [4272/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`
✔ [4274/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.5s)
✔ [4275/4295] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.6s)
⚠ [4276/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`
✔ [4278/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.5s)
✔ [4280/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (20s)
✔ [4282/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.6s)
⚠ [4283/4302] 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`
✔ [4286/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.3s)
✔ [4288/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (17s)
✔ [4289/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4293/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.2s)
✔ [4295/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4297/4306] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (12s)
ℹ [4298/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.
✔ [4299/4307] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.7s)
⚠ [4300/4307] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
✔ [4301/4345] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (33s)
✔ [4319/4355] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.5s)
✔ [4335/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.2s)
✔ [4336/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.2s)
✔ [4337/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.3s)
✔ [4338/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.1s)
✔ [4339/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.3s)
✔ [4340/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.1s)
✔ [4341/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.3s)
✔ [4342/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.2s)
✔ [4343/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.2s)
✔ [4344/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.1s)
✔ [4345/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.1s)
✔ [4346/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.2s)
✔ [4347/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.1s)
✔ [4348/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.2s)
⚠ [4349/4356] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4351/4358] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.2s)
⚠ [4352/4358] 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`
✔ [4355/4385] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.3s)
✔ [4367/4385] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.1s)
✔ [4374/4453] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers:blueprint (2.9s)
✔ [4394/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.3s)
⚠ [4395/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`
✔ [4396/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (2.9s)
⚠ [4423/4495] 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`
✔ [4425/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4426/4495] 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`
✔ [4446/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4448/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.7s)
⚠ [4449/4495] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4460/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4461/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.RectangleArgumentPrinciple:blueprint (2.5s)
✔ [4462/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.9s)
✔ [4467/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4468/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.3s)
✔ [4469/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4489/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (4.1s)
⚠ [4490/4495] 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`
✔ [4491/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (42s)
✔ [4493/4495] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (4.4s)
ℹ [4494/4496] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (63ms)
info: Blueprint indexing
Build completed successfully (4496 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

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

apx-semantic-phase	{"duration_ms":17,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2311,"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":483822,"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":2,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":168548,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":168548,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":3316,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":479251,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.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":344356,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":344356,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":4872,"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":479918,"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":2,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":255256,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"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":24074,"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":477493,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":1281745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":1281745,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":8911,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 05d2d50cab05b3f97e2fef779e772d269554c41458abec1e0f4110aea81dc7b9
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":56,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1981645,"ok":true}

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":5683,"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":494315,"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":8,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396654,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"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":20299,"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":487383,"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":22,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1486947,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"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":24929,"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":496411,"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":29,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1805467,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1805467,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":15004,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 05d2d50cab05b3f97e2fef779e772d269554c41458abec1e0f4110aea81dc7b9
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":63,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1535401,"ok":true}