Run 52

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

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

git checkout 3d767d56dc9f06459a32daa83c3f340648c24e7f

Note: switching to '3d767d56dc9f06459a32daa83c3f340648c24e7f'.

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 3d767d5 fix: align Dusart lemma_5_10b with 1-indexed prime numbering (#1566)

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%, 9 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8459 = 0%, 29 KB/s], Decompressed: 15
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 26 KB/s], Decompressed: 31
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 25 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 89 KB/s], Decompressed: 93
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 92 KB/s], Decompressed: 124
Downloaded: 169 file(s) [attempted 169/8459 = 1%, 69 KB/s], Decompressed: 165
Downloaded: 208 file(s) [attempted 208/8459 = 2%, 117 KB/s], Decompressed: 203
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 162 KB/s], Decompressed: 240
Downloaded: 286 file(s) [attempted 286/8459 = 3%, 945 KB/s], Decompressed: 278
Downloaded: 323 file(s) [attempted 323/8459 = 3%, 722 KB/s], Decompressed: 316
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 88 KB/s], Decompressed: 353
Downloaded: 401 file(s) [attempted 401/8459 = 4%, 148 KB/s], Decompressed: 398
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 1728 KB/s], Decompressed: 439
Downloaded: 480 file(s) [attempted 480/8459 = 5%, 971 KB/s], Decompressed: 477
Downloaded: 523 file(s) [attempted 523/8459 = 6%, 260 KB/s], Decompressed: 518
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 353 KB/s], Decompressed: 559
Downloaded: 604 file(s) [attempted 604/8459 = 7%, 74 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 88 KB/s], Decompressed: 638
Downloaded: 682 file(s) [attempted 682/8459 = 8%, 566 KB/s], Decompressed: 675
Downloaded: 723 file(s) [attempted 723/8459 = 8%, 455 KB/s], Decompressed: 720
Downloaded: 765 file(s) [attempted 765/8459 = 9%, 221 KB/s], Decompressed: 758
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 689 KB/s], Decompressed: 802
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 94 KB/s], Decompressed: 845
Downloaded: 887 file(s) [attempted 887/8459 = 10%, 211 KB/s], Decompressed: 878
Downloaded: 922 file(s) [attempted 922/8459 = 10%, 462 KB/s], Decompressed: 919
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 342 KB/s], Decompressed: 956
Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 368 KB/s], Decompressed: 1004
Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 113 KB/s], Decompressed: 1045
Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 64 KB/s], Decompressed: 1083
Downloaded: 1131 file(s) [attempted 1131/8459 = 13%, 190 KB/s], Decompressed: 1127
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 269 KB/s], Decompressed: 1165
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 88 KB/s], Decompressed: 1199
Downloaded: 1251 file(s) [attempted 1251/8459 = 14%, 561 KB/s], Decompressed: 1244
Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 785 KB/s], Decompressed: 1281
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 581 KB/s], Decompressed: 1333
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 37 KB/s], Decompressed: 1370
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 402 KB/s], Decompressed: 1408
Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 236 KB/s], Decompressed: 1453
Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 265 KB/s], Decompressed: 1490
Downloaded: 1536 file(s) [attempted 1536/8459 = 18%, 370 KB/s], Decompressed: 1531
Downloaded: 1574 file(s) [attempted 1574/8459 = 18%, 511 KB/s], Decompressed: 1569
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 89 KB/s], Decompressed: 1609
Downloaded: 1654 file(s) [attempted 1654/8459 = 19%, 132 KB/s], Decompressed: 1648
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 294 KB/s], Decompressed: 1685
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 242 KB/s], Decompressed: 1726
Downloaded: 1772 file(s) [attempted 1772/8459 = 20%, 145 KB/s], Decompressed: 1767
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 59 KB/s], Decompressed: 1808
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 25 KB/s], Decompressed: 1850
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 43 KB/s], Decompressed: 1894
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 292 KB/s], Decompressed: 1921
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 841 KB/s], Decompressed: 1963
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 130 KB/s], Decompressed: 2007
Downloaded: 2050 file(s) [attempted 2050/8459 = 24%, 707 KB/s], Decompressed: 2045
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 246 KB/s], Decompressed: 2093
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 757 KB/s], Decompressed: 2130
Downloaded: 2170 file(s) [attempted 2170/8459 = 25%, 1263 KB/s], Decompressed: 2164
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 257 KB/s], Decompressed: 2206
Downloaded: 2251 file(s) [attempted 2251/8459 = 26%, 1127 KB/s], Decompressed: 2247
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 130 KB/s], Decompressed: 2288
Downloaded: 2331 file(s) [attempted 2331/8459 = 27%, 139 KB/s], Decompressed: 2322
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 98 KB/s], Decompressed: 2360
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 44 KB/s], Decompressed: 2404
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 252 KB/s], Decompressed: 2444
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 259 KB/s], Decompressed: 2479
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 681 KB/s], Decompressed: 2524
Downloaded: 2571 file(s) [attempted 2571/8459 = 30%, 630 KB/s], Decompressed: 2565
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 1014 KB/s], Decompressed: 2602
Downloaded: 2644 file(s) [attempted 2644/8459 = 31%, 397 KB/s], Decompressed: 2640
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 808 KB/s], Decompressed: 2681
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 167 KB/s], Decompressed: 2722
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 250 KB/s], Decompressed: 2767
Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 214 KB/s], Decompressed: 2801
Downloaded: 2848 file(s) [attempted 2848/8459 = 33%, 1415 KB/s], Decompressed: 2839
Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 148 KB/s], Decompressed: 2883
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 611 KB/s], Decompressed: 2931
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 22 KB/s], Decompressed: 2972
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 26 KB/s], Decompressed: 3017
Downloaded: 3058 file(s) [attempted 3058/8459 = 36%, 153 KB/s], Decompressed: 3054
Downloaded: 3095 file(s) [attempted 3095/8459 = 36%, 115 KB/s], Decompressed: 3088
Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 373 KB/s], Decompressed: 3133
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 177 KB/s], Decompressed: 3177
Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 162 KB/s], Decompressed: 3222
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 280 KB/s], Decompressed: 3266
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 167 KB/s], Decompressed: 3307
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 426 KB/s], Decompressed: 3346
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 90 KB/s], Decompressed: 3383
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 481 KB/s], Decompressed: 3427
Downloaded: 3477 file(s) [attempted 3477/8459 = 41%, 786 KB/s], Decompressed: 3472
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 943 KB/s], Decompressed: 3509
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 88 KB/s], Decompressed: 3544
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 74 KB/s], Decompressed: 3585
Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 328 KB/s], Decompressed: 3633
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 116 KB/s], Decompressed: 3670
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 85 KB/s], Decompressed: 3711
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 45 KB/s], Decompressed: 3742
Downloaded: 3793 file(s) [attempted 3793/8459 = 44%, 165 KB/s], Decompressed: 3790
Downloaded: 3840 file(s) [attempted 3840/8459 = 45%, 332 KB/s], Decompressed: 3835
Downloaded: 3880 file(s) [attempted 3880/8459 = 45%, 27 KB/s], Decompressed: 3872
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 1648 KB/s], Decompressed: 3910
Downloaded: 3952 file(s) [attempted 3952/8459 = 46%, 322 KB/s], Decompressed: 3947
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 180 KB/s], Decompressed: 3992
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 105 KB/s], Decompressed: 4036
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 62 KB/s], Decompressed: 4079
Downloaded: 4117 file(s) [attempted 4117/8459 = 48%, 102 KB/s], Decompressed: 4112
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 51 KB/s], Decompressed: 4149
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 320 KB/s], Decompressed: 4190
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 254 KB/s], Decompressed: 4235
Downloaded: 4283 file(s) [attempted 4283/8459 = 50%, 267 KB/s], Decompressed: 4279
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 790 KB/s], Decompressed: 4317
Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 29 KB/s], Decompressed: 4358
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 598 KB/s], Decompressed: 4392
Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 259 KB/s], Decompressed: 4437
Downloaded: 4482 file(s) [attempted 4482/8459 = 52%, 433 KB/s], Decompressed: 4475
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 23 KB/s], Decompressed: 4519
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 479 KB/s], Decompressed: 4557
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 22 KB/s], Decompressed: 4594
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 69 KB/s], Decompressed: 4629
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 139 KB/s], Decompressed: 4673
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 674 KB/s], Decompressed: 4721
Downloaded: 4766 file(s) [attempted 4766/8459 = 56%, 702 KB/s], Decompressed: 4759
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 409 KB/s], Decompressed: 4800
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 195 KB/s], Decompressed: 4834
Downloaded: 4879 file(s) [attempted 4879/8459 = 57%, 122 KB/s], Decompressed: 4875
Downloaded: 4923 file(s) [attempted 4923/8459 = 58%, 162 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 244 KB/s], Decompressed: 4961
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 130 KB/s], Decompressed: 5002
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 161 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 144 KB/s], Decompressed: 5080
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 298 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 430 KB/s], Decompressed: 5159
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 93 KB/s], Decompressed: 5200
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 240 KB/s], Decompressed: 5241
Downloaded: 5292 file(s) [attempted 5292/8459 = 62%, 602 KB/s], Decompressed: 5289
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 44 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 786 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 229 KB/s], Decompressed: 5405
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 353 KB/s], Decompressed: 5446
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 320 KB/s], Decompressed: 5488
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 575 KB/s], Decompressed: 5529
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 857 KB/s], Decompressed: 5570
Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 132 KB/s], Decompressed: 5607
Downloaded: 5652 file(s) [attempted 5652/8459 = 66%, 1418 KB/s], Decompressed: 5648
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 111 KB/s], Decompressed: 5694
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 203 KB/s], Decompressed: 5731
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 101 KB/s], Decompressed: 5775
Downloaded: 5821 file(s) [attempted 5821/8459 = 68%, 110 KB/s], Decompressed: 5813
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 602 KB/s], Decompressed: 5850
Downloaded: 5898 file(s) [attempted 5898/8459 = 69%, 994 KB/s], Decompressed: 5891
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 57 KB/s], Decompressed: 5936
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 199 KB/s], Decompressed: 5977
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 284 KB/s], Decompressed: 6019
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 142 KB/s], Decompressed: 6052
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 177 KB/s], Decompressed: 6090
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 87 KB/s], Decompressed: 6134
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 143 KB/s], Decompressed: 6175
Downloaded: 6220 file(s) [attempted 6220/8459 = 73%, 484 KB/s], Decompressed: 6213
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 83 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 731 KB/s], Decompressed: 6288
Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 36 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 91 KB/s], Decompressed: 6374
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 189 KB/s], Decompressed: 6415
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 293 KB/s], Decompressed: 6456
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 74 KB/s], Decompressed: 6495
Downloaded: 6542 file(s) [attempted 6542/8459 = 77%, 953 KB/s], Decompressed: 6538
Downloaded: 6582 file(s) [attempted 6582/8459 = 77%, 353 KB/s], Decompressed: 6576
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 87 KB/s], Decompressed: 6617
Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 73 KB/s], Decompressed: 6658
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 93 KB/s], Decompressed: 6696
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 861 KB/s], Decompressed: 6733
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 25 KB/s], Decompressed: 6778
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 229 KB/s], Decompressed: 6819
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 113 KB/s], Decompressed: 6860
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 496 KB/s], Decompressed: 6894
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 448 KB/s], Decompressed: 6935
Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 332 KB/s], Decompressed: 6980
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 100 KB/s], Decompressed: 7021
Downloaded: 7063 file(s) [attempted 7063/8459 = 83%, 158 KB/s], Decompressed: 7058
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 974 KB/s], Decompressed: 7099
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 444 KB/s], Decompressed: 7137
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 87 KB/s], Decompressed: 7178
Downloaded: 7221 file(s) [attempted 7221/8459 = 85%, 577 KB/s], Decompressed: 7216
Downloaded: 7260 file(s) [attempted 7260/8459 = 85%, 632 KB/s], Decompressed: 7257
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 28 KB/s], Decompressed: 7298
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 56 KB/s], Decompressed: 7336
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 39 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 216 KB/s], Decompressed: 7414
Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 322 KB/s], Decompressed: 7459
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 152 KB/s], Decompressed: 7496
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 159 KB/s], Decompressed: 7531
Downloaded: 7577 file(s) [attempted 7577/8459 = 89%, 907 KB/s], Decompressed: 7568
Downloaded: 7615 file(s) [attempted 7615/8459 = 90%, 509 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 459 KB/s], Decompressed: 7654
Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 47 KB/s], Decompressed: 7695
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 118 KB/s], Decompressed: 7729
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 173 KB/s], Decompressed: 7767
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 121 KB/s], Decompressed: 7808
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 303 KB/s], Decompressed: 7846
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 645 KB/s], Decompressed: 7889
Downloaded: 7926 file(s) [attempted 7926/8459 = 93%, 674 KB/s], Decompressed: 7917
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 80 KB/s], Decompressed: 7958
Downloaded: 8002 file(s) [attempted 8002/8459 = 94%, 48 KB/s], Decompressed: 7996
Downloaded: 8041 file(s) [attempted 8041/8459 = 95%, 189 KB/s], Decompressed: 8037
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 321 KB/s], Decompressed: 8075
Downloaded: 8112 file(s) [attempted 8112/8459 = 95%, 656 KB/s], Decompressed: 8102
Downloaded: 8149 file(s) [attempted 8149/8459 = 96%, 123 KB/s], Decompressed: 8143
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 38 KB/s], Decompressed: 8181
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 425 KB/s], Decompressed: 8215
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 78 KB/s], Decompressed: 8249
Downloaded: 8298 file(s) [attempted 8298/8459 = 98%, 590 KB/s], Decompressed: 8290
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 438 KB/s], Decompressed: 8335
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 339 KB/s], Decompressed: 8379
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 61 KB/s], Decompressed: 8423
Downloaded: 8457 file(s) [attempted 8457/8459 = 99%, 513 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 513 KB/s], Decompressed: 8455

lake build

✔ [2068/2071] Built PrimeNumberTheoremAnd.Auxiliary (23s)
✔ [2776/2792] Built PrimeNumberTheoremAnd.Sobolev (15s)
✔ [2832/2838] Built PrimeNumberTheoremAnd.Fourier (3.0s)
✔ [2872/2892] Built PrimeNumberTheoremAnd.Defs (4.4s)
✔ [3455/3467] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (2.2s)
✔ [3457/3468] Built PrimeNumberTheoremAnd.Rectangle (3.4s)
✔ [3461/3469] Built PrimeNumberTheoremAnd.EulerMaclaurin (2.7s)
✔ [3463/3469] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.4s)
✔ [3465/3474] Built PrimeNumberTheoremAnd.ZetaConj (3.0s)
✔ [3467/3474] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (6.7s)
✔ [3468/3474] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (10s)
✔ [3470/3474] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (2.8s)
✔ [3472/3476] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.8s)
✔ [3473/3481] Built PrimeNumberTheoremAnd.ZetaBounds (18s)
✔ [3479/3482] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (3.4s)
✔ [3481/3497] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (2.6s)
✔ [3484/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.3s)
✔ [3486/3499] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (2.1s)
✔ [3488/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (2.0s)
✔ [3489/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (2.2s)
✔ [3490/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (2.1s)
✔ [3491/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (3.2s)
✔ [3492/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (2.9s)
✔ [3493/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (4.3s)
✔ [3494/3501] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.9s)
✔ [3495/3501] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.0s)
✔ [3497/3503] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.0s)
✔ [3499/3503] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.4s)
✔ [3501/3516] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (2.0s)
✔ [3521/3540] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (1.8s)
✔ [3522/3540] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (1.9s)
✔ [3524/3542] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (2.5s)
✔ [3526/3542] Built PrimeNumberTheoremAnd.MellinCalculus (7.8s)
✔ [3527/3542] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.3s)
✔ [3529/3543] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (1.5s)
✔ [3531/3543] Built PrimeNumberTheoremAnd.SmoothExistence (3.0s)
✔ [3533/3544] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (1.9s)
ℹ [3537/3548] Built PrimeNumberTheoremAnd.MediumPNT (27s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3544/3551] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (2.2s)
✔ [3546/3551] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (4.0s)
✔ [3548/3551] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (3.8s)
✔ [3550/3561] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (18s)
✔ [3554/3566] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (1.9s)
✔ [3558/3567] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (3.1s)
✔ [3560/3567] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (3.0s)
✔ [3562/3570] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (5.4s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (12s)
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`
✔ [3565/3571] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (2.0s)
✔ [3566/3572] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.0s)
✔ [3569/3579] Built PrimeNumberTheoremAnd.BrunTitchmarsh (3.8s)
⚠ [3697/3700] Built PrimeNumberTheoremAnd.Wiener (25s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3699/3711] Built PrimeNumberTheoremAnd.Consequences (27s)
✔ [3805/3817] Built PrimeNumberTheoremAnd.IEANTN.LogTables (27s)
✔ [3807/3817] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.2s)
✔ [3808/3817] Built PrimeNumberTheoremAnd.HadamardFactorization (1.0s)
✔ [3809/3817] Built PrimeNumberTheoremAnd.HoffsteinLockhart (2.1s)
✔ [3810/3817] Built PrimeNumberTheoremAnd.IEANTN.KLN (2.8s)
⚠ [3811/3818] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (2.4s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3814/3819] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (1.8s)
⚠ [3816/3819] 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`
✔ [3817/3834] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (8.7s)
✔ [3874/3890] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.4s)
✔ [3879/3890] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (6.0s)
⚠ [3880/3890] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (45s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3882/3892] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (17s)
⚠ [3883/3893] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (2.5s)
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`
✔ [3884/3893] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (7.3s)
✔ [3886/3894] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.1s)
✔ [3887/3895] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.5s)
✔ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (5.7s)
⚠ [3892/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.3s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3894/3913] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.6s)
⚠ [4013/4022] 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`
✔ [4016/4022] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (46s)
✔ [4017/4025] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (2.2s)
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (13s)
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`
✔ [4019/4026] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (89s)
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4023/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (26s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4033/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (4.6s)
✔ [4036/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.6s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (64s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (37s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (38s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (38s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (39s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (39s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (39s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (40s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (38s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (38s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (38s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (37s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.5s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.5s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (44s)
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.
✔ [4057/4068] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.6s)
✔ [4058/4070] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (2.4s)
✔ [4059/4075] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (59s)
⚠ [4060/4075] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (12s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4062/4075] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (20s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4064/4075] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (38s)
⚠ [4066/4075] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (51s)
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:3776:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4432:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4454:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4481:8: declaration uses `sorry`
✔ [4067/4075] Built PrimeNumberTheoremAnd.Tactic.Simprocs (1.8s)
✔ [4069/4076] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (14s)
⚠ [4070/4076] Built PrimeNumberTheoremAnd.IEANTN.Dusart (17s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4072/4077] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.5s)
✔ [4074/4078] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (44s)
✔ [4076/4083] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (18s)
⚠ [4087/4097] 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`
✔ [4089/4097] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax (1.8s)
✔ [4090/4097] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (6.1s)
✔ [4092/4133] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.3s)
✔ [4093/4133] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (2.0s)
✔ [4095/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound (1.6s)
✔ [4096/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory (2.1s)
✔ [4097/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (1.8s)
✔ [4098/4133] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation (1.8s)
✔ [4099/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic (1.7s)
✔ [4100/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric (1.7s)
✔ [4101/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds (1.8s)
✔ [4102/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds (3.2s)
✔ [4103/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux (1.9s)
✔ [4104/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (1.9s)
✔ [4105/4133] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta (2.4s)
✔ [4106/4133] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex (2.0s)
✔ [4107/4133] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn (1.7s)
✔ [4108/4133] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring (1.2s)
✔ [4109/4133] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (1.6s)
✔ [4110/4133] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (1.9s)
⚠ [4111/4141] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (13s)
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`
✔ [4114/4141] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly (7.7s)
✔ [4115/4141] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi (1.8s)
✔ [4116/4141] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds (5.3s)
✔ [4117/4141] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (1.9s)
⚠ [4118/4141] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
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/4147] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (2.7s)
✔ [4122/4147] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
✔ [4124/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth (3.7s)
✔ [4125/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel (2.6s)
⚠ [4126/4154] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4127/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues (2.4s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4130/4154] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (4.8s)
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`
✔ [4131/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (2.3s)
✔ [4132/4154] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.5s)
✔ [4133/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound (4.8s)
✔ [4135/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral (1.7s)
✔ [4136/4154] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy (1.5s)
✔ [4137/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum (2.7s)
✔ [4139/4154] Built PrimeNumberTheoremAnd.PerronFormula (5.9s)
✔ [4140/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound (10s)
✔ [4141/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound (2.5s)
✔ [4142/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition (1.5s)
✔ [4143/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation (2.6s)
ℹ [4144/4154] 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.
✔ [4145/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth (4.6s)
✔ [4146/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity (2.4s)
✔ [4147/4154] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (52s)
✔ [4148/4154] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order (2.2s)
✔ [4149/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound (1.8s)
✔ [4150/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder (13s)
✔ [4151/4154] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard (3.1s)
⚠ [4152/4154] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4153/4154] Built PrimeNumberTheoremAnd (2.8s)
Build completed successfully (4154 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

✔ [14/35] Built Batteries.Lean.NameMapAttribute:c.o (762ms)
✔ [26/35] Built Cli.Basic:c.o (3.3s)
✔ [31/35] Built Cli.Extensions:c.o (501ms)
✔ [32/35] Built Cli:c.o (63ms)
✔ [2100/2109] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (3.5s)
✔ [2810/2823] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.3s)
✔ [2865/2875] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.4s)
✔ [2897/2910] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (9.0s)
✔ [3485/3501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (1.0s)
✔ [3486/3501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.0s)
✔ [3491/3501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMaclaurin:blueprint (2.3s)
✔ [3496/3509] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (12s)
✔ [3497/3509] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.4s)
✔ [3502/3511] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (10s)
✔ [3503/3511] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (12s)
✔ [3506/3518] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.2s)
✔ [3507/3518] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (1.8s)
✔ [3509/3544] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (61s)
✔ [3517/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (2.2s)
✔ [3520/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.3s)
✔ [3522/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.3s)
✔ [3527/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (1.0s)
✔ [3529/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.6s)
✔ [3530/3551] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.3s)
✔ [3533/3551] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.2s)
✔ [3534/3551] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.2s)
✔ [3537/3553] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.2s)
✔ [3540/3557] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.2s)
✔ [3543/3559] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.3s)
✔ [3548/3562] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.3s)
✔ [3552/3566] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.3s)
✔ [3556/3566] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.2s)
✔ [3561/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.3s)
✔ [3577/3605] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (1.9s)
✔ [3578/3605] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic:blueprint (2.2s)
✔ [3579/3605] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic:blueprint (1.9s)
✔ [3584/3607] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog:blueprint (1.9s)
✔ [3586/3607] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (23s)
✔ [3587/3607] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (1.2s)
✔ [3591/3610] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (1.9s)
✔ [3592/3610] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (3.0s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3598/3614] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (58s)
✔ [3605/3614] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (2.3s)
✔ [3608/3614] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth:blueprint (2.3s)
✔ [3611/3628] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (2.3s)
✔ [3614/3637] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (2.5s)
✔ [3619/3637] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.8s)
✔ [3624/3641] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.3s)
✔ [3626/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.3s)
⚠ [3629/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`
✔ [3631/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (47s)
✔ [3633/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.2s)
✔ [3637/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.4s)
✔ [3638/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (2.4s)
✔ [3642/3653] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.3s)
⚠ [3764/3773] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3768/3773] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (35s)
✔ [3771/3783] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (13s)
✔ [3880/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.4s)
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3887/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.6s)
✔ [3888/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.1s)
✔ [3889/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (2.3s)
✔ [3890/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (2.5s)
✔ [3891/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (2.6s)
⚠ [3895/3901] 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`
✔ [3896/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.1s)
✔ [3899/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.3s)
✔ [3900/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (34s)
✔ [3958/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.3s)
⚠ [3963/3985] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3964/3985] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3966/3985] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.0s)
✔ [3967/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [3968/3987] 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`
✔ [3970/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.3s)
✔ [3974/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.3s)
✔ [3975/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.2s)
✔ [3977/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.0s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.7s)
⚠ [3982/3990] 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`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.2s)
✔ [3988/3996] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.3s)
⚠ [4107/4122] 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`
✔ [4109/4122] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.0s)
✔ [4112/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (2.3s)
⚠ [4113/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (2.7s)
⚠ [4115/4126] 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`
✔ [4119/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4120/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4121/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.5s)
⚠ [4122/4177] 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`
✔ [4125/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (23s)
✔ [4137/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.7s)
✔ [4139/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.8s)
ℹ [4157/4200] 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.
✔ [4161/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.8s)
✔ [4162/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.8s)
✔ [4164/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (2.8s)
✔ [4165/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.8s)
✔ [4166/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.8s)
✔ [4167/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (2.8s)
✔ [4168/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (2.8s)
✔ [4169/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.8s)
✔ [4170/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (2.8s)
✔ [4171/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (2.8s)
✔ [4172/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (2.8s)
✔ [4173/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.8s)
✔ [4174/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (2.8s)
✔ [4175/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.8s)
✔ [4176/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (2.8s)
✔ [4177/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.7s)
✔ [4178/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (2.8s)
✔ [4179/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (50s)
⚠ [4180/4208] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
✔ [4182/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.2s)
✔ [4183/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.3s)
⚠ [4184/4208] 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`
⚠ [4187/4209] 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:3776:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4432:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4454:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4481:8: declaration uses `sorry`
✔ [4190/4209] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (18s)
✔ [4192/4209] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.1s)
⚠ [4193/4209] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4195/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (2.8s)
✔ [4197/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (30s)
✔ [4198/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.3s)
✔ [4200/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.8s)
✔ [4202/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (17s)
✔ [4203/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4206/4213] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.9s)
✔ [4208/4213] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4211/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (12s)
⚠ [4219/4238] 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`
✔ [4222/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (2.6s)
✔ [4225/4303] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.0s)
✔ [4228/4303] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax:blueprint (2.2s)
✔ [4229/4306] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (2.8s)
⚠ [4230/4306] 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`
✔ [4249/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (43s)
⚠ [4250/4331] 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`
✔ [4251/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (2.5s)
✔ [4253/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound:blueprint (1.9s)
✔ [4254/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory:blueprint (2.2s)
✔ [4256/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.1s)
✔ [4257/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation:blueprint (2.3s)
✔ [4259/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic:blueprint (1.9s)
✔ [4260/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric:blueprint (1.7s)
✔ [4261/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds:blueprint (2.2s)
✔ [4262/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds:blueprint (2.2s)
✔ [4263/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux:blueprint (2.2s)
✔ [4265/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (1.9s)
✔ [4266/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta:blueprint (2.3s)
✔ [4267/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex:blueprint (1.9s)
✔ [4268/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn:blueprint (2.1s)
✔ [4270/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring:blueprint (1.4s)
✔ [4271/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic:blueprint (2.2s)
✔ [4272/4331] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.3s)
✔ [4278/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.3s)
⚠ [4279/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4280/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly:blueprint (2.2s)
✔ [4282/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi:blueprint (2.3s)
✔ [4283/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds:blueprint (2.3s)
✔ [4284/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals:blueprint (2.2s)
✔ [4287/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.2s)
⚠ [4290/4343] 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`
✔ [4293/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4295/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.7s)
✔ [4296/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth:blueprint (2.2s)
✔ [4297/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel:blueprint (2.5s)
✔ [4302/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues:blueprint (2.4s)
✔ [4303/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4305/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (43s)
✔ [4306/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (2.2s)
✔ [4308/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound:blueprint (2.2s)
✔ [4311/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.7s)
✔ [4312/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum:blueprint (2.5s)
✔ [4315/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral:blueprint (2.2s)
✔ [4316/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy:blueprint (1.5s)
ℹ [4317/4343] 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.
✔ [4318/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4319/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound:blueprint (2.2s)
✔ [4320/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound:blueprint (2.2s)
✔ [4322/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation:blueprint (2.5s)
✔ [4324/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition:blueprint (2.0s)
✔ [4325/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.5s)
✔ [4327/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth:blueprint (2.3s)
✔ [4329/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity:blueprint (2.6s)
✔ [4331/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4332/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order:blueprint (2.4s)
✔ [4333/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound:blueprint (2.5s)
✔ [4335/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder:blueprint (2.6s)
✔ [4337/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard:blueprint (2.5s)
⚠ [4338/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4339/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (43s)
✔ [4341/4344] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (2.0s)
ℹ [4342/4344] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (56ms)
info: Blueprint indexing
Build completed successfully (4344 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-batch-00000)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: restored compiled static runner cache ce08cfbc68b3c704bd199132616b9e6d73946aa53a97fa72dbdaca18e17279fb
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-batch-00001)

lean semantic helper: restored compiled static runner cache a9be9aa136ac0e1b9ed39ca9fe3c6732a14c79aca987bd52e0d55b84e59ae3cf
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-batch-00002)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 744bdec20dce2ae1d24f8100f626352578134d446fbd890303323aa8524a32d3
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-batch-00003)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache cd7df8059fc53e349d3b16a4ed3cbe65cd1d95867fd85ce82db010a5e020a387
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-batch-00004)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 8340c994884d9ec363c8115cdf3c012c462cc112cf5a86bd627ed6b209a12848
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-batch-00005)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f483e8ae66d0e1e493c5cc3b48aeee5dadaec557b99a21ae2f76087db38b712f
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-batch-00006)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 5e35e8f6c9cd05cda796897621da4b4b57f31ee0a1ab6eb9957b6b91e470ffe8
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-batch-00007)

lean semantic helper: restored compiled static runner cache 5666eae891aeab65bd5ad432f84b37f48db41c323a6f2b00af7d1f099827a90b
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-batch-00008)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 482423e877ad6d6341a3f05d1d4afc417588cdb3db1a30f222694f16b7812ed7
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-batch-00009)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 950045d13a3d5d8f522468ac1e77ce3e6b894549630e733f55410a92722b854f
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-batch-00010)

lean semantic helper: restored compiled static runner cache 88183adc2abdc93ea067efe341db50508af07c274227d414974d67492b987e67
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-batch-00011)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache c35673243f2c909edfd66d0b957d099d912a8fa0d1c5d23ddd003da9645307b3
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-batch-00012)

lean semantic helper: restored compiled static runner cache 28cc804c2c409928e543314dc6285286d9a58eb890b02bb428cc905a26b2c0ea
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-batch-00013)

lean semantic helper: restored compiled static runner cache 072f3d61ff56d4706cc08239f26fb8a8cff3d9ba6af06b40abaeaf3323230dcf
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-batch-00014)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache dbf7d7e2e825262875da71990374cfc6f168a8221187b86ba45cc12556a2b31f
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-batch-00015)

lean semantic helper: restored compiled static runner cache 4f76707c7bd8fb40a22db985004cd4bee289f16058b8005fced32e61b9a891bd
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-batch-00016)

lean semantic helper: restored compiled static runner cache d3e9f82b516bfd9520e22152d1729dd54389a35a0acbb74e04622e20d8019f49
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-batch-00017)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 21be504c87a4f233b76696f65c0e0e67bef18a878044660c4adce75ef3c97dca
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-batch-00018)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache b2188d643ba615d7c742f5b8a6507772b18f2f196e35b435a7fda346413737ff
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-batch-00019)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 4338c0d848ddeeb159dfc7743e677826e9e7cfceb734381ea06fa1b679f4d1f1
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-batch-00020)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 8bd615edeea202b617369b789c309ca97f60d3f95c0b40ff2a23b9350b4de767
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-batch-00021)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 5e98ad5d0453c2826252bf2b4549eb250425081c057ea9169014477d232b0715
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-batch-00022)

lean semantic helper: restored compiled static runner cache b4760a95cb83f6f313e92d0899f90c0a9d398820352e08241a61c6ea77ad4d37
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-batch-00023)

lean semantic helper: restored compiled static runner cache 395e475866a73f2ae513581b343de5074d6f70f10184712f6182dd2fdd60b0e3
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-batch-00024)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 2c4ebe70f0784820b76e5a5d46c1c0bde25754d1964f2b384d42b8a06c17015f
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-batch-00025)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 91a4fcb48014ba08c1da96392a32aac8af683e0ab1f9de42c66df7d015eb2542
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-batch-00026)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 00a66635e15e631793044310d8e66dc5b40d1b57c44063095b67dc7508ce09a8
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-batch-00027)

lean semantic helper: restored compiled static runner cache a435981e9150db1553b61dc1c48337081a4863cbc469b5864f2c22b0a45c3466
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-batch-00028)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache c3f68166261cc2362baad7eea0e87c08dcbde0e84f8def35f148cab3216fba95
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-batch-00029)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 8366ac4cfc9366bc80ec48532403e0883cd91c92836ad10816c4a2616818dba8
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-batch-00030)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache b256fcf0090442a3ffd8291e0e7a2fd4ab8ff646ce2d518e5c332406f5f59849
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-batch-00031)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 773c22356d1b1366800fd97979d7126b87a291cbfcc4afccf9dc9d5e700aa480
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-batch-00032)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f15fc90061f26aa0d12e4d55db2770c32247f19f662d8ce20631e9775f088fde
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-batch-00033)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f01fd7f29d763b6c0e3a5f197714c52b1242d0bdc732ba7ecdfdd31e69e90c32
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-batch-00034)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 5f517032b349e4e63ef0ab0da010d126c6f815f4916ab758e6f541b19080aa1e
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-batch-00035)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache ea07a3930ef9e37daf86ba36be6e1210762f2b8df2cd47509f73136819855a2a
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-batch-00036)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 70e4eadf84337047aca3c82de9674afe5c6fd430342a47587df309c780f5430a
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-batch-00037)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 5b688503de843889b1cdcf858d0e36cd523e3fddcc32346ba8798b64913b88e3
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-batch-00038)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache dacf8a438e590601b15bceb4d33b8adb67df0a3051d1928442eb33708083e1bc
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-batch-00039)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 66223362b492db8a20926ac378acf319baa7cb9727bc7ac95608aa2fa495902d
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-batch-00040)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache c39f7fac0c670abce7873140878baa294d20fe5ec628f79adfb6a07c7fd7943e
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-batch-00041)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 892e79888f251d462a455f62e25f5549133419a234c5e81198919850861468e3
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-batch-00042)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 0d231c2b8e654a5061f51c1efa2a96dcff896a342dbfa9428ee44f39e29bb5db
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-batch-00043)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 4284333fe3aa5053b89d3e06da5ef9df1c7f99406694b7effa2014e36f0e1818
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-batch-00044)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f77db45b040ecf12021678ae350505b3e93d65bb31da65792e08bea78c32bf57
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-batch-00045)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 23331131a4ae2856e732fc446551024cbaaa56019be6b9912e5f08695b6a42e9
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-batch-00046)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 6329d9e78e040e6a2deb01fcaeeff6d7b80c91a229b0ed4a60c5635918d1ada3
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-batch-00047)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 36b3228d7e5ddeaa77dff4ffaefdc2b9c3f9e70ba8fbd473cd2c647d056878e7
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-batch-00048)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache e0270fe1c03f4c9f9750cadccb93bc7fbd9c75adbe71858e21c34d350ac9ee6a
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-batch-00049)

lean semantic helper: restored compiled static runner cache 9b71e2dc3b5c16d5ff9f4e8c5755aea74240d14c40b8cc48dc055357372577e3
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-batch-00050)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache a124be37984f8f731bdee6e8a3eecdd5aef328658a2177649ef94721fc37a198
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-batch-00051)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache bb70289b1883006264157136ea01bf190c43e7e99cc4710ca867bddeed8f194b
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-batch-00052)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 10af634c8876c4f97df3b0d201853cf628a5c1b320c62cdf30dec07749419de2
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-batch-00053)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache e52c735f13b139713c7685064d07088e810afcc30684e4d2f6904de959e60afd
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-batch-00054)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache fa5a47cf823ec938f9e1ce5186e19271cb9901f9e7559e0532d103a9447cd446
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-batch-00055)

lean semantic helper: restored compiled static runner cache 65d02e0b45322095024ccee30e0f39a2caf4226f61fb72d40d12181c0886960a
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-batch-00056)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache b2e38b78e637de63c954ade1fd9829d69db46590c39f0901cb05c2614cd0181b
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-batch-00057)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache b5c360e5dc61351059cd81ccace4aa5eea1b13ec3777e7294cf8057d33f4b6f2
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-batch-00058)

lean semantic helper: restored compiled static runner cache 90f3fc0f5c7381426e827cb32c9c2b80a878b4d83d4cf63860fc79351d390e0f
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-batch-00059)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 0c895e2bd97087267a376c74a0a43a4a39c43d4d581c2491778b22d717faf1d7
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-batch-00060)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache c64120e3edcef0e3488a04c70e791df08f193556d5c0d06993d0a1cfeeaca11f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes