Verification run
Run 146
failed commit
ddabba3864bb toolchain lean-v4-30-0 prover lean took 13m 53s · finished 1w 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)
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-1040-source
exit_code=Some(0) duration_ms=962
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1040-source'...
$ git checkout ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
exit_code=Some(128) duration_ms=1
stderr:
fatal: reference is not a tree: ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
$ git fetch --depth 1 origin ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
exit_code=Some(0) duration_ms=940
stderr:
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
* branch ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0 -> FETCH_HEAD
$ git checkout ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0 (after fetch)
exit_code=Some(0) duration_ms=50
stderr:
Note: switching to 'ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0'.
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 ddabba3 refactor(ResidueCalc): extract residue calculus from CH2 (#1537) (#1606)
Resolved source revision: ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0 provenance={"branch":"main","checked_out_revision":"ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0","used_missing_commit_fetch":true}
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=57038
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: 10
Downloaded: 33 file(s) [attempted 33/8459 = 0%, 30 KB/s], Decompressed: 29
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 56 KB/s], Decompressed: 56
Downloaded: 78 file(s) [attempted 78/8459 = 0%, 101 KB/s], Decompressed: 72
Downloaded: 103 file(s) [attempted 103/8459 = 1%, 186 KB/s], Decompressed: 102
Downloaded: 138 file(s) [attempted 138/8459 = 1%, 380 KB/s], Decompressed: 134
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 332 KB/s], Decompressed: 162
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 275 KB/s], Decompressed: 189
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 578 KB/s], Decompressed: 223
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 164 KB/s], Decompressed: 258
Downloaded: 295 file(s) [attempted 295/8459 = 3%, 175 KB/s], Decompressed: 292
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 74 KB/s], Decompressed: 329
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 107 KB/s], Decompressed: 367
Downloaded: 412 file(s) [attempted 412/8459 = 4%, 54 KB/s], Decompressed: 401
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 284 KB/s], Decompressed: 443
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 270 KB/s], Decompressed: 484
Downloaded: 525 file(s) [attempted 525/8459 = 6%, 570 KB/s], Decompressed: 521
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 519 KB/s], Decompressed: 559
Downloaded: 604 file(s) [attempted 604/8459 = 7%, 154 KB/s], Decompressed: 597
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 83 KB/s], Decompressed: 638
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 66 KB/s], Decompressed: 675
Downloaded: 717 file(s) [attempted 717/8459 = 8%, 375 KB/s], Decompressed: 710
Downloaded: 758 file(s) [attempted 758/8459 = 8%, 147 KB/s], Decompressed: 754
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 415 KB/s], Decompressed: 788
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 479 KB/s], Decompressed: 833
Downloaded: 874 file(s) [attempted 874/8459 = 10%, 239 KB/s], Decompressed: 871
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 871 KB/s], Decompressed: 912
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 388 KB/s], Decompressed: 949
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 145 KB/s], Decompressed: 984
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 408 KB/s], Decompressed: 1018
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 219 KB/s], Decompressed: 1062
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 394 KB/s], Decompressed: 1104
Downloaded: 1145 file(s) [attempted 1145/8459 = 13%, 235 KB/s], Decompressed: 1134
Downloaded: 1182 file(s) [attempted 1182/8459 = 13%, 37 KB/s], Decompressed: 1179
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 165 KB/s], Decompressed: 1216
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 55 KB/s], Decompressed: 1261
Downloaded: 1302 file(s) [attempted 1302/8459 = 15%, 179 KB/s], Decompressed: 1292
Downloaded: 1338 file(s) [attempted 1338/8459 = 15%, 1119 KB/s], Decompressed: 1329
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 337 KB/s], Decompressed: 1370
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 1431 KB/s], Decompressed: 1415
Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 171 KB/s], Decompressed: 1459
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 1237 KB/s], Decompressed: 1504
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 142 KB/s], Decompressed: 1535
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 398 KB/s], Decompressed: 1572
Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 193 KB/s], Decompressed: 1613
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 216 KB/s], Decompressed: 1655
Downloaded: 1694 file(s) [attempted 1694/8459 = 20%, 1073 KB/s], Decompressed: 1689
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 290 KB/s], Decompressed: 1726
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 475 KB/s], Decompressed: 1767
Downloaded: 1815 file(s) [attempted 1815/8459 = 21%, 556 KB/s], Decompressed: 1809
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 23 KB/s], Decompressed: 1850
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 713 KB/s], Decompressed: 1887
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 707 KB/s], Decompressed: 1925
Downloaded: 1966 file(s) [attempted 1966/8459 = 23%, 228 KB/s], Decompressed: 1963
Downloaded: 2007 file(s) [attempted 2007/8459 = 23%, 257 KB/s], Decompressed: 2000
Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 180 KB/s], Decompressed: 2024
Downloaded: 2075 file(s) [attempted 2075/8459 = 24%, 235 KB/s], Decompressed: 2072
Downloaded: 2117 file(s) [attempted 2117/8459 = 25%, 116 KB/s], Decompressed: 2113
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 495 KB/s], Decompressed: 2151
Downloaded: 2192 file(s) [attempted 2192/8459 = 25%, 397 KB/s], Decompressed: 2182
Downloaded: 2226 file(s) [attempted 2226/8459 = 26%, 38 KB/s], Decompressed: 2219
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 456 KB/s], Decompressed: 2260
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 1294 KB/s], Decompressed: 2305
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 63 KB/s], Decompressed: 2339
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 127 KB/s], Decompressed: 2363
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 220 KB/s], Decompressed: 2411
Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 167 KB/s], Decompressed: 2455
Downloaded: 2503 file(s) [attempted 2503/8459 = 29%, 85 KB/s], Decompressed: 2493
Downloaded: 2538 file(s) [attempted 2538/8459 = 30%, 567 KB/s], Decompressed: 2531
Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 685 KB/s], Decompressed: 2565
Downloaded: 2612 file(s) [attempted 2612/8459 = 30%, 69 KB/s], Decompressed: 2603
Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 135 KB/s], Decompressed: 2626
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 56 KB/s], Decompressed: 2692
Downloaded: 2727 file(s) [attempted 2727/8459 = 32%, 158 KB/s], Decompressed: 2722
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 334 KB/s], Decompressed: 2763
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 61 KB/s], Decompressed: 2784
Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 1297 KB/s], Decompressed: 2846
Downloaded: 2880 file(s) [attempted 2880/8459 = 34%, 76 KB/s], Decompressed: 2876
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 114 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 222 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 98 KB/s], Decompressed: 2994
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 147 KB/s], Decompressed: 3023
Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 191 KB/s], Decompressed: 3061
Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 685 KB/s], Decompressed: 3102
Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 53 KB/s], Decompressed: 3140
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 250 KB/s], Decompressed: 3181
Downloaded: 3222 file(s) [attempted 3222/8459 = 38%, 162 KB/s], Decompressed: 3201
Downloaded: 3255 file(s) [attempted 3255/8459 = 38%, 1300 KB/s], Decompressed: 3229
Downloaded: 3301 file(s) [attempted 3301/8459 = 39%, 64 KB/s], Decompressed: 3297
Downloaded: 3342 file(s) [attempted 3342/8459 = 39%, 467 KB/s], Decompressed: 3331
Downloaded: 3374 file(s) [attempted 3374/8459 = 39%, 634 KB/s], Decompressed: 3369
Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 240 KB/s], Decompressed: 3410
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 228 KB/s], Decompressed: 3427
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 355 KB/s], Decompressed: 3489
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 67 KB/s], Decompressed: 3527
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 103 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 35 KB/s], Decompressed: 3602
Downloaded: 3642 file(s) [attempted 3642/8459 = 43%, 39 KB/s], Decompressed: 3636
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 328 KB/s], Decompressed: 3674
Downloaded: 3720 file(s) [attempted 3720/8459 = 43%, 408 KB/s], Decompressed: 3715
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 842 KB/s], Decompressed: 3752
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 49 KB/s], Decompressed: 3787
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 1042 KB/s], Decompressed: 3824
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 199 KB/s], Decompressed: 3872
Downloaded: 3924 file(s) [attempted 3924/8459 = 46%, 2316 KB/s], Decompressed: 3903
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 222 KB/s], Decompressed: 3958
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 273 KB/s], Decompressed: 3992
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 270 KB/s], Decompressed: 4030
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 446 KB/s], Decompressed: 4067
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 202 KB/s], Decompressed: 4108
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 102 KB/s], Decompressed: 4146
Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 318 KB/s], Decompressed: 4184
Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 256 KB/s], Decompressed: 4221
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 360 KB/s], Decompressed: 4262
Downloaded: 4307 file(s) [attempted 4307/8459 = 50%, 234 KB/s], Decompressed: 4293
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 211 KB/s], Decompressed: 4334
Downloaded: 4381 file(s) [attempted 4381/8459 = 51%, 643 KB/s], Decompressed: 4375
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 271 KB/s], Decompressed: 4416
Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 565 KB/s], Decompressed: 4440
Downloaded: 4502 file(s) [attempted 4502/8459 = 53%, 169 KB/s], Decompressed: 4488
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 1032 KB/s], Decompressed: 4533
Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 440 KB/s], Decompressed: 4574
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 41 KB/s], Decompressed: 4611
Downloaded: 4650 file(s) [attempted 4650/8459 = 54%, 792 KB/s], Decompressed: 4646
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 340 KB/s], Decompressed: 4680
Downloaded: 4725 file(s) [attempted 4725/8459 = 55%, 403 KB/s], Decompressed: 4721
Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 519 KB/s], Decompressed: 4762
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 101 KB/s], Decompressed: 4796
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1694 KB/s], Decompressed: 4834
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 33 KB/s], Decompressed: 4865
Downloaded: 4917 file(s) [attempted 4917/8459 = 58%, 535 KB/s], Decompressed: 4899
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 117 KB/s], Decompressed: 4923
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1046 KB/s], Decompressed: 4974
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 224 KB/s], Decompressed: 5026
Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 58 KB/s], Decompressed: 5063
Downloaded: 5108 file(s) [attempted 5108/8459 = 60%, 481 KB/s], Decompressed: 5097
Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 161 KB/s], Decompressed: 5139
Downloaded: 5186 file(s) [attempted 5186/8459 = 61%, 723 KB/s], Decompressed: 5183
Downloaded: 5224 file(s) [attempted 5224/8459 = 61%, 750 KB/s], Decompressed: 5207
Downloaded: 5259 file(s) [attempted 5259/8459 = 62%, 122 KB/s], Decompressed: 5255
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 203 KB/s], Decompressed: 5289
Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 82 KB/s], Decompressed: 5306
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 171 KB/s], Decompressed: 5364
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 58 KB/s], Decompressed: 5399
Downloaded: 5437 file(s) [attempted 5437/8459 = 64%, 229 KB/s], Decompressed: 5433
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 191 KB/s], Decompressed: 5477
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 87 KB/s], Decompressed: 5512
Downloaded: 5554 file(s) [attempted 5554/8459 = 65%, 371 KB/s], Decompressed: 5549
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 363 KB/s], Decompressed: 5583
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 25 KB/s], Decompressed: 5628
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 184 KB/s], Decompressed: 5666
Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 197 KB/s], Decompressed: 5690
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 94 KB/s], Decompressed: 5741
Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 78 KB/s], Decompressed: 5772
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 170 KB/s], Decompressed: 5820
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 181 KB/s], Decompressed: 5861
Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 329 KB/s], Decompressed: 5898
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 58 KB/s], Decompressed: 5933
Downloaded: 5971 file(s) [attempted 5971/8459 = 70%, 1825 KB/s], Decompressed: 5967
Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 161 KB/s], Decompressed: 6011
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 1860 KB/s], Decompressed: 6056
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 534 KB/s], Decompressed: 6087
Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 122 KB/s], Decompressed: 6121
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 673 KB/s], Decompressed: 6148
Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 405 KB/s], Decompressed: 6200
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 67 KB/s], Decompressed: 6241
Downloaded: 6272 file(s) [attempted 6272/8459 = 74%, 262 KB/s], Decompressed: 6268
Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 154 KB/s], Decompressed: 6302
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 95 KB/s], Decompressed: 6347
Downloaded: 6395 file(s) [attempted 6395/8459 = 75%, 185 KB/s], Decompressed: 6391
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 204 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 21 KB/s], Decompressed: 6456
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 537 KB/s], Decompressed: 6490
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 465 KB/s], Decompressed: 6535
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 370 KB/s], Decompressed: 6569
Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 132 KB/s], Decompressed: 6610
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 422 KB/s], Decompressed: 6648
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 215 KB/s], Decompressed: 6682
Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 166 KB/s], Decompressed: 6720
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 1361 KB/s], Decompressed: 6751
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 1260 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 31 KB/s], Decompressed: 6840
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 37 KB/s], Decompressed: 6874
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 32 KB/s], Decompressed: 6911
Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 45 KB/s], Decompressed: 6949
Downloaded: 6997 file(s) [attempted 6997/8459 = 82%, 1576 KB/s], Decompressed: 6990
Downloaded: 7035 file(s) [attempted 7035/8459 = 83%, 309 KB/s], Decompressed: 7032
Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 242 KB/s], Decompressed: 7069
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 353 KB/s], Decompressed: 7106
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 421 KB/s], Decompressed: 7141
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 684 KB/s], Decompressed: 7178
Downloaded: 7220 file(s) [attempted 7220/8459 = 85%, 305 KB/s], Decompressed: 7216
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 35 KB/s], Decompressed: 7250
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 34 KB/s], Decompressed: 7291
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 348 KB/s], Decompressed: 7332
Downloaded: 7375 file(s) [attempted 7375/8459 = 87%, 40 KB/s], Decompressed: 7367
Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 454 KB/s], Decompressed: 7401
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 114 KB/s], Decompressed: 7442
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 705 KB/s], Decompressed: 7469
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 369 KB/s], Decompressed: 7521
Downloaded: 7562 file(s) [attempted 7562/8459 = 89%, 290 KB/s], Decompressed: 7558
Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 207 KB/s], Decompressed: 7592
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 1431 KB/s], Decompressed: 7637
Downloaded: 7687 file(s) [attempted 7687/8459 = 90%, 291 KB/s], Decompressed: 7678
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 41 KB/s], Decompressed: 7719
Downloaded: 7759 file(s) [attempted 7759/8459 = 91%, 881 KB/s], Decompressed: 7753
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 483 KB/s], Decompressed: 7791
Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 809 KB/s], Decompressed: 7832
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 78 KB/s], Decompressed: 7870
Downloaded: 7911 file(s) [attempted 7911/8459 = 93%, 55 KB/s], Decompressed: 7907
Downloaded: 7942 file(s) [attempted 7942/8459 = 93%, 224 KB/s], Decompressed: 7938
Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 189 KB/s], Decompressed: 7979
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 554 KB/s], Decompressed: 8020
Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 116 KB/s], Decompressed: 8050
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 156 KB/s], Decompressed: 8092
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 998 KB/s], Decompressed: 8113
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 1039 KB/s], Decompressed: 8171
Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 134 KB/s], Decompressed: 8208
Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 753 KB/s], Decompressed: 8243
Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 118 KB/s], Decompressed: 8285
Downloaded: 8329 file(s) [attempted 8329/8459 = 98%, 623 KB/s], Decompressed: 8325
Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 697 KB/s], Decompressed: 8360
Downloaded: 8397 file(s) [attempted 8397/8459 = 99%, 127 KB/s], Decompressed: 8393
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 674 KB/s], Decompressed: 8427
Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 479 KB/s], Decompressed: 8448
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 19 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 19 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=239761
stdout:
✔ [3472/3478] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (55s)
✔ [3477/3499] Built PrimeNumberTheoremAnd.ZetaBounds (29s)
ℹ [3538/3549] Built PrimeNumberTheoremAnd.MediumPNT (28s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3550/3561] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (19s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (13s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3566/3576] Built PrimeNumberTheoremAnd.BorelCaratheodory (3.7s)
⚠ [3695/3721] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3807/3817] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.3s)
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3817/3823] Building PrimeNumberTheoremAnd.IEANTN.Mertens (14s)
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
⚠ [3882/3899] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4066/4101] 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`
⚠ [4119/4130] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (10s)
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`
ℹ [4165/4188] 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.
⚠ [4167/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`
✔ [4171/4188] Built PrimeNumberTheoremAnd.LaplaceInversion (10s)
✔ [4178/4188] Built PrimeNumberTheoremAnd.PerronFormula (6.8s)
⚠ [4186/4188] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
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=337362
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (514ms)
✔ [33/43] Built Cli:c.o (67ms)
✔ [3507/3519] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (15s)
✔ [3512/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (61s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3600/3614] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (66s)
✔ [3614/3637] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.8s)
⚠ [3626/3642] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3630/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (48s)
✔ [3636/3650] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.8s)
⚠ [3765/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3887/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.0s)
✖ [3897/3916] 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
⚠ [3969/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`
⚠ [4194/4239] 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`
⚠ [4269/4288] 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`
✔ [4279/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.2s)
ℹ [4332/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.
⚠ [4333/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`
✔ [4365/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.7s)
✔ [4368/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (22s)
⚠ [4391/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 (45s)
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_checkout exit 0
git fetch --depth 1 origin ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0 -> FETCH_HEAD
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-1040-source
Cloning into '/var/lib/apodeixis/repos/job-1040-source'...
git_checkout exit 128
git checkout ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
fatal: reference is not a tree: ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0
git_checkout exit 0
git checkout ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0 (after fetch)
Note: switching to 'ddabba3864bb2ddf08494bf1ef6b064b6b9f86e0'. 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 ddabba3 refactor(ResidueCalc): extract residue calculus from CH2 (#1537) (#1606)
lake_cache exit 0
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: 10 Downloaded: 33 file(s) [attempted 33/8459 = 0%, 30 KB/s], Decompressed: 29 Downloaded: 57 file(s) [attempted 57/8459 = 0%, 56 KB/s], Decompressed: 56 Downloaded: 78 file(s) [attempted 78/8459 = 0%, 101 KB/s], Decompressed: 72 Downloaded: 103 file(s) [attempted 103/8459 = 1%, 186 KB/s], Decompressed: 102 Downloaded: 138 file(s) [attempted 138/8459 = 1%, 380 KB/s], Decompressed: 134 Downloaded: 165 file(s) [attempted 165/8459 = 1%, 332 KB/s], Decompressed: 162 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 275 KB/s], Decompressed: 189 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 578 KB/s], Decompressed: 223 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 164 KB/s], Decompressed: 258 Downloaded: 295 file(s) [attempted 295/8459 = 3%, 175 KB/s], Decompressed: 292 Downloaded: 336 file(s) [attempted 336/8459 = 3%, 74 KB/s], Decompressed: 329 Downloaded: 374 file(s) [attempted 374/8459 = 4%, 107 KB/s], Decompressed: 367 Downloaded: 412 file(s) [attempted 412/8459 = 4%, 54 KB/s], Decompressed: 401 Downloaded: 453 file(s) [attempted 453/8459 = 5%, 284 KB/s], Decompressed: 443 Downloaded: 487 file(s) [attempted 487/8459 = 5%, 270 KB/s], Decompressed: 484 Downloaded: 525 file(s) [attempted 525/8459 = 6%, 570 KB/s], Decompressed: 521 Downloaded: 562 file(s) [attempted 562/8459 = 6%, 519 KB/s], Decompressed: 559 Downloaded: 604 file(s) [attempted 604/8459 = 7%, 154 KB/s], Decompressed: 597 Downloaded: 641 file(s) [attempted 641/8459 = 7%, 83 KB/s], Decompressed: 638 Downloaded: 679 file(s) [attempted 679/8459 = 8%, 66 KB/s], Decompressed: 675 Downloaded: 717 file(s) [attempted 717/8459 = 8%, 375 KB/s], Decompressed: 710 Downloaded: 758 file(s) [attempted 758/8459 = 8%, 147 KB/s], Decompressed: 754 Downloaded: 799 file(s) [attempted 799/8459 = 9%, 415 KB/s], Decompressed: 788 Downloaded: 836 file(s) [attempted 836/8459 = 9%, 479 KB/s], Decompressed: 833 Downloaded: 874 file(s) [attempted 874/8459 = 10%, 239 KB/s], Decompressed: 871 Downloaded: 915 file(s) [attempted 915/8459 = 10%, 871 KB/s], Decompressed: 912 Downloaded: 953 file(s) [attempted 953/8459 = 11%, 388 KB/s], Decompressed: 949 Downloaded: 994 file(s) [attempted 994/8459 = 11%, 145 KB/s], Decompressed: 984 Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 408 KB/s], Decompressed: 1018 Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 219 KB/s], Decompressed: 1062 Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 394 KB/s], Decompressed: 1104 Downloaded: 1145 file(s) [attempted 1145/8459 = 13%, 235 KB/s], Decompressed: 1134 Downloaded: 1182 file(s) [attempted 1182/8459 = 13%, 37 KB/s], Decompressed: 1179 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 165 KB/s], Decompressed: 1216 Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 55 KB/s], Decompressed: 1261 Downloaded: 1302 file(s) [attempted 1302/8459 = 15%, 179 KB/s], Decompressed: 1292 Downloaded: 1338 file(s) [attempted 1338/8459 = 15%, 1119 KB/s], Decompressed: 1329 Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 337 KB/s], Decompressed: 1370 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 1431 KB/s], Decompressed: 1415 Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 171 KB/s], Decompressed: 1459 Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 1237 KB/s], Decompressed: 1504 Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 142 KB/s], Decompressed: 1535 Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 398 KB/s], Decompressed: 1572 Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 193 KB/s], Decompressed: 1613 Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 216 KB/s], Decompressed: 1655 Downloaded: 1694 file(s) [attempted 1694/8459 = 20%, 1073 KB/s], Decompressed: 1689 Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 290 KB/s], Decompressed: 1726 Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 475 KB/s], Decompressed: 1767 Downloaded: 1815 file(s) [attempted 1815/8459 = 21%, 556 KB/s], Decompressed: 1809 Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 23 KB/s], Decompressed: 1850 Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 713 KB/s], Decompressed: 1887 Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 707 KB/s], Decompressed: 1925 Downloaded: 1966 file(s) [attempted 1966/8459 = 23%, 228 KB/s], Decompressed: 1963 Downloaded: 2007 file(s) [attempted 2007/8459 = 23%, 257 KB/s], Decompressed: 2000 Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 180 KB/s], Decompressed: 2024 Downloaded: 2075 file(s) [attempted 2075/8459 = 24%, 235 KB/s], Decompressed: 2072 Downloaded: 2117 file(s) [attempted 2117/8459 = 25%, 116 KB/s], Decompressed: 2113 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 495 KB/s], Decompressed: 2151 Downloaded: 2192 file(s) [attempted 2192/8459 = 25%, 397 KB/s], Decompressed: 2182 Downloaded: 2226 file(s) [attempted 2226/8459 = 26%, 38 KB/s], Decompressed: 2219 Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 456 KB/s], Decompressed: 2260 Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 1294 KB/s], Decompressed: 2305 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 63 KB/s], Decompressed: 2339 Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 127 KB/s], Decompressed: 2363 Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 220 KB/s], Decompressed: 2411 Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 167 KB/s], Decompressed: 2455 Downloaded: 2503 file(s) [attempted 2503/8459 = 29%, 85 KB/s], Decompressed: 2493 Downloaded: 2538 file(s) [attempted 2538/8459 = 30%, 567 KB/s], Decompressed: 2531 Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 685 KB/s], Decompressed: 2565 Downloaded: 2612 file(s) [attempted 2612/8459 = 30%, 69 KB/s], Decompressed: 2603 Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 135 KB/s], Decompressed: 2626 Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 56 KB/s], Decompressed: 2692 Downloaded: 2727 file(s) [attempted 2727/8459 = 32%, 158 KB/s], Decompressed: 2722 Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 334 KB/s], Decompressed: 2763 Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 61 KB/s], Decompressed: 2784 Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 1297 KB/s], Decompressed: 2846 Downloaded: 2880 file(s) [attempted 2880/8459 = 34%, 76 KB/s], Decompressed: 2876 Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 114 KB/s], Decompressed: 2911 Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 222 KB/s], Decompressed: 2952 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 98 KB/s], Decompressed: 2994 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 147 KB/s], Decompressed: 3023 Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 191 KB/s], Decompressed: 3061 Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 685 KB/s], Decompressed: 3102 Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 53 KB/s], Decompressed: 3140 Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 250 KB/s], Decompressed: 3181 Downloaded: 3222 file(s) [attempted 3222/8459 = 38%, 162 KB/s], Decompressed: 3201 Downloaded: 3255 file(s) [attempted 3255/8459 = 38%, 1300 KB/s], Decompressed: 3229 Downloaded: 3301 file(s) [attempted 3301/8459 = 39%, 64 KB/s], Decompressed: 3297 Downloaded: 3342 file(s) [attempted 3342/8459 = 39%, 467 KB/s], Decompressed: 3331 Downloaded: 3374 file(s) [attempted 3374/8459 = 39%, 634 KB/s], Decompressed: 3369 Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 240 KB/s], Decompressed: 3410 Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 228 KB/s], Decompressed: 3427 Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 355 KB/s], Decompressed: 3489 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 67 KB/s], Decompressed: 3527 Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 103 KB/s], Decompressed: 3561 Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 35 KB/s], Decompressed: 3602 Downloaded: 3642 file(s) [attempted 3642/8459 = 43%, 39 KB/s], Decompressed: 3636 Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 328 KB/s], Decompressed: 3674 Downloaded: 3720 file(s) [attempted 3720/8459 = 43%, 408 KB/s], Decompressed: 3715 Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 842 KB/s], Decompressed: 3752 Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 49 KB/s], Decompressed: 3787 Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 1042 KB/s], Decompressed: 3824 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 199 KB/s], Decompressed: 3872 Downloaded: 3924 file(s) [attempted 3924/8459 = 46%, 2316 KB/s], Decompressed: 3903 Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 222 KB/s], Decompressed: 3958 Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 273 KB/s], Decompressed: 3992 Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 270 KB/s], Decompressed: 4030 Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 446 KB/s], Decompressed: 4067 Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 202 KB/s], Decompressed: 4108 Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 102 KB/s], Decompressed: 4146 Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 318 KB/s], Decompressed: 4184 Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 256 KB/s], Decompressed: 4221 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 360 KB/s], Decompressed: 4262 Downloaded: 4307 file(s) [attempted 4307/8459 = 50%, 234 KB/s], Decompressed: 4293 Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 211 KB/s], Decompressed: 4334 Downloaded: 4381 file(s) [attempted 4381/8459 = 51%, 643 KB/s], Decompressed: 4375 Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 271 KB/s], Decompressed: 4416 Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 565 KB/s], Decompressed: 4440 Downloaded: 4502 file(s) [attempted 4502/8459 = 53%, 169 KB/s], Decompressed: 4488 Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 1032 KB/s], Decompressed: 4533 Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 440 KB/s], Decompressed: 4574 Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 41 KB/s], Decompressed: 4611 Downloaded: 4650 file(s) [attempted 4650/8459 = 54%, 792 KB/s], Decompressed: 4646 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 340 KB/s], Decompressed: 4680 Downloaded: 4725 file(s) [attempted 4725/8459 = 55%, 403 KB/s], Decompressed: 4721 Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 519 KB/s], Decompressed: 4762 Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 101 KB/s], Decompressed: 4796 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1694 KB/s], Decompressed: 4834 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 33 KB/s], Decompressed: 4865 Downloaded: 4917 file(s) [attempted 4917/8459 = 58%, 535 KB/s], Decompressed: 4899 Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 117 KB/s], Decompressed: 4923 Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1046 KB/s], Decompressed: 4974 Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 224 KB/s], Decompressed: 5026 Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 58 KB/s], Decompressed: 5063 Downloaded: 5108 file(s) [attempted 5108/8459 = 60%, 481 KB/s], Decompressed: 5097 Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 161 KB/s], Decompressed: 5139 Downloaded: 5186 file(s) [attempted 5186/8459 = 61%, 723 KB/s], Decompressed: 5183 Downloaded: 5224 file(s) [attempted 5224/8459 = 61%, 750 KB/s], Decompressed: 5207 Downloaded: 5259 file(s) [attempted 5259/8459 = 62%, 122 KB/s], Decompressed: 5255 Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 203 KB/s], Decompressed: 5289 Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 82 KB/s], Decompressed: 5306 Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 171 KB/s], Decompressed: 5364 Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 58 KB/s], Decompressed: 5399 Downloaded: 5437 file(s) [attempted 5437/8459 = 64%, 229 KB/s], Decompressed: 5433 Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 191 KB/s], Decompressed: 5477 Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 87 KB/s], Decompressed: 5512 Downloaded: 5554 file(s) [attempted 5554/8459 = 65%, 371 KB/s], Decompressed: 5549 Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 363 KB/s], Decompressed: 5583 Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 25 KB/s], Decompressed: 5628 Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 184 KB/s], Decompressed: 5666 Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 197 KB/s], Decompressed: 5690 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 94 KB/s], Decompressed: 5741 Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 78 KB/s], Decompressed: 5772 Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 170 KB/s], Decompressed: 5820 Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 181 KB/s], Decompressed: 5861 Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 329 KB/s], Decompressed: 5898 Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 58 KB/s], Decompressed: 5933 Downloaded: 5971 file(s) [attempted 5971/8459 = 70%, 1825 KB/s], Decompressed: 5967 Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 161 KB/s], Decompressed: 6011 Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 1860 KB/s], Decompressed: 6056 Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 534 KB/s], Decompressed: 6087 Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 122 KB/s], Decompressed: 6121 Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 673 KB/s], Decompressed: 6148 Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 405 KB/s], Decompressed: 6200 Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 67 KB/s], Decompressed: 6241 Downloaded: 6272 file(s) [attempted 6272/8459 = 74%, 262 KB/s], Decompressed: 6268 Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 154 KB/s], Decompressed: 6302 Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 95 KB/s], Decompressed: 6347 Downloaded: 6395 file(s) [attempted 6395/8459 = 75%, 185 KB/s], Decompressed: 6391 Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 204 KB/s], Decompressed: 6425 Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 21 KB/s], Decompressed: 6456 Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 537 KB/s], Decompressed: 6490 Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 465 KB/s], Decompressed: 6535 Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 370 KB/s], Decompressed: 6569 Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 132 KB/s], Decompressed: 6610 Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 422 KB/s], Decompressed: 6648 Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 215 KB/s], Decompressed: 6682 Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 166 KB/s], Decompressed: 6720 Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 1361 KB/s], Decompressed: 6751 Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 1260 KB/s], Decompressed: 6802 Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 31 KB/s], Decompressed: 6840 Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 37 KB/s], Decompressed: 6874 Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 32 KB/s], Decompressed: 6911 Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 45 KB/s], Decompressed: 6949 Downloaded: 6997 file(s) [attempted 6997/8459 = 82%, 1576 KB/s], Decompressed: 6990 Downloaded: 7035 file(s) [attempted 7035/8459 = 83%, 309 KB/s], Decompressed: 7032 Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 242 KB/s], Decompressed: 7069 Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 353 KB/s], Decompressed: 7106 Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 421 KB/s], Decompressed: 7141 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 684 KB/s], Decompressed: 7178 Downloaded: 7220 file(s) [attempted 7220/8459 = 85%, 305 KB/s], Decompressed: 7216 Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 35 KB/s], Decompressed: 7250 Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 34 KB/s], Decompressed: 7291 Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 348 KB/s], Decompressed: 7332 Downloaded: 7375 file(s) [attempted 7375/8459 = 87%, 40 KB/s], Decompressed: 7367 Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 454 KB/s], Decompressed: 7401 Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 114 KB/s], Decompressed: 7442 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 705 KB/s], Decompressed: 7469 Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 369 KB/s], Decompressed: 7521 Downloaded: 7562 file(s) [attempted 7562/8459 = 89%, 290 KB/s], Decompressed: 7558 Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 207 KB/s], Decompressed: 7592 Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 1431 KB/s], Decompressed: 7637 Downloaded: 7687 file(s) [attempted 7687/8459 = 90%, 291 KB/s], Decompressed: 7678 Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 41 KB/s], Decompressed: 7719 Downloaded: 7759 file(s) [attempted 7759/8459 = 91%, 881 KB/s], Decompressed: 7753 Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 483 KB/s], Decompressed: 7791 Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 809 KB/s], Decompressed: 7832 Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 78 KB/s], Decompressed: 7870 Downloaded: 7911 file(s) [attempted 7911/8459 = 93%, 55 KB/s], Decompressed: 7907 Downloaded: 7942 file(s) [attempted 7942/8459 = 93%, 224 KB/s], Decompressed: 7938 Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 189 KB/s], Decompressed: 7979 Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 554 KB/s], Decompressed: 8020 Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 116 KB/s], Decompressed: 8050 Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 156 KB/s], Decompressed: 8092 Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 998 KB/s], Decompressed: 8113 Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 1039 KB/s], Decompressed: 8171 Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 134 KB/s], Decompressed: 8208 Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 753 KB/s], Decompressed: 8243 Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 118 KB/s], Decompressed: 8285 Downloaded: 8329 file(s) [attempted 8329/8459 = 98%, 623 KB/s], Decompressed: 8325 Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 697 KB/s], Decompressed: 8360 Downloaded: 8397 file(s) [attempted 8397/8459 = 99%, 127 KB/s], Decompressed: 8393 Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 674 KB/s], Decompressed: 8427 Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 479 KB/s], Decompressed: 8448 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 19 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 19 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [3472/3478] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (55s)
✔ [3477/3499] Built PrimeNumberTheoremAnd.ZetaBounds (29s)
ℹ [3538/3549] Built PrimeNumberTheoremAnd.MediumPNT (28s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3550/3561] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (19s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (13s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3566/3576] Built PrimeNumberTheoremAnd.BorelCaratheodory (3.7s)
⚠ [3695/3721] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3807/3817] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.3s)
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3817/3823] Building PrimeNumberTheoremAnd.IEANTN.Mertens (14s)
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
⚠ [3882/3899] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4066/4101] 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`
⚠ [4119/4130] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (10s)
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`
ℹ [4165/4188] 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.
⚠ [4167/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`
✔ [4171/4188] Built PrimeNumberTheoremAnd.LaplaceInversion (10s)
✔ [4178/4188] Built PrimeNumberTheoremAnd.PerronFormula (6.8s)
⚠ [4186/4188] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
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
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (514ms)
✔ [33/43] Built Cli:c.o (67ms)
✔ [3507/3519] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (15s)
✔ [3512/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (61s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3600/3614] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (66s)
✔ [3614/3637] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.8s)
⚠ [3626/3642] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3630/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (48s)
✔ [3636/3650] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.8s)
⚠ [3765/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3887/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.0s)
✖ [3897/3916] 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
⚠ [3969/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`
⚠ [4194/4239] 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`
⚠ [4269/4288] 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`
✔ [4279/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.2s)
ℹ [4332/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.
⚠ [4333/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`
✔ [4365/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.7s)
✔ [4368/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (22s)
⚠ [4391/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 (45s)
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