Verification run

Run 79

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 774afdb6d161 toolchain lean-v4-30-0 prover lean took 19m 24s · finished 4w ago

lake build failed with exit code 1 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

$ git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-531-source
exit_code=Some(0) duration_ms=944
stderr:
Cloning into '/var/lib/apodeixis/repos/job-531-source'...


$ git checkout 774afdb6d16164bbbcd47bd094fe96a920436f73
exit_code=Some(0) duration_ms=52
stderr:
Note: switching to '774afdb6d16164bbbcd47bd094fe96a920436f73'.

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 774afdb proof(kadiri): package eq13 limit (#1601)

Resolved source revision: 774afdb6d16164bbbcd47bd094fe96a920436f73

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=774afdb6d16164bbbcd47bd094fe96a920436f73 provenance={"branch":"main","checked_out_revision":"774afdb6d16164bbbcd47bd094fe96a920436f73","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"774afdb6d16164bbbcd47bd094fe96a920436f73","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 13 Lean dependency package snapshot(s)
Prepared 13 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction

$ lake exe cache get
exit_code=Some(0) duration_ms=61454
stdout:
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)

stderr:
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%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 6 KB/s], Decompressed: 11
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 14 KB/s], Decompressed: 37
Downloaded: 72 file(s) [attempted 72/8459 = 0%, 101 KB/s], Decompressed: 71
Downloaded: 103 file(s) [attempted 103/8459 = 1%, 246 KB/s], Decompressed: 100
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 370 KB/s], Decompressed: 131
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 678 KB/s], Decompressed: 165
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 164 KB/s], Decompressed: 196
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 475 KB/s], Decompressed: 234
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 271 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 668 KB/s], Decompressed: 312
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 542 KB/s], Decompressed: 350
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 137 KB/s], Decompressed: 384
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 53 KB/s], Decompressed: 425
Downloaded: 472 file(s) [attempted 472/8459 = 5%, 406 KB/s], Decompressed: 466
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 581 KB/s], Decompressed: 508
Downloaded: 547 file(s) [attempted 547/8459 = 6%, 28 KB/s], Decompressed: 535
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 322 KB/s], Decompressed: 580
Downloaded: 621 file(s) [attempted 621/8459 = 7%, 286 KB/s], Decompressed: 617
Downloaded: 666 file(s) [attempted 666/8459 = 7%, 46 KB/s], Decompressed: 662
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 220 KB/s], Decompressed: 693
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 283 KB/s], Decompressed: 730
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 68 KB/s], Decompressed: 777
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1726 KB/s], Decompressed: 816
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 535 KB/s], Decompressed: 860
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 50 KB/s], Decompressed: 905
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 461 KB/s], Decompressed: 936
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 70 KB/s], Decompressed: 980
Downloaded: 1023 file(s) [attempted 1023/8459 = 12%, 437 KB/s], Decompressed: 1018
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 172 KB/s], Decompressed: 1062
Downloaded: 1114 file(s) [attempted 1114/8459 = 13%, 310 KB/s], Decompressed: 1110
Downloaded: 1155 file(s) [attempted 1155/8459 = 13%, 614 KB/s], Decompressed: 1148
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 908 KB/s], Decompressed: 1189
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 273 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 632 KB/s], Decompressed: 1264
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 44 KB/s], Decompressed: 1305
Downloaded: 1343 file(s) [attempted 1343/8459 = 15%, 53 KB/s], Decompressed: 1340
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 188 KB/s], Decompressed: 1370
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 877 KB/s], Decompressed: 1415
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 370 KB/s], Decompressed: 1456
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 150 KB/s], Decompressed: 1490
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 161 KB/s], Decompressed: 1528
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 271 KB/s], Decompressed: 1572
Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 200 KB/s], Decompressed: 1613
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 463 KB/s], Decompressed: 1644
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 181 KB/s], Decompressed: 1685
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 284 KB/s], Decompressed: 1726
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 557 KB/s], Decompressed: 1767
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 315 KB/s], Decompressed: 1815
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 480 KB/s], Decompressed: 1853
Downloaded: 1895 file(s) [attempted 1895/8459 = 22%, 44 KB/s], Decompressed: 1891
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 73 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 97 KB/s], Decompressed: 1959
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 128 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 699 KB/s], Decompressed: 2048
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 326 KB/s], Decompressed: 2093
Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 127 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 196 KB/s], Decompressed: 2171
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 569 KB/s], Decompressed: 2209
Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 396 KB/s], Decompressed: 2247
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 129 KB/s], Decompressed: 2288
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 48 KB/s], Decompressed: 2329
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 984 KB/s], Decompressed: 2366
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 71 KB/s], Decompressed: 2407
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 265 KB/s], Decompressed: 2448
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 611 KB/s], Decompressed: 2493
Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 28 KB/s], Decompressed: 2527
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 600 KB/s], Decompressed: 2568
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 378 KB/s], Decompressed: 2609
Downloaded: 2656 file(s) [attempted 2656/8459 = 31%, 574 KB/s], Decompressed: 2650
Downloaded: 2692 file(s) [attempted 2692/8459 = 31%, 342 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 180 KB/s], Decompressed: 2722
Downloaded: 2765 file(s) [attempted 2765/8459 = 32%, 1824 KB/s], Decompressed: 2760
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 679 KB/s], Decompressed: 2801
Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 114 KB/s], Decompressed: 2842
Downloaded: 2892 file(s) [attempted 2892/8459 = 34%, 39 KB/s], Decompressed: 2883
Downloaded: 2927 file(s) [attempted 2927/8459 = 34%, 81 KB/s], Decompressed: 2917
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 184 KB/s], Decompressed: 2958
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 323 KB/s], Decompressed: 3003
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 1221 KB/s], Decompressed: 3044
Downloaded: 3089 file(s) [attempted 3089/8459 = 36%, 310 KB/s], Decompressed: 3085
Downloaded: 3130 file(s) [attempted 3130/8459 = 37%, 55 KB/s], Decompressed: 3119
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1553 KB/s], Decompressed: 3157
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 232 KB/s], Decompressed: 3201
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 44 KB/s], Decompressed: 3239
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 126 KB/s], Decompressed: 3284
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 201 KB/s], Decompressed: 3321
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 61 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 117 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 52 KB/s], Decompressed: 3444
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 1589 KB/s], Decompressed: 3482
Downloaded: 3525 file(s) [attempted 3525/8459 = 41%, 580 KB/s], Decompressed: 3520
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 406 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 101 KB/s], Decompressed: 3602
Downloaded: 3644 file(s) [attempted 3644/8459 = 43%, 487 KB/s], Decompressed: 3638
Downloaded: 3682 file(s) [attempted 3682/8459 = 43%, 250 KB/s], Decompressed: 3674
Downloaded: 3722 file(s) [attempted 3722/8459 = 44%, 44 KB/s], Decompressed: 3718
Downloaded: 3760 file(s) [attempted 3760/8459 = 44%, 60 KB/s], Decompressed: 3756
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 300 KB/s], Decompressed: 3793
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 208 KB/s], Decompressed: 3831
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 249 KB/s], Decompressed: 3869
Downloaded: 3911 file(s) [attempted 3911/8459 = 46%, 591 KB/s], Decompressed: 3906
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 188 KB/s], Decompressed: 3948
Downloaded: 3991 file(s) [attempted 3991/8459 = 47%, 688 KB/s], Decompressed: 3985
Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 102 KB/s], Decompressed: 4026
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 63 KB/s], Decompressed: 4060
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 40 KB/s], Decompressed: 4101
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 955 KB/s], Decompressed: 4139
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 1317 KB/s], Decompressed: 4177
Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 675 KB/s], Decompressed: 4221
Downloaded: 4264 file(s) [attempted 4264/8459 = 50%, 48 KB/s], Decompressed: 4259
Downloaded: 4305 file(s) [attempted 4305/8459 = 50%, 317 KB/s], Decompressed: 4297
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 165 KB/s], Decompressed: 4334
Downloaded: 4379 file(s) [attempted 4379/8459 = 51%, 494 KB/s], Decompressed: 4376
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 294 KB/s], Decompressed: 4410
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 188 KB/s], Decompressed: 4451
Downloaded: 4496 file(s) [attempted 4496/8459 = 53%, 131 KB/s], Decompressed: 4492
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 908 KB/s], Decompressed: 4533
Downloaded: 4575 file(s) [attempted 4575/8459 = 54%, 341 KB/s], Decompressed: 4570
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 355 KB/s], Decompressed: 4611
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 763 KB/s], Decompressed: 4653
Downloaded: 4696 file(s) [attempted 4696/8459 = 55%, 35 KB/s], Decompressed: 4690
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 91 KB/s], Decompressed: 4728
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 30 KB/s], Decompressed: 4765
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 274 KB/s], Decompressed: 4810
Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 84 KB/s], Decompressed: 4851
Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 163 KB/s], Decompressed: 4885
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 377 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 1670 KB/s], Decompressed: 4964
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 98 KB/s], Decompressed: 5008
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 369 KB/s], Decompressed: 5053
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 135 KB/s], Decompressed: 5087
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 1027 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 1453 KB/s], Decompressed: 5162
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 182 KB/s], Decompressed: 5207
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 739 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 61 KB/s], Decompressed: 5293
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 252 KB/s], Decompressed: 5323
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 1065 KB/s], Decompressed: 5361
Downloaded: 5403 file(s) [attempted 5403/8459 = 63%, 56 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 479 KB/s], Decompressed: 5440
Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 191 KB/s], Decompressed: 5488
Downloaded: 5526 file(s) [attempted 5526/8459 = 65%, 83 KB/s], Decompressed: 5522
Downloaded: 5560 file(s) [attempted 5560/8459 = 65%, 300 KB/s], Decompressed: 5558
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 797 KB/s], Decompressed: 5597
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 136 KB/s], Decompressed: 5638
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 604 KB/s], Decompressed: 5686
Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 62 KB/s], Decompressed: 5724
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 201 KB/s], Decompressed: 5751
Downloaded: 5797 file(s) [attempted 5797/8459 = 68%, 733 KB/s], Decompressed: 5792
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 219 KB/s], Decompressed: 5837
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 89 KB/s], Decompressed: 5881
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1060 KB/s], Decompressed: 5915
Downloaded: 5955 file(s) [attempted 5955/8459 = 70%, 733 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 583 KB/s], Decompressed: 5991
Downloaded: 6042 file(s) [attempted 6042/8459 = 71%, 110 KB/s], Decompressed: 6039
Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 314 KB/s], Decompressed: 6083
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 150 KB/s], Decompressed: 6124
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 281 KB/s], Decompressed: 6165
Downloaded: 6199 file(s) [attempted 6199/8459 = 73%, 73 KB/s], Decompressed: 6196
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 179 KB/s], Decompressed: 6240
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 374 KB/s], Decompressed: 6285
Downloaded: 6331 file(s) [attempted 6331/8459 = 74%, 49 KB/s], Decompressed: 6312
Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 186 KB/s], Decompressed: 6357
Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 104 KB/s], Decompressed: 6398
Downloaded: 6442 file(s) [attempted 6442/8459 = 76%, 88 KB/s], Decompressed: 6436
Downloaded: 6483 file(s) [attempted 6483/8459 = 76%, 389 KB/s], Decompressed: 6477
Downloaded: 6528 file(s) [attempted 6528/8459 = 77%, 432 KB/s], Decompressed: 6525
Downloaded: 6571 file(s) [attempted 6571/8459 = 77%, 345 KB/s], Decompressed: 6562
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 526 KB/s], Decompressed: 6596
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 30 KB/s], Decompressed: 6637
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 79 KB/s], Decompressed: 6675
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 1505 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 141 KB/s], Decompressed: 6768
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 34 KB/s], Decompressed: 6802
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 81 KB/s], Decompressed: 6846
Downloaded: 6891 file(s) [attempted 6891/8459 = 81%, 271 KB/s], Decompressed: 6887
Downloaded: 6932 file(s) [attempted 6932/8459 = 81%, 192 KB/s], Decompressed: 6928
Downloaded: 6973 file(s) [attempted 6973/8459 = 82%, 521 KB/s], Decompressed: 6966
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 96 KB/s], Decompressed: 7000
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 133 KB/s], Decompressed: 7047
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 137 KB/s], Decompressed: 7093
Downloaded: 7137 file(s) [attempted 7137/8459 = 84%, 488 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 100 KB/s], Decompressed: 7171
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 2055 KB/s], Decompressed: 7209
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 425 KB/s], Decompressed: 7247
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 80 KB/s], Decompressed: 7288
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 367 KB/s], Decompressed: 7332
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 69 KB/s], Decompressed: 7366
Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 28 KB/s], Decompressed: 7404
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 112 KB/s], Decompressed: 7442
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 1159 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 85 KB/s], Decompressed: 7527
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 125 KB/s], Decompressed: 7565
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 63 KB/s], Decompressed: 7606
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 289 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 22 KB/s], Decompressed: 7685
Downloaded: 7731 file(s) [attempted 7731/8459 = 91%, 931 KB/s], Decompressed: 7726
Downloaded: 7768 file(s) [attempted 7768/8459 = 91%, 465 KB/s], Decompressed: 7763
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 48 KB/s], Decompressed: 7805
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 207 KB/s], Decompressed: 7846
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 311 KB/s], Decompressed: 7883
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 655 KB/s], Decompressed: 7928
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 370 KB/s], Decompressed: 7965
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 244 KB/s], Decompressed: 7996
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 497 KB/s], Decompressed: 8030
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 800 KB/s], Decompressed: 8075
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 39 KB/s], Decompressed: 8106
Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 72 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 31 KB/s], Decompressed: 8188
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 54 KB/s], Decompressed: 8229
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 140 KB/s], Decompressed: 8270
Downloaded: 8315 file(s) [attempted 8315/8459 = 98%, 524 KB/s], Decompressed: 8311
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 1095 KB/s], Decompressed: 8349
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 271 KB/s], Decompressed: 8386
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 725 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 483 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 483 KB/s], Decompressed: 8451


$ lake build
exit_code=Some(1) duration_ms=528865
stdout:
✔ [3473/3476] Built PrimeNumberTheoremAnd.ZetaBounds (98s)
ℹ [3538/3549] Built PrimeNumberTheoremAnd.MediumPNT (35s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3547/3551] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (5.7s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (14s)
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`
✔ [3566/3572] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.5s)
⚠ [3694/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3805/3817] Built PrimeNumberTheoremAnd.IEANTN.LogTables (29s)
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3814/3819] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.2s)
✖ [3816/3819] Building PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1184:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1210:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1486:14: private declaration `Mertens.integrableOn_E₂Λ_mul_rpow` has already been declared
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1566:33: Application type mismatch: The argument
  hs
has type
  1 < s
of sort `Prop` but is expected to have type
  ℝ
of sort `Type` in the application
  integrableOn_E₂Λ_mul_rpow hs
error: Lean exited with code 1
✔ [3817/3824] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (9.0s)
✔ [3871/3880] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.8s)
⚠ [3882/3893] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3888/3895] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.4s)
✔ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (48s)
✔ [4020/4045] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (98s)
✔ [4064/4072] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (4.8s)
⚠ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4072/4082] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (48s)
⚠ [4120/4130] 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`
✔ [4133/4166] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (2.9s)
ℹ [4163/4188] 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.
⚠ [4165/4188] 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`
✔ [4179/4188] Built PrimeNumberTheoremAnd.PerronFormula (8.4s)
✔ [4185/4188] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (6.3s)
⚠ [4186/4188] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: build failed


$ lake build :blueprint
exit_code=Some(1) duration_ms=370409
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [32/35] Built Cli.Extensions:c.o (522ms)
✔ [33/35] Built Cli:c.o (65ms)
✔ [3509/3518] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (67s)
ℹ [3593/3609] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3596/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (58s)
✔ [3611/3628] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (2.7s)
⚠ [3620/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 (48s)
✔ [3637/3649] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.7s)
⚠ [3765/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3879/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.7s)
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3896/3902] Building PrimeNumberTheoremAnd.IEANTN.Mertens (12s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1184:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1210:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1486:14: private declaration `Mertens.integrableOn_E₂Λ_mul_rpow` has already been declared
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1566:33: Application type mismatch: The argument
  hs
has type
  1 < s
of sort `Prop` but is expected to have type
  ℝ
of sort `Type` in the application
  integrableOn_E₂Λ_mul_rpow hs
error: Lean exited with code 1
✔ [3897/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.4s)
✔ [3899/3916] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.8s)
✔ [3963/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.7s)
⚠ [3967/3988] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3980/4000] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.1s)
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (5.5s)
✔ [4119/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (5.0s)
✔ [4192/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.7s)
⚠ [4193/4206] 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`
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.5s)
✔ [4204/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
⚠ [4278/4356] 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`
✔ [4309/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.4s)
ℹ [4334/4397] 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.
⚠ [4335/4397] 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`
✔ [4353/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.9s)
✔ [4390/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4391/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (3.9s)
⚠ [4392/4397] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
✔ [4394/4398] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (43s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: build failed


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_clone exit 0 duration 944 ms · created 6/18/2026, 8:34:08 PM

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

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

git_checkout exit 0 duration 52 ms · created 6/18/2026, 8:34:08 PM

git checkout 774afdb6d16164bbbcd47bd094fe96a920436f73

Note: switching to '774afdb6d16164bbbcd47bd094fe96a920436f73'.

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 774afdb proof(kadiri): package eq13 limit (#1601)

lake_cache exit 0 duration 1m 1s · created 6/18/2026, 8:34:08 PM

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%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 6 KB/s], Decompressed: 11
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 14 KB/s], Decompressed: 37
Downloaded: 72 file(s) [attempted 72/8459 = 0%, 101 KB/s], Decompressed: 71
Downloaded: 103 file(s) [attempted 103/8459 = 1%, 246 KB/s], Decompressed: 100
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 370 KB/s], Decompressed: 131
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 678 KB/s], Decompressed: 165
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 164 KB/s], Decompressed: 196
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 475 KB/s], Decompressed: 234
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 271 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 668 KB/s], Decompressed: 312
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 542 KB/s], Decompressed: 350
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 137 KB/s], Decompressed: 384
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 53 KB/s], Decompressed: 425
Downloaded: 472 file(s) [attempted 472/8459 = 5%, 406 KB/s], Decompressed: 466
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 581 KB/s], Decompressed: 508
Downloaded: 547 file(s) [attempted 547/8459 = 6%, 28 KB/s], Decompressed: 535
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 322 KB/s], Decompressed: 580
Downloaded: 621 file(s) [attempted 621/8459 = 7%, 286 KB/s], Decompressed: 617
Downloaded: 666 file(s) [attempted 666/8459 = 7%, 46 KB/s], Decompressed: 662
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 220 KB/s], Decompressed: 693
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 283 KB/s], Decompressed: 730
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 68 KB/s], Decompressed: 777
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1726 KB/s], Decompressed: 816
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 535 KB/s], Decompressed: 860
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 50 KB/s], Decompressed: 905
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 461 KB/s], Decompressed: 936
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 70 KB/s], Decompressed: 980
Downloaded: 1023 file(s) [attempted 1023/8459 = 12%, 437 KB/s], Decompressed: 1018
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 172 KB/s], Decompressed: 1062
Downloaded: 1114 file(s) [attempted 1114/8459 = 13%, 310 KB/s], Decompressed: 1110
Downloaded: 1155 file(s) [attempted 1155/8459 = 13%, 614 KB/s], Decompressed: 1148
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 908 KB/s], Decompressed: 1189
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 273 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 632 KB/s], Decompressed: 1264
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 44 KB/s], Decompressed: 1305
Downloaded: 1343 file(s) [attempted 1343/8459 = 15%, 53 KB/s], Decompressed: 1340
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 188 KB/s], Decompressed: 1370
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 877 KB/s], Decompressed: 1415
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 370 KB/s], Decompressed: 1456
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 150 KB/s], Decompressed: 1490
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 161 KB/s], Decompressed: 1528
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 271 KB/s], Decompressed: 1572
Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 200 KB/s], Decompressed: 1613
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 463 KB/s], Decompressed: 1644
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 181 KB/s], Decompressed: 1685
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 284 KB/s], Decompressed: 1726
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 557 KB/s], Decompressed: 1767
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 315 KB/s], Decompressed: 1815
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 480 KB/s], Decompressed: 1853
Downloaded: 1895 file(s) [attempted 1895/8459 = 22%, 44 KB/s], Decompressed: 1891
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 73 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 97 KB/s], Decompressed: 1959
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 128 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 699 KB/s], Decompressed: 2048
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 326 KB/s], Decompressed: 2093
Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 127 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 196 KB/s], Decompressed: 2171
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 569 KB/s], Decompressed: 2209
Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 396 KB/s], Decompressed: 2247
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 129 KB/s], Decompressed: 2288
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 48 KB/s], Decompressed: 2329
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 984 KB/s], Decompressed: 2366
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 71 KB/s], Decompressed: 2407
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 265 KB/s], Decompressed: 2448
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 611 KB/s], Decompressed: 2493
Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 28 KB/s], Decompressed: 2527
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 600 KB/s], Decompressed: 2568
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 378 KB/s], Decompressed: 2609
Downloaded: 2656 file(s) [attempted 2656/8459 = 31%, 574 KB/s], Decompressed: 2650
Downloaded: 2692 file(s) [attempted 2692/8459 = 31%, 342 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 180 KB/s], Decompressed: 2722
Downloaded: 2765 file(s) [attempted 2765/8459 = 32%, 1824 KB/s], Decompressed: 2760
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 679 KB/s], Decompressed: 2801
Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 114 KB/s], Decompressed: 2842
Downloaded: 2892 file(s) [attempted 2892/8459 = 34%, 39 KB/s], Decompressed: 2883
Downloaded: 2927 file(s) [attempted 2927/8459 = 34%, 81 KB/s], Decompressed: 2917
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 184 KB/s], Decompressed: 2958
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 323 KB/s], Decompressed: 3003
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 1221 KB/s], Decompressed: 3044
Downloaded: 3089 file(s) [attempted 3089/8459 = 36%, 310 KB/s], Decompressed: 3085
Downloaded: 3130 file(s) [attempted 3130/8459 = 37%, 55 KB/s], Decompressed: 3119
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1553 KB/s], Decompressed: 3157
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 232 KB/s], Decompressed: 3201
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 44 KB/s], Decompressed: 3239
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 126 KB/s], Decompressed: 3284
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 201 KB/s], Decompressed: 3321
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 61 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 117 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 52 KB/s], Decompressed: 3444
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 1589 KB/s], Decompressed: 3482
Downloaded: 3525 file(s) [attempted 3525/8459 = 41%, 580 KB/s], Decompressed: 3520
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 406 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 101 KB/s], Decompressed: 3602
Downloaded: 3644 file(s) [attempted 3644/8459 = 43%, 487 KB/s], Decompressed: 3638
Downloaded: 3682 file(s) [attempted 3682/8459 = 43%, 250 KB/s], Decompressed: 3674
Downloaded: 3722 file(s) [attempted 3722/8459 = 44%, 44 KB/s], Decompressed: 3718
Downloaded: 3760 file(s) [attempted 3760/8459 = 44%, 60 KB/s], Decompressed: 3756
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 300 KB/s], Decompressed: 3793
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 208 KB/s], Decompressed: 3831
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 249 KB/s], Decompressed: 3869
Downloaded: 3911 file(s) [attempted 3911/8459 = 46%, 591 KB/s], Decompressed: 3906
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 188 KB/s], Decompressed: 3948
Downloaded: 3991 file(s) [attempted 3991/8459 = 47%, 688 KB/s], Decompressed: 3985
Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 102 KB/s], Decompressed: 4026
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 63 KB/s], Decompressed: 4060
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 40 KB/s], Decompressed: 4101
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 955 KB/s], Decompressed: 4139
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 1317 KB/s], Decompressed: 4177
Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 675 KB/s], Decompressed: 4221
Downloaded: 4264 file(s) [attempted 4264/8459 = 50%, 48 KB/s], Decompressed: 4259
Downloaded: 4305 file(s) [attempted 4305/8459 = 50%, 317 KB/s], Decompressed: 4297
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 165 KB/s], Decompressed: 4334
Downloaded: 4379 file(s) [attempted 4379/8459 = 51%, 494 KB/s], Decompressed: 4376
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 294 KB/s], Decompressed: 4410
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 188 KB/s], Decompressed: 4451
Downloaded: 4496 file(s) [attempted 4496/8459 = 53%, 131 KB/s], Decompressed: 4492
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 908 KB/s], Decompressed: 4533
Downloaded: 4575 file(s) [attempted 4575/8459 = 54%, 341 KB/s], Decompressed: 4570
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 355 KB/s], Decompressed: 4611
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 763 KB/s], Decompressed: 4653
Downloaded: 4696 file(s) [attempted 4696/8459 = 55%, 35 KB/s], Decompressed: 4690
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 91 KB/s], Decompressed: 4728
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 30 KB/s], Decompressed: 4765
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 274 KB/s], Decompressed: 4810
Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 84 KB/s], Decompressed: 4851
Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 163 KB/s], Decompressed: 4885
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 377 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 1670 KB/s], Decompressed: 4964
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 98 KB/s], Decompressed: 5008
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 369 KB/s], Decompressed: 5053
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 135 KB/s], Decompressed: 5087
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 1027 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 1453 KB/s], Decompressed: 5162
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 182 KB/s], Decompressed: 5207
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 739 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 61 KB/s], Decompressed: 5293
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 252 KB/s], Decompressed: 5323
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 1065 KB/s], Decompressed: 5361
Downloaded: 5403 file(s) [attempted 5403/8459 = 63%, 56 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 479 KB/s], Decompressed: 5440
Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 191 KB/s], Decompressed: 5488
Downloaded: 5526 file(s) [attempted 5526/8459 = 65%, 83 KB/s], Decompressed: 5522
Downloaded: 5560 file(s) [attempted 5560/8459 = 65%, 300 KB/s], Decompressed: 5558
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 797 KB/s], Decompressed: 5597
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 136 KB/s], Decompressed: 5638
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 604 KB/s], Decompressed: 5686
Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 62 KB/s], Decompressed: 5724
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 201 KB/s], Decompressed: 5751
Downloaded: 5797 file(s) [attempted 5797/8459 = 68%, 733 KB/s], Decompressed: 5792
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 219 KB/s], Decompressed: 5837
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 89 KB/s], Decompressed: 5881
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1060 KB/s], Decompressed: 5915
Downloaded: 5955 file(s) [attempted 5955/8459 = 70%, 733 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 583 KB/s], Decompressed: 5991
Downloaded: 6042 file(s) [attempted 6042/8459 = 71%, 110 KB/s], Decompressed: 6039
Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 314 KB/s], Decompressed: 6083
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 150 KB/s], Decompressed: 6124
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 281 KB/s], Decompressed: 6165
Downloaded: 6199 file(s) [attempted 6199/8459 = 73%, 73 KB/s], Decompressed: 6196
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 179 KB/s], Decompressed: 6240
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 374 KB/s], Decompressed: 6285
Downloaded: 6331 file(s) [attempted 6331/8459 = 74%, 49 KB/s], Decompressed: 6312
Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 186 KB/s], Decompressed: 6357
Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 104 KB/s], Decompressed: 6398
Downloaded: 6442 file(s) [attempted 6442/8459 = 76%, 88 KB/s], Decompressed: 6436
Downloaded: 6483 file(s) [attempted 6483/8459 = 76%, 389 KB/s], Decompressed: 6477
Downloaded: 6528 file(s) [attempted 6528/8459 = 77%, 432 KB/s], Decompressed: 6525
Downloaded: 6571 file(s) [attempted 6571/8459 = 77%, 345 KB/s], Decompressed: 6562
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 526 KB/s], Decompressed: 6596
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 30 KB/s], Decompressed: 6637
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 79 KB/s], Decompressed: 6675
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 1505 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 141 KB/s], Decompressed: 6768
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 34 KB/s], Decompressed: 6802
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 81 KB/s], Decompressed: 6846
Downloaded: 6891 file(s) [attempted 6891/8459 = 81%, 271 KB/s], Decompressed: 6887
Downloaded: 6932 file(s) [attempted 6932/8459 = 81%, 192 KB/s], Decompressed: 6928
Downloaded: 6973 file(s) [attempted 6973/8459 = 82%, 521 KB/s], Decompressed: 6966
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 96 KB/s], Decompressed: 7000
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 133 KB/s], Decompressed: 7047
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 137 KB/s], Decompressed: 7093
Downloaded: 7137 file(s) [attempted 7137/8459 = 84%, 488 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 100 KB/s], Decompressed: 7171
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 2055 KB/s], Decompressed: 7209
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 425 KB/s], Decompressed: 7247
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 80 KB/s], Decompressed: 7288
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 367 KB/s], Decompressed: 7332
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 69 KB/s], Decompressed: 7366
Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 28 KB/s], Decompressed: 7404
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 112 KB/s], Decompressed: 7442
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 1159 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 85 KB/s], Decompressed: 7527
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 125 KB/s], Decompressed: 7565
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 63 KB/s], Decompressed: 7606
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 289 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 22 KB/s], Decompressed: 7685
Downloaded: 7731 file(s) [attempted 7731/8459 = 91%, 931 KB/s], Decompressed: 7726
Downloaded: 7768 file(s) [attempted 7768/8459 = 91%, 465 KB/s], Decompressed: 7763
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 48 KB/s], Decompressed: 7805
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 207 KB/s], Decompressed: 7846
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 311 KB/s], Decompressed: 7883
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 655 KB/s], Decompressed: 7928
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 370 KB/s], Decompressed: 7965
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 244 KB/s], Decompressed: 7996
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 497 KB/s], Decompressed: 8030
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 800 KB/s], Decompressed: 8075
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 39 KB/s], Decompressed: 8106
Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 72 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 31 KB/s], Decompressed: 8188
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 54 KB/s], Decompressed: 8229
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 140 KB/s], Decompressed: 8270
Downloaded: 8315 file(s) [attempted 8315/8459 = 98%, 524 KB/s], Decompressed: 8311
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 1095 KB/s], Decompressed: 8349
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 271 KB/s], Decompressed: 8386
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 725 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 483 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 483 KB/s], Decompressed: 8451

lean_checker exit 1 duration 8m 49s · created 6/18/2026, 8:34:08 PM

lake build

✔ [3473/3476] Built PrimeNumberTheoremAnd.ZetaBounds (98s)
ℹ [3538/3549] Built PrimeNumberTheoremAnd.MediumPNT (35s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3547/3551] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (5.7s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (14s)
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`
✔ [3566/3572] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.5s)
⚠ [3694/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3805/3817] Built PrimeNumberTheoremAnd.IEANTN.LogTables (29s)
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3814/3819] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.2s)
✖ [3816/3819] Building PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1184:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1210:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1486:14: private declaration `Mertens.integrableOn_E₂Λ_mul_rpow` has already been declared
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1566:33: Application type mismatch: The argument
  hs
has type
  1 < s
of sort `Prop` but is expected to have type
  ℝ
of sort `Type` in the application
  integrableOn_E₂Λ_mul_rpow hs
error: Lean exited with code 1
✔ [3817/3824] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (9.0s)
✔ [3871/3880] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.8s)
⚠ [3882/3893] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3888/3895] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.4s)
✔ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (48s)
✔ [4020/4045] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (98s)
✔ [4064/4072] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (4.8s)
⚠ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4072/4082] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (48s)
⚠ [4120/4130] 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`
✔ [4133/4166] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (2.9s)
ℹ [4163/4188] 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.
⚠ [4165/4188] 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`
✔ [4179/4188] Built PrimeNumberTheoremAnd.PerronFormula (8.4s)
✔ [4185/4188] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (6.3s)
⚠ [4186/4188] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens

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

blueprint_build exit 1 duration 6m 10s · created 6/18/2026, 8:34:08 PM

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [32/35] Built Cli.Extensions:c.o (522ms)
✔ [33/35] Built Cli:c.o (65ms)
✔ [3509/3518] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (67s)
ℹ [3593/3609] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3596/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (58s)
✔ [3611/3628] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (2.7s)
⚠ [3620/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 (48s)
✔ [3637/3649] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.7s)
⚠ [3765/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3879/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.7s)
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3896/3902] Building PrimeNumberTheoremAnd.IEANTN.Mertens (12s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1184:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1210:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1486:14: private declaration `Mertens.integrableOn_E₂Λ_mul_rpow` has already been declared
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1566:33: Application type mismatch: The argument
  hs
has type
  1 < s
of sort `Prop` but is expected to have type
  ℝ
of sort `Type` in the application
  integrableOn_E₂Λ_mul_rpow hs
error: Lean exited with code 1
✔ [3897/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.4s)
✔ [3899/3916] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.8s)
✔ [3963/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.7s)
⚠ [3967/3988] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3980/4000] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.1s)
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (5.5s)
✔ [4119/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (5.0s)
✔ [4192/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.7s)
⚠ [4193/4206] 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`
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.5s)
✔ [4204/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
⚠ [4278/4356] 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`
✔ [4309/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.4s)
ℹ [4334/4397] 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.
⚠ [4335/4397] 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`
✔ [4353/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.9s)
✔ [4390/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4391/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (3.9s)
⚠ [4392/4397] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
✔ [4394/4398] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (43s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens

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