Run 122

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

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

git checkout e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc

fatal: reference is not a tree: e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc

git fetch --depth 1 origin e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc

From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc -> FETCH_HEAD

git checkout e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc (after fetch)

Note: switching to 'e3fb6ef3e305742d1c8b78a2c899e34e9ca997cc'.

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 e3fb6ef chore(Mertens/ZetaBounds): unify use of Euler-Maclaurin (#1561)

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 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/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 34 KB/s], Decompressed: 34
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 108 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 302 KB/s], Decompressed: 93
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 84 KB/s], Decompressed: 131
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 691 KB/s], Decompressed: 168
Downloaded: 210 file(s) [attempted 210/8459 = 2%, 441 KB/s], Decompressed: 206
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 37 KB/s], Decompressed: 240
Downloaded: 284 file(s) [attempted 284/8459 = 3%, 748 KB/s], Decompressed: 275
Downloaded: 326 file(s) [attempted 326/8459 = 3%, 388 KB/s], Decompressed: 323
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 604 KB/s], Decompressed: 367
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 229 KB/s], Decompressed: 405
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 71 KB/s], Decompressed: 449
Downloaded: 494 file(s) [attempted 494/8459 = 5%, 258 KB/s], Decompressed: 487
Downloaded: 530 file(s) [attempted 530/8459 = 6%, 272 KB/s], Decompressed: 525
Downloaded: 575 file(s) [attempted 575/8459 = 6%, 608 KB/s], Decompressed: 566
Downloaded: 614 file(s) [attempted 614/8459 = 7%, 470 KB/s], Decompressed: 610
Downloaded: 655 file(s) [attempted 655/8459 = 7%, 402 KB/s], Decompressed: 641
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 240 KB/s], Decompressed: 696
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 252 KB/s], Decompressed: 737
Downloaded: 785 file(s) [attempted 785/8459 = 9%, 349 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 169 KB/s], Decompressed: 823
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 43 KB/s], Decompressed: 867
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 981 KB/s], Decompressed: 912
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 180 KB/s], Decompressed: 960
Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 26 KB/s], Decompressed: 997
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 114 KB/s], Decompressed: 1035
Downloaded: 1084 file(s) [attempted 1084/8459 = 12%, 76 KB/s], Decompressed: 1080
Downloaded: 1131 file(s) [attempted 1131/8459 = 13%, 98 KB/s], Decompressed: 1127
Downloaded: 1176 file(s) [attempted 1176/8459 = 13%, 102 KB/s], Decompressed: 1169
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 102 KB/s], Decompressed: 1206
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 122 KB/s], Decompressed: 1251
Downloaded: 1296 file(s) [attempted 1296/8459 = 15%, 842 KB/s], Decompressed: 1288
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 541 KB/s], Decompressed: 1333
Downloaded: 1381 file(s) [attempted 1381/8459 = 16%, 251 KB/s], Decompressed: 1374
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 83 KB/s], Decompressed: 1415
Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 111 KB/s], Decompressed: 1459
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 149 KB/s], Decompressed: 1504
Downloaded: 1544 file(s) [attempted 1544/8459 = 18%, 256 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 36 KB/s], Decompressed: 1583
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1743 KB/s], Decompressed: 1617
Downloaded: 1667 file(s) [attempted 1667/8459 = 19%, 453 KB/s], Decompressed: 1661
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 443 KB/s], Decompressed: 1709
Downloaded: 1750 file(s) [attempted 1750/8459 = 20%, 742 KB/s], Decompressed: 1743
Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 55 KB/s], Decompressed: 1788
Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 692 KB/s], Decompressed: 1826
Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 301 KB/s], Decompressed: 1867
Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 470 KB/s], Decompressed: 1904
Downloaded: 1952 file(s) [attempted 1952/8459 = 23%, 55 KB/s], Decompressed: 1949
Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 510 KB/s], Decompressed: 1993
Downloaded: 2041 file(s) [attempted 2041/8459 = 24%, 35 KB/s], Decompressed: 2031
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 306 KB/s], Decompressed: 2072
Downloaded: 2117 file(s) [attempted 2117/8459 = 25%, 685 KB/s], Decompressed: 2113
Downloaded: 2160 file(s) [attempted 2160/8459 = 25%, 437 KB/s], Decompressed: 2151
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 204 KB/s], Decompressed: 2195
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 192 KB/s], Decompressed: 2240
Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 23 KB/s], Decompressed: 2284
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 94 KB/s], Decompressed: 2325
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 235 KB/s], Decompressed: 2370
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 46 KB/s], Decompressed: 2407
Downloaded: 2452 file(s) [attempted 2452/8459 = 28%, 91 KB/s], Decompressed: 2448
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 644 KB/s], Decompressed: 2483
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 650 KB/s], Decompressed: 2520
Downloaded: 2573 file(s) [attempted 2573/8459 = 30%, 927 KB/s], Decompressed: 2568
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 83 KB/s], Decompressed: 2613
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 655 KB/s], Decompressed: 2661
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 127 KB/s], Decompressed: 2698
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 598 KB/s], Decompressed: 2733
Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 32 KB/s], Decompressed: 2770
Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 82 KB/s], Decompressed: 2811
Downloaded: 2857 file(s) [attempted 2857/8459 = 33%, 268 KB/s], Decompressed: 2852
Downloaded: 2902 file(s) [attempted 2902/8459 = 34%, 126 KB/s], Decompressed: 2893
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 1046 KB/s], Decompressed: 2934
Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 35 KB/s], Decompressed: 2972
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 211 KB/s], Decompressed: 3013
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 230 KB/s], Decompressed: 3058
Downloaded: 3103 file(s) [attempted 3103/8459 = 36%, 230 KB/s], Decompressed: 3095
Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 329 KB/s], Decompressed: 3140
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 1307 KB/s], Decompressed: 3177
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 167 KB/s], Decompressed: 3218
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 198 KB/s], Decompressed: 3263
Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 615 KB/s], Decompressed: 3304
Downloaded: 3351 file(s) [attempted 3351/8459 = 39%, 731 KB/s], Decompressed: 3345
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 76 KB/s], Decompressed: 3383
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 84 KB/s], Decompressed: 3424
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 1988 KB/s], Decompressed: 3472
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 275 KB/s], Decompressed: 3509
Downloaded: 3558 file(s) [attempted 3558/8459 = 42%, 703 KB/s], Decompressed: 3554
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 190 KB/s], Decompressed: 3588
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 122 KB/s], Decompressed: 3636
Downloaded: 3682 file(s) [attempted 3682/8459 = 43%, 341 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 158 KB/s], Decompressed: 3718
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 106 KB/s], Decompressed: 3759
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 385 KB/s], Decompressed: 3800
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 787 KB/s], Decompressed: 3845
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 144 KB/s], Decompressed: 3882
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 150 KB/s], Decompressed: 3923
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 693 KB/s], Decompressed: 3961
Downloaded: 4008 file(s) [attempted 4008/8459 = 47%, 50 KB/s], Decompressed: 4002
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 146 KB/s], Decompressed: 4047
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 195 KB/s], Decompressed: 4091
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 332 KB/s], Decompressed: 4130
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 57 KB/s], Decompressed: 4160
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 197 KB/s], Decompressed: 4197
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 955 KB/s], Decompressed: 4249
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 623 KB/s], Decompressed: 4290
Downloaded: 4340 file(s) [attempted 4340/8459 = 51%, 67 KB/s], Decompressed: 4327
Downloaded: 4379 file(s) [attempted 4379/8459 = 51%, 178 KB/s], Decompressed: 4372
Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 83 KB/s], Decompressed: 4403
Downloaded: 4454 file(s) [attempted 4454/8459 = 52%, 1964 KB/s], Decompressed: 4451
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 300 KB/s], Decompressed: 4492
Downloaded: 4539 file(s) [attempted 4539/8459 = 53%, 42 KB/s], Decompressed: 4533
Downloaded: 4581 file(s) [attempted 4581/8459 = 54%, 691 KB/s], Decompressed: 4577
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 1109 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 54 KB/s], Decompressed: 4652
Downloaded: 4699 file(s) [attempted 4699/8459 = 55%, 1135 KB/s], Decompressed: 4694
Downloaded: 4744 file(s) [attempted 4744/8459 = 56%, 111 KB/s], Decompressed: 4735
Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 141 KB/s], Decompressed: 4782
Downloaded: 4829 file(s) [attempted 4829/8459 = 57%, 2057 KB/s], Decompressed: 4824
Downloaded: 4872 file(s) [attempted 4872/8459 = 57%, 195 KB/s], Decompressed: 4865
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 475 KB/s], Decompressed: 4895
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 52 KB/s], Decompressed: 4943
Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 484 KB/s], Decompressed: 4991
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 64 KB/s], Decompressed: 5029
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 120 KB/s], Decompressed: 5073
Downloaded: 5114 file(s) [attempted 5114/8459 = 60%, 102 KB/s], Decompressed: 5111
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 1328 KB/s], Decompressed: 5145
Downloaded: 5193 file(s) [attempted 5193/8459 = 61%, 241 KB/s], Decompressed: 5186
Downloaded: 5238 file(s) [attempted 5238/8459 = 61%, 1762 KB/s], Decompressed: 5234
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 301 KB/s], Decompressed: 5268
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 231 KB/s], Decompressed: 5310
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 1171 KB/s], Decompressed: 5347
Downloaded: 5398 file(s) [attempted 5398/8459 = 63%, 93 KB/s], Decompressed: 5388
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 72 KB/s], Decompressed: 5433
Downloaded: 5482 file(s) [attempted 5482/8459 = 64%, 536 KB/s], Decompressed: 5477
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 96 KB/s], Decompressed: 5511
Downloaded: 5557 file(s) [attempted 5557/8459 = 65%, 48 KB/s], Decompressed: 5549
Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 709 KB/s], Decompressed: 5590
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 46 KB/s], Decompressed: 5638
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 219 KB/s], Decompressed: 5679
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 293 KB/s], Decompressed: 5720
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 110 KB/s], Decompressed: 5761
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 25 KB/s], Decompressed: 5809
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 112 KB/s], Decompressed: 5847
Downloaded: 5892 file(s) [attempted 5892/8459 = 69%, 162 KB/s], Decompressed: 5888
Downloaded: 5930 file(s) [attempted 5930/8459 = 70%, 113 KB/s], Decompressed: 5926
Downloaded: 5973 file(s) [attempted 5973/8459 = 70%, 596 KB/s], Decompressed: 5969
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 69 KB/s], Decompressed: 6011
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 328 KB/s], Decompressed: 6052
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1270 KB/s], Decompressed: 6090
Downloaded: 6135 file(s) [attempted 6135/8459 = 72%, 903 KB/s], Decompressed: 6127
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 558 KB/s], Decompressed: 6172
Downloaded: 6216 file(s) [attempted 6216/8459 = 73%, 42 KB/s], Decompressed: 6206
Downloaded: 6255 file(s) [attempted 6255/8459 = 73%, 87 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 859 KB/s], Decompressed: 6285
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 373 KB/s], Decompressed: 6333
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 149 KB/s], Decompressed: 6377
Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 1563 KB/s], Decompressed: 6418
Downloaded: 6464 file(s) [attempted 6464/8459 = 76%, 141 KB/s], Decompressed: 6456
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 45 KB/s], Decompressed: 6504
Downloaded: 6555 file(s) [attempted 6555/8459 = 77%, 239 KB/s], Decompressed: 6548
Downloaded: 6600 file(s) [attempted 6600/8459 = 78%, 467 KB/s], Decompressed: 6596
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 244 KB/s], Decompressed: 6631
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 373 KB/s], Decompressed: 6668
Downloaded: 6720 file(s) [attempted 6720/8459 = 79%, 258 KB/s], Decompressed: 6716
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 426 KB/s], Decompressed: 6757
Downloaded: 6808 file(s) [attempted 6808/8459 = 80%, 891 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 36 KB/s], Decompressed: 6843
Downloaded: 6882 file(s) [attempted 6882/8459 = 81%, 195 KB/s], Decompressed: 6874
Downloaded: 6921 file(s) [attempted 6921/8459 = 81%, 207 KB/s], Decompressed: 6918
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 162 KB/s], Decompressed: 6963
Downloaded: 7010 file(s) [attempted 7010/8459 = 82%, 291 KB/s], Decompressed: 7007
Downloaded: 7055 file(s) [attempted 7055/8459 = 83%, 35 KB/s], Decompressed: 7045
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 200 KB/s], Decompressed: 7093
Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 135 KB/s], Decompressed: 7134
Downloaded: 7183 file(s) [attempted 7183/8459 = 84%, 134 KB/s], Decompressed: 7178
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 134 KB/s], Decompressed: 7223
Downloaded: 7260 file(s) [attempted 7260/8459 = 85%, 189 KB/s], Decompressed: 7258
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 27 KB/s], Decompressed: 7294
Downloaded: 7346 file(s) [attempted 7346/8459 = 86%, 317 KB/s], Decompressed: 7339
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 462 KB/s], Decompressed: 7380
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 206 KB/s], Decompressed: 7428
Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 295 KB/s], Decompressed: 7455
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 210 KB/s], Decompressed: 7503
Downloaded: 7550 file(s) [attempted 7550/8459 = 89%, 55 KB/s], Decompressed: 7541
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 98 KB/s], Decompressed: 7585
Downloaded: 7633 file(s) [attempted 7633/8459 = 90%, 1279 KB/s], Decompressed: 7630
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 149 KB/s], Decompressed: 7678
Downloaded: 7719 file(s) [attempted 7719/8459 = 91%, 46 KB/s], Decompressed: 7715
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 75 KB/s], Decompressed: 7760
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 192 KB/s], Decompressed: 7801
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 151 KB/s], Decompressed: 7842
Downloaded: 7889 file(s) [attempted 7889/8459 = 93%, 1137 KB/s], Decompressed: 7880
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 638 KB/s], Decompressed: 7914
Downloaded: 7963 file(s) [attempted 7963/8459 = 94%, 308 KB/s], Decompressed: 7955
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 48 KB/s], Decompressed: 8003
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 119 KB/s], Decompressed: 8047
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 161 KB/s], Decompressed: 8085
Downloaded: 8129 file(s) [attempted 8129/8459 = 96%, 927 KB/s], Decompressed: 8126
Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 1393 KB/s], Decompressed: 8164
Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 139 KB/s], Decompressed: 8208
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 1132 KB/s], Decompressed: 8253
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 410 KB/s], Decompressed: 8290
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 851 KB/s], Decompressed: 8331
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 317 KB/s], Decompressed: 8376
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 281 KB/s], Decompressed: 8417
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 649 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 649 KB/s], Decompressed: 8455

lake build

✔ [3473/3481] Built PrimeNumberTheoremAnd.ZetaBounds (91s)
ℹ [3538/3549] Built PrimeNumberTheoremAnd.MediumPNT (38s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3549/3566] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (20s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (13s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3567/3573] Built PrimeNumberTheoremAnd.BorelCaratheodory (9.4s)
⚠ [3699/3706] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3704/3714] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3763/3769] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (50s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3765/3769] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (35s)
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`
✔ [3767/3779] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.9s)
✔ [3873/3886] Built PrimeNumberTheoremAnd.IEANTN.LogTables (9.1s)
✔ [3875/3886] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.9s)
⚠ [3879/3890] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.7s)
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`
⚠ [3880/3890] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3884/3891] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.5s)
✔ [3888/3891] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (9.6s)
✔ [3890/3891] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (9.3s)
⚠ [4010/4018] 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`
⚠ [4014/4021] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (17s)
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`
✔ [4015/4021] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (91s)
⚠ [4016/4022] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4018/4039] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4029/4057] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.8s)
✔ [4032/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (8.0s)
✔ [4034/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (18s)
✔ [4035/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4036/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (278s)
✔ [4037/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (229s)
✔ [4038/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (203s)
✔ [4039/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (182s)
✔ [4040/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (135s)
✔ [4041/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (129s)
✔ [4042/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (112s)
✔ [4043/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (113s)
✔ [4044/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (100s)
✔ [4045/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (87s)
✔ [4046/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (97s)
✔ [4047/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (80s)
✔ [4048/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (26s)
✔ [4049/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (33s)
✔ [4050/4064] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (19s)
⚠ [4051/4064] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (45s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: 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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4053/4064] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (10s)
✔ [4055/4071] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (123s)
⚠ [4056/4071] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (28s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [4058/4071] 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`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4060/4071] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (83s)
⚠ [4062/4071] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (60s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
✔ [4065/4071] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (26s)
⚠ [4066/4072] Built PrimeNumberTheoremAnd.IEANTN.Dusart (18s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [4068/4073] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.8s)
✔ [4070/4073] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (44s)
✔ [4071/4079] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (19s)
⚠ [4084/4128] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (11s)
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4088/4130] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.6s)
⚠ [4108/4136] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4115/4140] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.1s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4120/4140] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
⚠ [4123/4146] 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`
✔ [4127/4153] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4128/4153] Built PrimeNumberTheoremAnd.IEANTN.Mertens (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [4132/4153] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
⚠ [4135/4153] 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`
ℹ [4146/4153] 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.
✔ [4150/4153] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (55s)
⚠ [4151/4153] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:128:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:165:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:273:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:532:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:575:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1975:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2001:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2607:8: declaration uses `sorry`
✔ [4152/4153] Built PrimeNumberTheoremAnd (3.7s)
Build completed successfully (4153 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

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (535ms)
✔ [33/41] Built Cli:c.o (66ms)
✔ [3509/3546] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (67s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3596/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (59s)
✔ [3616/3641] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (2.9s)
⚠ [3626/3642] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3634/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3637/3647] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.5s)
⚠ [3767/3784] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3771/3789] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3841/3851] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3842/3851] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (25s)
⚠ [3843/3851] 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`
✔ [3845/3851] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.2s)
✔ [3848/3861] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.8s)
✔ [3956/3977] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.6s)
✔ [3961/3980] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [3962/3980] 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`
✔ [3966/3982] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
⚠ [3967/3982] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3974/3982] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.1s)
✔ [3979/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.5s)
✔ [3981/3986] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.7s)
⚠ [4101/4116] 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`
⚠ [4105/4120] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4108/4120] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.4s)
⚠ [4109/4120] 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`
✔ [4113/4171] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4114/4171] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4115/4171] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.6s)
⚠ [4116/4171] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4119/4192] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4131/4192] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.9s)
⚠ [4133/4192] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: 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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4137/4194] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (50s)
⚠ [4138/4194] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
✔ [4139/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.0s)
✔ [4158/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.6s)
⚠ [4160/4202] 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`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4162/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.0s)
✔ [4163/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.1s)
✔ [4165/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.1s)
✔ [4166/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.1s)
✔ [4167/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.0s)
✔ [4168/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.0s)
✔ [4169/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.0s)
✔ [4170/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.0s)
✔ [4171/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.0s)
✔ [4172/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.0s)
✔ [4173/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.0s)
✔ [4174/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.1s)
✔ [4175/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.1s)
✔ [4176/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.1s)
✔ [4177/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.0s)
✔ [4178/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.1s)
✔ [4179/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.0s)
✔ [4180/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (18s)
⚠ [4182/4203] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
⚠ [4187/4203] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [4189/4204] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4191/4205] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.0s)
✔ [4193/4205] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4194/4205] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4198/4207] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.0s)
✔ [4200/4207] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4202/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.1s)
✔ [4206/4232] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (13s)
⚠ [4213/4232] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4218/4299] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.1s)
✔ [4238/4313] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.2s)
⚠ [4239/4313] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4244/4320] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4245/4320] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4272/4330] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.5s)
⚠ [4273/4330] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4286/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.0s)
✔ [4292/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
⚠ [4293/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [4294/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
⚠ [4297/4342] 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`
✔ [4311/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (34s)
✔ [4312/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.9s)
ℹ [4314/4342] 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.
✔ [4327/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.9s)
⚠ [4336/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:128:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:165:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:273:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:532:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:575:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1975:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2001:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2607:8: declaration uses `sorry`
✔ [4337/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4338/4342] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (44s)
✔ [4340/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.2s)
ℹ [4341/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (55ms)
info: Blueprint indexing
Build completed successfully (4343 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":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":158,"diagnostic_count":52,"duration_ms":18247,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":411676,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":158,"diagnostic_count":52,"duration_ms":7,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.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":2105901,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2105901,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":177,"diagnostic_count":46,"duration_ms":17300,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":404884,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":177,"diagnostic_count":46,"duration_ms":14,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.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":1044442,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1044442,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":443,"diagnostic_count":273,"duration_ms":41857,"module_name":"PrimeNumberTheoremAnd.ZetaBounds","module_path":"PrimeNumberTheoremAnd/ZetaBounds.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":397251,"module_count":1,"module_name":"PrimeNumberTheoremAnd.ZetaBounds","module_path":"PrimeNumberTheoremAnd/ZetaBounds.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":443,"diagnostic_count":273,"duration_ms":21,"module_count":1,"module_name":"PrimeNumberTheoremAnd.ZetaBounds","module_path":"PrimeNumberTheoremAnd/ZetaBounds.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":3412708,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":3412708,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":8163,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"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":1371667,"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":351,"diagnostic_count":268,"duration_ms":31445,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":410271,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":351,"diagnostic_count":268,"duration_ms":17,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.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":2947852,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2947852,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":540,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":407449,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.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":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":231,"diagnostic_count":161,"duration_ms":19833,"module_name":"PrimeNumberTheoremAnd.MediumPNT","module_path":"PrimeNumberTheoremAnd/MediumPNT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":393383,"module_count":1,"module_name":"PrimeNumberTheoremAnd.MediumPNT","module_path":"PrimeNumberTheoremAnd/MediumPNT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":231,"diagnostic_count":161,"duration_ms":11,"module_count":1,"module_name":"PrimeNumberTheoremAnd.MediumPNT","module_path":"PrimeNumberTheoremAnd/MediumPNT.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":1718199,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1718199,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":26}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":14663,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":50,"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":1284826,"ok":true}

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":10414,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":411843,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.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":509503,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509503,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":402118,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.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":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":42,"diagnostic_count":31,"duration_ms":3258,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":419124,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":42,"diagnostic_count":31,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.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":209195,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":209195,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":205,"diagnostic_count":137,"duration_ms":17262,"module_name":"PrimeNumberTheoremAnd.StrongPNT","module_path":"PrimeNumberTheoremAnd/StrongPNT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":397429,"module_count":1,"module_name":"PrimeNumberTheoremAnd.StrongPNT","module_path":"PrimeNumberTheoremAnd/StrongPNT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":205,"diagnostic_count":137,"duration_ms":18,"module_count":1,"module_name":"PrimeNumberTheoremAnd.StrongPNT","module_path":"PrimeNumberTheoremAnd/StrongPNT.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":1503514,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":1503514,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10356,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":46,"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":1669697,"ok":true}

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":5162,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":404252,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.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":430031,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1420,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":429105,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.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":101503,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":21717,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":436064,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":33,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.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":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":15369,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":464,"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":1307196,"ok":true}

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":159,"diagnostic_count":101,"duration_ms":11803,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":413872,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":159,"diagnostic_count":101,"duration_ms":7,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.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":936198,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":936198,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":681,"diagnostic_count":493,"duration_ms":64813,"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":419455,"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":681,"diagnostic_count":493,"duration_ms":41,"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":3854329,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3854329,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":402728,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.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":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":26}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":7591,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":40,"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":1317222,"ok":true}

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":2786,"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":422646,"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":2,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":265,"diagnostic_count":144,"duration_ms":21242,"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":423583,"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":265,"diagnostic_count":144,"duration_ms":24,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1291893,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1291893,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":8972,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":46,"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":874789,"ok":true}

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":4257,"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":415485,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":4017,"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":409683,"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":7,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":7454,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":33,"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":837760,"ok":true}

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":18150,"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":426678,"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":10,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":269,"diagnostic_count":182,"duration_ms":23005,"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":426670,"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":269,"diagnostic_count":182,"duration_ms":13,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1825220,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1825220,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":8795,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 99123414dc8a56b156122ff96b3b77339036a0402efc070b60c842590ce983af
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":48,"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":898973,"ok":true}