Run 56

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

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

git checkout ecbab15576d09a0197c70668e0765c66a0552e26

fatal: reference is not a tree: ecbab15576d09a0197c70668e0765c66a0552e26

git fetch --depth 1 origin ecbab15576d09a0197c70668e0765c66a0552e26

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

git checkout ecbab15576d09a0197c70668e0765c66a0552e26 (after fetch)

Note: switching to 'ecbab15576d09a0197c70668e0765c66a0552e26'.

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 ecbab15 feat(Hadamard): prereqs for Hadamard factorization part1 (#1496)

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%, 8 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 3 KB/s], Decompressed: 13
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 20 KB/s], Decompressed: 30
Downloaded: 61 file(s) [attempted 61/8459 = 0%, 51 KB/s], Decompressed: 56
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 153 KB/s], Decompressed: 61
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 509 KB/s], Decompressed: 61
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 85 KB/s], Decompressed: 68
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 658 KB/s], Decompressed: 179
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 597 KB/s], Decompressed: 227
Downloaded: 266 file(s) [attempted 266/8459 = 3%, 141 KB/s], Decompressed: 261
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 76 KB/s], Decompressed: 302
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 22 KB/s], Decompressed: 343
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 56 KB/s], Decompressed: 384
Downloaded: 427 file(s) [attempted 427/8459 = 5%, 1095 KB/s], Decompressed: 415
Downloaded: 464 file(s) [attempted 464/8459 = 5%, 825 KB/s], Decompressed: 460
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 140 KB/s], Decompressed: 497
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 174 KB/s], Decompressed: 535
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 786 KB/s], Decompressed: 576
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 336 KB/s], Decompressed: 624
Downloaded: 672 file(s) [attempted 672/8459 = 7%, 238 KB/s], Decompressed: 665
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 290 KB/s], Decompressed: 703
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 213 KB/s], Decompressed: 747
Downloaded: 796 file(s) [attempted 796/8459 = 9%, 1506 KB/s], Decompressed: 785
Downloaded: 830 file(s) [attempted 830/8459 = 9%, 583 KB/s], Decompressed: 826
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 36 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 623 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 317 KB/s], Decompressed: 939
Downloaded: 991 file(s) [attempted 991/8459 = 11%, 232 KB/s], Decompressed: 984
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 932 KB/s], Decompressed: 1025
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 222 KB/s], Decompressed: 1066
Downloaded: 1114 file(s) [attempted 1114/8459 = 13%, 82 KB/s], Decompressed: 1097
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 312 KB/s], Decompressed: 1148
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 924 KB/s], Decompressed: 1186
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 94 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 266 KB/s], Decompressed: 1268
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 46 KB/s], Decompressed: 1309
Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 134 KB/s], Decompressed: 1340
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 106 KB/s], Decompressed: 1346
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 378 KB/s], Decompressed: 1346
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 25 KB/s], Decompressed: 1466
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 977 KB/s], Decompressed: 1511
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 258 KB/s], Decompressed: 1538
Downloaded: 1584 file(s) [attempted 1584/8459 = 18%, 284 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1555 KB/s], Decompressed: 1624
Downloaded: 1674 file(s) [attempted 1674/8459 = 19%, 119 KB/s], Decompressed: 1665
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 192 KB/s], Decompressed: 1699
Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 966 KB/s], Decompressed: 1740
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 1097 KB/s], Decompressed: 1778
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 255 KB/s], Decompressed: 1822
Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 264 KB/s], Decompressed: 1863
Downloaded: 1911 file(s) [attempted 1911/8459 = 22%, 111 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 756 KB/s], Decompressed: 1945
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 75 KB/s], Decompressed: 1980
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 409 KB/s], Decompressed: 2017
Downloaded: 2064 file(s) [attempted 2064/8459 = 24%, 126 KB/s], Decompressed: 2058
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 331 KB/s], Decompressed: 2093
Downloaded: 2141 file(s) [attempted 2141/8459 = 25%, 925 KB/s], Decompressed: 2130
Downloaded: 2173 file(s) [attempted 2173/8459 = 25%, 1266 KB/s], Decompressed: 2164
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 187 KB/s], Decompressed: 2209
Downloaded: 2255 file(s) [attempted 2255/8459 = 26%, 385 KB/s], Decompressed: 2243
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 375 KB/s], Decompressed: 2284
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 285 KB/s], Decompressed: 2325
Downloaded: 2370 file(s) [attempted 2370/8459 = 28%, 307 KB/s], Decompressed: 2366
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 288 KB/s], Decompressed: 2394
Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 96 KB/s], Decompressed: 2394
Downloaded: 2483 file(s) [attempted 2483/8459 = 29%, 269 KB/s], Decompressed: 2404
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 686 KB/s], Decompressed: 2517
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 683 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 113 KB/s], Decompressed: 2592
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 36 KB/s], Decompressed: 2633
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 208 KB/s], Decompressed: 2676
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 1137 KB/s], Decompressed: 2712
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 191 KB/s], Decompressed: 2750
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1182 KB/s], Decompressed: 2791
Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 210 KB/s], Decompressed: 2832
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 58 KB/s], Decompressed: 2873
Downloaded: 2915 file(s) [attempted 2915/8459 = 34%, 48 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 40 KB/s], Decompressed: 2955
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 95 KB/s], Decompressed: 2996
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 282 KB/s], Decompressed: 3037
Downloaded: 3079 file(s) [attempted 3079/8459 = 36%, 888 KB/s], Decompressed: 3071
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 34 KB/s], Decompressed: 3116
Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 408 KB/s], Decompressed: 3157
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 513 KB/s], Decompressed: 3195
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 196 KB/s], Decompressed: 3236
Downloaded: 3280 file(s) [attempted 3280/8459 = 38%, 242 KB/s], Decompressed: 3273
Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 861 KB/s], Decompressed: 3307
Downloaded: 3357 file(s) [attempted 3357/8459 = 39%, 223 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 49 KB/s], Decompressed: 3390
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 401 KB/s], Decompressed: 3427
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 664 KB/s], Decompressed: 3468
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 277 KB/s], Decompressed: 3506
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 208 KB/s], Decompressed: 3550
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 24 KB/s], Decompressed: 3581
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 1554 KB/s], Decompressed: 3626
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 200 KB/s], Decompressed: 3667
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 164 KB/s], Decompressed: 3708
Downloaded: 3749 file(s) [attempted 3749/8459 = 44%, 640 KB/s], Decompressed: 3739
Downloaded: 3788 file(s) [attempted 3788/8459 = 44%, 410 KB/s], Decompressed: 3780
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 1132 KB/s], Decompressed: 3821
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 249 KB/s], Decompressed: 3859
Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 20 KB/s], Decompressed: 3906
Downloaded: 3944 file(s) [attempted 3944/8459 = 46%, 93 KB/s], Decompressed: 3941
Downloaded: 3982 file(s) [attempted 3982/8459 = 47%, 375 KB/s], Decompressed: 3971
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 632 KB/s], Decompressed: 4009
Downloaded: 4058 file(s) [attempted 4058/8459 = 47%, 1876 KB/s], Decompressed: 4050
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 74 KB/s], Decompressed: 4078
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 165 KB/s], Decompressed: 4078
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 303 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 1209 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 189 KB/s], Decompressed: 4249
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 910 KB/s], Decompressed: 4293
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 63 KB/s], Decompressed: 4327
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 172 KB/s], Decompressed: 4368
Downloaded: 4408 file(s) [attempted 4408/8459 = 52%, 108 KB/s], Decompressed: 4403
Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 97 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 225 KB/s], Decompressed: 4488
Downloaded: 4528 file(s) [attempted 4528/8459 = 53%, 449 KB/s], Decompressed: 4522
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 34 KB/s], Decompressed: 4553
Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 22 KB/s], Decompressed: 4591
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 110 KB/s], Decompressed: 4639
Downloaded: 4685 file(s) [attempted 4685/8459 = 55%, 92 KB/s], Decompressed: 4676
Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 1543 KB/s], Decompressed: 4714
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 711 KB/s], Decompressed: 4731
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 285 KB/s], Decompressed: 4731
Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 228 KB/s], Decompressed: 4817
Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 222 KB/s], Decompressed: 4878
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 920 KB/s], Decompressed: 4916
Downloaded: 4961 file(s) [attempted 4961/8459 = 58%, 396 KB/s], Decompressed: 4950
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 257 KB/s], Decompressed: 4988
Downloaded: 5037 file(s) [attempted 5037/8459 = 59%, 57 KB/s], Decompressed: 5026
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 469 KB/s], Decompressed: 5073
Downloaded: 5115 file(s) [attempted 5115/8459 = 60%, 92 KB/s], Decompressed: 5101
Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 129 KB/s], Decompressed: 5145
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 130 KB/s], Decompressed: 5193
Downloaded: 5238 file(s) [attempted 5238/8459 = 61%, 399 KB/s], Decompressed: 5234
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 1206 KB/s], Decompressed: 5279
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 1021 KB/s], Decompressed: 5323
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 321 KB/s], Decompressed: 5358
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 277 KB/s], Decompressed: 5392
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 477 KB/s], Decompressed: 5440
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 151 KB/s], Decompressed: 5481
Downloaded: 5530 file(s) [attempted 5530/8459 = 65%, 76 KB/s], Decompressed: 5515
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5515
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 314 KB/s], Decompressed: 5522
Downloaded: 5640 file(s) [attempted 5640/8459 = 66%, 140 KB/s], Decompressed: 5631
Downloaded: 5680 file(s) [attempted 5680/8459 = 67%, 218 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 297 KB/s], Decompressed: 5720
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 454 KB/s], Decompressed: 5758
Downloaded: 5802 file(s) [attempted 5802/8459 = 68%, 585 KB/s], Decompressed: 5799
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 217 KB/s], Decompressed: 5837
Downloaded: 5884 file(s) [attempted 5884/8459 = 69%, 56 KB/s], Decompressed: 5874
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 600 KB/s], Decompressed: 5915
Downloaded: 5963 file(s) [attempted 5963/8459 = 70%, 925 KB/s], Decompressed: 5953
Downloaded: 5995 file(s) [attempted 5995/8459 = 70%, 274 KB/s], Decompressed: 5987
Downloaded: 6035 file(s) [attempted 6035/8459 = 71%, 359 KB/s], Decompressed: 6032
Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 255 KB/s], Decompressed: 6076
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 406 KB/s], Decompressed: 6110
Downloaded: 6155 file(s) [attempted 6155/8459 = 72%, 1152 KB/s], Decompressed: 6148
Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 733 KB/s], Decompressed: 6189
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 25 KB/s], Decompressed: 6230
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 163 KB/s], Decompressed: 6230
Downloaded: 6319 file(s) [attempted 6319/8459 = 74%, 560 KB/s], Decompressed: 6230
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 29 KB/s], Decompressed: 6350
Downloaded: 6395 file(s) [attempted 6395/8459 = 75%, 731 KB/s], Decompressed: 6384
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 158 KB/s], Decompressed: 6429
Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 260 KB/s], Decompressed: 6470
Downloaded: 6514 file(s) [attempted 6514/8459 = 77%, 1506 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 174 KB/s], Decompressed: 6545
Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 81 KB/s], Decompressed: 6579
Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 55 KB/s], Decompressed: 6627
Downloaded: 6672 file(s) [attempted 6672/8459 = 78%, 81 KB/s], Decompressed: 6665
Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 155 KB/s], Decompressed: 6703
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 110 KB/s], Decompressed: 6733
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 76 KB/s], Decompressed: 6781
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 908 KB/s], Decompressed: 6822
Downloaded: 6868 file(s) [attempted 6868/8459 = 81%, 107 KB/s], Decompressed: 6863
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 101 KB/s], Decompressed: 6898
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 445 KB/s], Decompressed: 6939
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 607 KB/s], Decompressed: 6973
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 306 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1151 KB/s], Decompressed: 7048
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 288 KB/s], Decompressed: 7096
Downloaded: 7139 file(s) [attempted 7139/8459 = 84%, 643 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 100 KB/s], Decompressed: 7175
Downloaded: 7222 file(s) [attempted 7222/8459 = 85%, 285 KB/s], Decompressed: 7212
Downloaded: 7258 file(s) [attempted 7258/8459 = 85%, 36 KB/s], Decompressed: 7256
Downloaded: 7296 file(s) [attempted 7296/8459 = 86%, 199 KB/s], Decompressed: 7292
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 73 KB/s], Decompressed: 7332
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 385 KB/s], Decompressed: 7373
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 141 KB/s], Decompressed: 7408
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 207 KB/s], Decompressed: 7452
Downloaded: 7495 file(s) [attempted 7495/8459 = 88%, 301 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 625 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 117 KB/s], Decompressed: 7572
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 170 KB/s], Decompressed: 7609
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 120 KB/s], Decompressed: 7647
Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 106 KB/s], Decompressed: 7695
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 118 KB/s], Decompressed: 7733
Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 313 KB/s], Decompressed: 7763
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 959 KB/s], Decompressed: 7801
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 131 KB/s], Decompressed: 7828
Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 844 KB/s], Decompressed: 7828
Downloaded: 7937 file(s) [attempted 7937/8459 = 93%, 86 KB/s], Decompressed: 7924
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 75 KB/s], Decompressed: 7962
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 47 KB/s], Decompressed: 8003
Downloaded: 8046 file(s) [attempted 8046/8459 = 95%, 488 KB/s], Decompressed: 8037
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 109 KB/s], Decompressed: 8078
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 490 KB/s], Decompressed: 8119
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 117 KB/s], Decompressed: 8160
Downloaded: 8201 file(s) [attempted 8201/8459 = 96%, 30 KB/s], Decompressed: 8198
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 199 KB/s], Decompressed: 8239
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 82 KB/s], Decompressed: 8277
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 374 KB/s], Decompressed: 8318
Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 885 KB/s], Decompressed: 8355
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 125 KB/s], Decompressed: 8397
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 108 KB/s], Decompressed: 8431
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 108 KB/s], Decompressed: 8451

lake build

ℹ [3472/3481] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3494/3506] 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`
⚠ [3632/3645] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3641/3655] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3703/3717] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3704/3717] 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`
⚠ [3812/3829] 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:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
⚠ [3813/3829] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3945/3955] 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`
⚠ [3947/3964] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3949/3964] 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:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
⚠ [3951/3964] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3954/3964] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3955/3964] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [3962/3964] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
⚠ [3967/3983] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2193:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2222:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2302:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2420:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2455:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2609:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2623:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2649:8: declaration uses `sorry`
⚠ [3973/3983] 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`
⚠ [3974/3983] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
⚠ [3977/3983] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [3998/4021] 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`
⚠ [4001/4021] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4003/4021] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4007/4021] 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`
⚠ [4010/4046] 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`
⚠ [4011/4046] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4015/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (22s)
✔ [4023/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (6.2s)
✔ [4026/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (3.2s)
ℹ [4027/4046] 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.
✔ [4032/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.1s)
✔ [4033/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (2.2s)
✔ [4035/4046] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (2.3s)
✔ [4044/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (2.3s)
✔ [4045/4046] Built PrimeNumberTheoremAnd (116s)
Build completed successfully (4046 jobs).

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

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (879ms)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (557ms)
✔ [33/35] Built Cli:c.o (69ms)
ℹ [3505/3517] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3531/3549] 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`
⚠ [3681/3698] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3691/3698] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3755/3772] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3757/3772] 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`
⚠ [3868/3887] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3874/3893] 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:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
⚠ [4011/4033] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4015/4033] 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`
⚠ [4017/4033] 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:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
⚠ [4021/4033] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [4024/4033] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [4027/4054] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [4034/4054] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
⚠ [4043/4067] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2193:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2222:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2302:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2420:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2455:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2609:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2623:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2649:8: declaration uses `sorry`
⚠ [4050/4067] 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`
⚠ [4052/4067] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
⚠ [4057/4067] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [4082/4124] 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`
⚠ [4087/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4091/4124] 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`
⚠ [4098/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4102/4169] 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`
✔ [4109/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (45s)
⚠ [4124/4169] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4127/4169] 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.
✔ [4132/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (12s)
✔ [4135/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (3.5s)
✔ [4158/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.4s)
✔ [4159/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (2.3s)
✔ [4161/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (3.0s)
✔ [4164/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (2.3s)
✔ [4167/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (31s)
ℹ [4168/4170] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (89ms)
info: Blueprint indexing
Build completed successfully (4170 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)

apx-semantic-phase	{"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":10,"diagnostic_count":7,"duration_ms":630,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":10,"dependency_count":3,"diagnostic_count":87,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":459421,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":10,"dependency_count":3,"diagnostic_count":87,"duration_ms":64,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":103888,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":103888,"phase":"lean_json_write"}

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":4485}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":215,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3864,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 1211ac1e9e7c87463945aa86120ebdafd3730fb5e93c76b817367c5a41d97f99
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":463413,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":22,"diagnostic_count":4,"duration_ms":1391,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":22,"dependency_count":46,"diagnostic_count":350,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":565963,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":22,"dependency_count":46,"diagnostic_count":350,"duration_ms":87,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":306822,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":306822,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":110,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":10,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4132,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 19914302d18249e17b9159b53e2945ea599a5ca7b5e05871314eae259741228c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":570824,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":4,"diagnostic_count":0,"duration_ms":309,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":4,"dependency_count":7,"diagnostic_count":24,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":288309,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":4,"dependency_count":7,"diagnostic_count":24,"duration_ms":73,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":34192,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":34192,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":190,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":10,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3692,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2db6dfcbcf33f069ed7c36d97a7f51d8ee21991f1e54ca95696c71fc41ccf47e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":292230,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":8,"diagnostic_count":7,"duration_ms":414,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":8,"dependency_count":1,"diagnostic_count":13,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":244103,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":8,"dependency_count":1,"diagnostic_count":13,"duration_ms":71,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":47602,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":47602,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":10}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":131,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":9,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3100,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 92fd139ec3ae9a88208a02da4975ad3d5a27559b069b9469438394cbe16a6f04
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":247787,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":20,"diagnostic_count":8,"duration_ms":966,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":20,"dependency_count":15,"diagnostic_count":246,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":220566,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":20,"dependency_count":15,"diagnostic_count":246,"duration_ms":70,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":227194,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":227194,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":196,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3251,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache c70793a231a1aa6c0f51a73d9cc37ce7aad5ede1f6f42aff3543537512b02cd4
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":224744,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":7,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":428803,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":66,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":772,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":772,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":9}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":154,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":10792,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 0b5d5990030ca1d8a39ec60a92b926e478f411357012492540d471b1497b6c43
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":432874,"ok":true}