Verification run
Run 145
failed commit
ab37dadcb078 toolchain lean-v4-30-0 prover lean took 20m 37s · finished 6d 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-1037-source
exit_code=Some(0) duration_ms=1934
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1037-source'...
$ git checkout ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
exit_code=Some(128) duration_ms=2
stderr:
fatal: reference is not a tree: ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
$ git fetch --depth 1 origin ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
exit_code=Some(0) duration_ms=942
stderr:
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
* branch ab37dadcb0789525ac90b7dc9064cabb2eaa3c92 -> FETCH_HEAD
$ git checkout ab37dadcb0789525ac90b7dc9064cabb2eaa3c92 (after fetch)
exit_code=Some(0) duration_ms=49
stderr:
Note: switching to 'ab37dadcb0789525ac90b7dc9064cabb2eaa3c92'.
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 ab37dad feat(laplace): cpow inversion bridge to truncated Fourier reconstruction (#1605)
Resolved source revision: ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=ab37dadcb0789525ac90b7dc9064cabb2eaa3c92 provenance={"branch":"main","checked_out_revision":"ab37dadcb0789525ac90b7dc9064cabb2eaa3c92","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"ab37dadcb0789525ac90b7dc9064cabb2eaa3c92","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=84478
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%, 15 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 2 KB/s], Decompressed: 11
Downloaded: 32 file(s) [attempted 32/8459 = 0%, 12 KB/s], Decompressed: 16
Downloaded: 59 file(s) [attempted 59/8459 = 0%, 28 KB/s], Decompressed: 16
Downloaded: 79 file(s) [attempted 79/8459 = 0%, 119 KB/s], Decompressed: 27
Downloaded: 115 file(s) [attempted 115/8459 = 1%, 60 KB/s], Decompressed: 27
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 358 KB/s], Decompressed: 78
Downloaded: 179 file(s) [attempted 179/8459 = 2%, 487 KB/s], Decompressed: 175
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 245 KB/s], Decompressed: 186
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 160 KB/s], Decompressed: 186
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 71 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 147 KB/s], Decompressed: 306
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 81 KB/s], Decompressed: 343
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 76 KB/s], Decompressed: 384
Downloaded: 419 file(s) [attempted 419/8459 = 4%, 431 KB/s], Decompressed: 415
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 249 KB/s], Decompressed: 419
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 336 KB/s], Decompressed: 426
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 165 KB/s], Decompressed: 501
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 31 KB/s], Decompressed: 501
Downloaded: 621 file(s) [attempted 621/8459 = 7%, 40 KB/s], Decompressed: 514
Downloaded: 655 file(s) [attempted 655/8459 = 7%, 75 KB/s], Decompressed: 514
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 194 KB/s], Decompressed: 600
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 431 KB/s], Decompressed: 600
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 181 KB/s], Decompressed: 686
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 29 KB/s], Decompressed: 802
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 134 KB/s], Decompressed: 812
Downloaded: 891 file(s) [attempted 891/8459 = 10%, 210 KB/s], Decompressed: 812
Downloaded: 932 file(s) [attempted 932/8459 = 11%, 78 KB/s], Decompressed: 929
Downloaded: 973 file(s) [attempted 973/8459 = 11%, 525 KB/s], Decompressed: 932
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 124 KB/s], Decompressed: 932
Downloaded: 1049 file(s) [attempted 1049/8459 = 12%, 615 KB/s], Decompressed: 939
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 443 KB/s], Decompressed: 939
Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 100 KB/s], Decompressed: 939
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 553 KB/s], Decompressed: 939
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 167 KB/s], Decompressed: 1021
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 64 KB/s], Decompressed: 1021
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 821 KB/s], Decompressed: 1021
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 295 KB/s], Decompressed: 1209
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 774 KB/s], Decompressed: 1209
Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 119 KB/s], Decompressed: 1405
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 695 KB/s], Decompressed: 1442
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 51 KB/s], Decompressed: 1480
Downloaded: 1521 file(s) [attempted 1521/8459 = 17%, 71 KB/s], Decompressed: 1518
Downloaded: 1562 file(s) [attempted 1562/8459 = 18%, 499 KB/s], Decompressed: 1531
Downloaded: 1600 file(s) [attempted 1600/8459 = 18%, 190 KB/s], Decompressed: 1531
Downloaded: 1639 file(s) [attempted 1639/8459 = 19%, 27 KB/s], Decompressed: 1617
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 545 KB/s], Decompressed: 1661
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 208 KB/s], Decompressed: 1699
Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 436 KB/s], Decompressed: 1754
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 892 KB/s], Decompressed: 1795
Downloaded: 1838 file(s) [attempted 1838/8459 = 21%, 204 KB/s], Decompressed: 1829
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 691 KB/s], Decompressed: 1860
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 74 KB/s], Decompressed: 1901
Downloaded: 1945 file(s) [attempted 1945/8459 = 22%, 113 KB/s], Decompressed: 1942
Downloaded: 1987 file(s) [attempted 1987/8459 = 23%, 127 KB/s], Decompressed: 1980
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 164 KB/s], Decompressed: 1980
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 320 KB/s], Decompressed: 1980
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 51 KB/s], Decompressed: 2058
Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 630 KB/s], Decompressed: 2058
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 487 KB/s], Decompressed: 2058
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 257 KB/s], Decompressed: 2058
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 649 KB/s], Decompressed: 2058
Downloaded: 2292 file(s) [attempted 2292/8459 = 27%, 955 KB/s], Decompressed: 2058
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 147 KB/s], Decompressed: 2058
Downloaded: 2370 file(s) [attempted 2370/8459 = 28%, 224 KB/s], Decompressed: 2075
Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 253 KB/s], Decompressed: 2075
Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 234 KB/s], Decompressed: 2336
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 133 KB/s], Decompressed: 2462
Downloaded: 2527 file(s) [attempted 2527/8459 = 29%, 1059 KB/s], Decompressed: 2462
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 619 KB/s], Decompressed: 2472
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 110 KB/s], Decompressed: 2568
Downloaded: 2644 file(s) [attempted 2644/8459 = 31%, 24 KB/s], Decompressed: 2568
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 491 KB/s], Decompressed: 2671
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 235 KB/s], Decompressed: 2705
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 98 KB/s], Decompressed: 2709
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1178 KB/s], Decompressed: 2709
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 66 KB/s], Decompressed: 2822
Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 22 KB/s], Decompressed: 2842
Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 216 KB/s], Decompressed: 2842
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 904 KB/s], Decompressed: 2846
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 915 KB/s], Decompressed: 2846
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 21 KB/s], Decompressed: 2924
Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 193 KB/s], Decompressed: 2924
Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 308 KB/s], Decompressed: 3010
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 419 KB/s], Decompressed: 3010
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 196 KB/s], Decompressed: 3099
Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 647 KB/s], Decompressed: 3225
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 498 KB/s], Decompressed: 3243
Downloaded: 3308 file(s) [attempted 3308/8459 = 39%, 140 KB/s], Decompressed: 3243
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 718 KB/s], Decompressed: 3345
Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 1356 KB/s], Decompressed: 3369
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 45 KB/s], Decompressed: 3369
Downloaded: 3462 file(s) [attempted 3462/8459 = 40%, 488 KB/s], Decompressed: 3376
Downloaded: 3503 file(s) [attempted 3503/8459 = 41%, 162 KB/s], Decompressed: 3376
Downloaded: 3542 file(s) [attempted 3542/8459 = 41%, 148 KB/s], Decompressed: 3451
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 572 KB/s], Decompressed: 3451
Downloaded: 3619 file(s) [attempted 3619/8459 = 42%, 754 KB/s], Decompressed: 3451
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 1378 KB/s], Decompressed: 3650
Downloaded: 3698 file(s) [attempted 3698/8459 = 43%, 166 KB/s], Decompressed: 3694
Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 182 KB/s], Decompressed: 3732
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 98 KB/s], Decompressed: 3749
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 47 KB/s], Decompressed: 3749
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 699 KB/s], Decompressed: 3752
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 37 KB/s], Decompressed: 3886
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 418 KB/s], Decompressed: 3920
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 99 KB/s], Decompressed: 3958
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 273 KB/s], Decompressed: 3999
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 73 KB/s], Decompressed: 4043
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 55 KB/s], Decompressed: 4084
Downloaded: 4127 file(s) [attempted 4127/8459 = 48%, 91 KB/s], Decompressed: 4115
Downloaded: 4157 file(s) [attempted 4157/8459 = 49%, 44 KB/s], Decompressed: 4153
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 710 KB/s], Decompressed: 4191
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 37 KB/s], Decompressed: 4232
Downloaded: 4277 file(s) [attempted 4277/8459 = 50%, 322 KB/s], Decompressed: 4269
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 824 KB/s], Decompressed: 4307
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 223 KB/s], Decompressed: 4341
Downloaded: 4389 file(s) [attempted 4389/8459 = 51%, 427 KB/s], Decompressed: 4348
Downloaded: 4434 file(s) [attempted 4434/8459 = 52%, 124 KB/s], Decompressed: 4348
Downloaded: 4475 file(s) [attempted 4475/8459 = 52%, 184 KB/s], Decompressed: 4447
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 177 KB/s], Decompressed: 4447
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 150 KB/s], Decompressed: 4454
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 154 KB/s], Decompressed: 4581
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 93 KB/s], Decompressed: 4625
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 1088 KB/s], Decompressed: 4659
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 24 KB/s], Decompressed: 4697
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 241 KB/s], Decompressed: 4697
Downloaded: 4783 file(s) [attempted 4783/8459 = 56%, 135 KB/s], Decompressed: 4697
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 204 KB/s], Decompressed: 4820
Downloaded: 4860 file(s) [attempted 4860/8459 = 57%, 1421 KB/s], Decompressed: 4851
Downloaded: 4897 file(s) [attempted 4897/8459 = 57%, 515 KB/s], Decompressed: 4889
Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 353 KB/s], Decompressed: 4926
Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 68 KB/s], Decompressed: 4926
Downloaded: 5019 file(s) [attempted 5019/8459 = 59%, 39 KB/s], Decompressed: 4933
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 52 KB/s], Decompressed: 4933
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 548 KB/s], Decompressed: 4933
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 348 KB/s], Decompressed: 5128
Downloaded: 5175 file(s) [attempted 5175/8459 = 61%, 157 KB/s], Decompressed: 5166
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 178 KB/s], Decompressed: 5176
Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 137 KB/s], Decompressed: 5176
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 378 KB/s], Decompressed: 5180
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 690 KB/s], Decompressed: 5180
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 670 KB/s], Decompressed: 5260
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 230 KB/s], Decompressed: 5260
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 774 KB/s], Decompressed: 5440
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 150 KB/s], Decompressed: 5481
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 603 KB/s], Decompressed: 5518
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 36 KB/s], Decompressed: 5563
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 663 KB/s], Decompressed: 5601
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 46 KB/s], Decompressed: 5607
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 750 KB/s], Decompressed: 5607
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 284 KB/s], Decompressed: 5611
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 290 KB/s], Decompressed: 5611
Downloaded: 5803 file(s) [attempted 5803/8459 = 68%, 477 KB/s], Decompressed: 5792
Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 633 KB/s], Decompressed: 5826
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 155 KB/s], Decompressed: 5874
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 693 KB/s], Decompressed: 5888
Downloaded: 5958 file(s) [attempted 5958/8459 = 70%, 71 KB/s], Decompressed: 5888
Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 140 KB/s], Decompressed: 5977
Downloaded: 6035 file(s) [attempted 6035/8459 = 71%, 356 KB/s], Decompressed: 6001
Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 213 KB/s], Decompressed: 6001
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 126 KB/s], Decompressed: 6104
Downloaded: 6146 file(s) [attempted 6146/8459 = 72%, 1041 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 653 KB/s], Decompressed: 6182
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 127 KB/s], Decompressed: 6182
Downloaded: 6282 file(s) [attempted 6282/8459 = 74%, 50 KB/s], Decompressed: 6182
Downloaded: 6319 file(s) [attempted 6319/8459 = 74%, 332 KB/s], Decompressed: 6182
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 307 KB/s], Decompressed: 6189
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 67 KB/s], Decompressed: 6189
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 301 KB/s], Decompressed: 6189
Downloaded: 6480 file(s) [attempted 6480/8459 = 76%, 227 KB/s], Decompressed: 6343
Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 109 KB/s], Decompressed: 6343
Downloaded: 6559 file(s) [attempted 6559/8459 = 77%, 157 KB/s], Decompressed: 6446
Downloaded: 6596 file(s) [attempted 6596/8459 = 77%, 127 KB/s], Decompressed: 6446
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 245 KB/s], Decompressed: 6531
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 131 KB/s], Decompressed: 6665
Downloaded: 6720 file(s) [attempted 6720/8459 = 79%, 153 KB/s], Decompressed: 6665
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 435 KB/s], Decompressed: 6668
Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 548 KB/s], Decompressed: 6788
Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 233 KB/s], Decompressed: 6822
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 200 KB/s], Decompressed: 6867
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 210 KB/s], Decompressed: 6891
Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 163 KB/s], Decompressed: 6891
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 155 KB/s], Decompressed: 6898
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 310 KB/s], Decompressed: 6898
Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 153 KB/s], Decompressed: 6898
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 71 KB/s], Decompressed: 6898
Downloaded: 7132 file(s) [attempted 7132/8459 = 84%, 325 KB/s], Decompressed: 6898
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 287 KB/s], Decompressed: 6898
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 644 KB/s], Decompressed: 6898
Downloaded: 7254 file(s) [attempted 7254/8459 = 85%, 1384 KB/s], Decompressed: 6980
Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 262 KB/s], Decompressed: 6980
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 75 KB/s], Decompressed: 6980
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 373 KB/s], Decompressed: 7219
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 112 KB/s], Decompressed: 7219
Downloaded: 7454 file(s) [attempted 7454/8459 = 88%, 223 KB/s], Decompressed: 7442
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 140 KB/s], Decompressed: 7486
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 47 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 889 KB/s], Decompressed: 7551
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 329 KB/s], Decompressed: 7551
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 277 KB/s], Decompressed: 7633
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 225 KB/s], Decompressed: 7633
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 141 KB/s], Decompressed: 7633
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 480 KB/s], Decompressed: 7647
Downloaded: 7805 file(s) [attempted 7805/8459 = 92%, 724 KB/s], Decompressed: 7647
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 452 KB/s], Decompressed: 7818
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 776 KB/s], Decompressed: 7876
Downloaded: 7928 file(s) [attempted 7928/8459 = 93%, 1059 KB/s], Decompressed: 7924
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 93 KB/s], Decompressed: 7959
Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 150 KB/s], Decompressed: 7989
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 28 KB/s], Decompressed: 7989
Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 455 KB/s], Decompressed: 7993
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 357 KB/s], Decompressed: 8075
Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 627 KB/s], Decompressed: 8075
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 229 KB/s], Decompressed: 8191
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 272 KB/s], Decompressed: 8215
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 266 KB/s], Decompressed: 8215
Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 159 KB/s], Decompressed: 8219
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 1111 KB/s], Decompressed: 8219
Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 52 KB/s], Decompressed: 8219
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 642 KB/s], Decompressed: 8219
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 263 KB/s], Decompressed: 8304
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 263 KB/s], Decompressed: 8304
$ lake build
exit_code=Some(1) duration_ms=308453
stdout:
ℹ [3536/3546] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3571] 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`
⚠ [3694/3715] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3816/3819] Building PrimeNumberTheoremAnd.IEANTN.Mertens (177s)
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
⚠ [3885/3895] 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`
⚠ [4125/4166] 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`
ℹ [4164/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.
⚠ [4166/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`
✔ [4173/4188] Built PrimeNumberTheoremAnd.LaplaceInversion (13s)
✔ [4185/4188] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (10s)
⚠ [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=111056
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (4.5s)
✔ [25/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (538ms)
✔ [33/41] Built Cli:c.o (66ms)
ℹ [3603/3641] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3628/3680] 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`
⚠ [3764/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3890/3901] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3896/3901] Building PrimeNumberTheoremAnd.IEANTN.Mertens (13s)
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
⚠ [3963/3985] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4194/4211] 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`
⚠ [4270/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`
ℹ [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`
✔ [4367/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (7.7s)
✔ [4391/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (5.8s)
⚠ [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 (47s)
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
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-1037-source
Cloning into '/var/lib/apodeixis/repos/job-1037-source'...
git_checkout exit 128
git checkout ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
fatal: reference is not a tree: ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
git_checkout exit 0
git fetch --depth 1 origin ab37dadcb0789525ac90b7dc9064cabb2eaa3c92
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch ab37dadcb0789525ac90b7dc9064cabb2eaa3c92 -> FETCH_HEAD
git_checkout exit 0
git checkout ab37dadcb0789525ac90b7dc9064cabb2eaa3c92 (after fetch)
Note: switching to 'ab37dadcb0789525ac90b7dc9064cabb2eaa3c92'. 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 ab37dad feat(laplace): cpow inversion bridge to truncated Fourier reconstruction (#1605)
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%, 15 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 2 KB/s], Decompressed: 11 Downloaded: 32 file(s) [attempted 32/8459 = 0%, 12 KB/s], Decompressed: 16 Downloaded: 59 file(s) [attempted 59/8459 = 0%, 28 KB/s], Decompressed: 16 Downloaded: 79 file(s) [attempted 79/8459 = 0%, 119 KB/s], Decompressed: 27 Downloaded: 115 file(s) [attempted 115/8459 = 1%, 60 KB/s], Decompressed: 27 Downloaded: 141 file(s) [attempted 141/8459 = 1%, 358 KB/s], Decompressed: 78 Downloaded: 179 file(s) [attempted 179/8459 = 2%, 487 KB/s], Decompressed: 175 Downloaded: 206 file(s) [attempted 206/8459 = 2%, 245 KB/s], Decompressed: 186 Downloaded: 237 file(s) [attempted 237/8459 = 2%, 160 KB/s], Decompressed: 186 Downloaded: 275 file(s) [attempted 275/8459 = 3%, 71 KB/s], Decompressed: 268 Downloaded: 312 file(s) [attempted 312/8459 = 3%, 147 KB/s], Decompressed: 306 Downloaded: 353 file(s) [attempted 353/8459 = 4%, 81 KB/s], Decompressed: 343 Downloaded: 388 file(s) [attempted 388/8459 = 4%, 76 KB/s], Decompressed: 384 Downloaded: 419 file(s) [attempted 419/8459 = 4%, 431 KB/s], Decompressed: 415 Downloaded: 460 file(s) [attempted 460/8459 = 5%, 249 KB/s], Decompressed: 419 Downloaded: 501 file(s) [attempted 501/8459 = 5%, 336 KB/s], Decompressed: 426 Downloaded: 545 file(s) [attempted 545/8459 = 6%, 165 KB/s], Decompressed: 501 Downloaded: 583 file(s) [attempted 583/8459 = 6%, 31 KB/s], Decompressed: 501 Downloaded: 621 file(s) [attempted 621/8459 = 7%, 40 KB/s], Decompressed: 514 Downloaded: 655 file(s) [attempted 655/8459 = 7%, 75 KB/s], Decompressed: 514 Downloaded: 696 file(s) [attempted 696/8459 = 8%, 194 KB/s], Decompressed: 600 Downloaded: 734 file(s) [attempted 734/8459 = 8%, 431 KB/s], Decompressed: 600 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 181 KB/s], Decompressed: 686 Downloaded: 806 file(s) [attempted 806/8459 = 9%, 29 KB/s], Decompressed: 802 Downloaded: 847 file(s) [attempted 847/8459 = 10%, 134 KB/s], Decompressed: 812 Downloaded: 891 file(s) [attempted 891/8459 = 10%, 210 KB/s], Decompressed: 812 Downloaded: 932 file(s) [attempted 932/8459 = 11%, 78 KB/s], Decompressed: 929 Downloaded: 973 file(s) [attempted 973/8459 = 11%, 525 KB/s], Decompressed: 932 Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 124 KB/s], Decompressed: 932 Downloaded: 1049 file(s) [attempted 1049/8459 = 12%, 615 KB/s], Decompressed: 939 Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 443 KB/s], Decompressed: 939 Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 100 KB/s], Decompressed: 939 Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 553 KB/s], Decompressed: 939 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 167 KB/s], Decompressed: 1021 Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 64 KB/s], Decompressed: 1021 Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 821 KB/s], Decompressed: 1021 Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 295 KB/s], Decompressed: 1209 Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 774 KB/s], Decompressed: 1209 Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 119 KB/s], Decompressed: 1405 Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 695 KB/s], Decompressed: 1442 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 51 KB/s], Decompressed: 1480 Downloaded: 1521 file(s) [attempted 1521/8459 = 17%, 71 KB/s], Decompressed: 1518 Downloaded: 1562 file(s) [attempted 1562/8459 = 18%, 499 KB/s], Decompressed: 1531 Downloaded: 1600 file(s) [attempted 1600/8459 = 18%, 190 KB/s], Decompressed: 1531 Downloaded: 1639 file(s) [attempted 1639/8459 = 19%, 27 KB/s], Decompressed: 1617 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 545 KB/s], Decompressed: 1661 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 208 KB/s], Decompressed: 1699 Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 436 KB/s], Decompressed: 1754 Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 892 KB/s], Decompressed: 1795 Downloaded: 1838 file(s) [attempted 1838/8459 = 21%, 204 KB/s], Decompressed: 1829 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 691 KB/s], Decompressed: 1860 Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 74 KB/s], Decompressed: 1901 Downloaded: 1945 file(s) [attempted 1945/8459 = 22%, 113 KB/s], Decompressed: 1942 Downloaded: 1987 file(s) [attempted 1987/8459 = 23%, 127 KB/s], Decompressed: 1980 Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 164 KB/s], Decompressed: 1980 Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 320 KB/s], Decompressed: 1980 Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 51 KB/s], Decompressed: 2058 Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 630 KB/s], Decompressed: 2058 Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 487 KB/s], Decompressed: 2058 Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 257 KB/s], Decompressed: 2058 Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 649 KB/s], Decompressed: 2058 Downloaded: 2292 file(s) [attempted 2292/8459 = 27%, 955 KB/s], Decompressed: 2058 Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 147 KB/s], Decompressed: 2058 Downloaded: 2370 file(s) [attempted 2370/8459 = 28%, 224 KB/s], Decompressed: 2075 Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 253 KB/s], Decompressed: 2075 Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 234 KB/s], Decompressed: 2336 Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 133 KB/s], Decompressed: 2462 Downloaded: 2527 file(s) [attempted 2527/8459 = 29%, 1059 KB/s], Decompressed: 2462 Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 619 KB/s], Decompressed: 2472 Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 110 KB/s], Decompressed: 2568 Downloaded: 2644 file(s) [attempted 2644/8459 = 31%, 24 KB/s], Decompressed: 2568 Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 491 KB/s], Decompressed: 2671 Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 235 KB/s], Decompressed: 2705 Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 98 KB/s], Decompressed: 2709 Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1178 KB/s], Decompressed: 2709 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 66 KB/s], Decompressed: 2822 Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 22 KB/s], Decompressed: 2842 Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 216 KB/s], Decompressed: 2842 Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 904 KB/s], Decompressed: 2846 Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 915 KB/s], Decompressed: 2846 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 21 KB/s], Decompressed: 2924 Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 193 KB/s], Decompressed: 2924 Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 308 KB/s], Decompressed: 3010 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 419 KB/s], Decompressed: 3010 Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 196 KB/s], Decompressed: 3099 Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 647 KB/s], Decompressed: 3225 Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 498 KB/s], Decompressed: 3243 Downloaded: 3308 file(s) [attempted 3308/8459 = 39%, 140 KB/s], Decompressed: 3243 Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 718 KB/s], Decompressed: 3345 Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 1356 KB/s], Decompressed: 3369 Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 45 KB/s], Decompressed: 3369 Downloaded: 3462 file(s) [attempted 3462/8459 = 40%, 488 KB/s], Decompressed: 3376 Downloaded: 3503 file(s) [attempted 3503/8459 = 41%, 162 KB/s], Decompressed: 3376 Downloaded: 3542 file(s) [attempted 3542/8459 = 41%, 148 KB/s], Decompressed: 3451 Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 572 KB/s], Decompressed: 3451 Downloaded: 3619 file(s) [attempted 3619/8459 = 42%, 754 KB/s], Decompressed: 3451 Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 1378 KB/s], Decompressed: 3650 Downloaded: 3698 file(s) [attempted 3698/8459 = 43%, 166 KB/s], Decompressed: 3694 Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 182 KB/s], Decompressed: 3732 Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 98 KB/s], Decompressed: 3749 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 47 KB/s], Decompressed: 3749 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 699 KB/s], Decompressed: 3752 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 37 KB/s], Decompressed: 3886 Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 418 KB/s], Decompressed: 3920 Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 99 KB/s], Decompressed: 3958 Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 273 KB/s], Decompressed: 3999 Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 73 KB/s], Decompressed: 4043 Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 55 KB/s], Decompressed: 4084 Downloaded: 4127 file(s) [attempted 4127/8459 = 48%, 91 KB/s], Decompressed: 4115 Downloaded: 4157 file(s) [attempted 4157/8459 = 49%, 44 KB/s], Decompressed: 4153 Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 710 KB/s], Decompressed: 4191 Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 37 KB/s], Decompressed: 4232 Downloaded: 4277 file(s) [attempted 4277/8459 = 50%, 322 KB/s], Decompressed: 4269 Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 824 KB/s], Decompressed: 4307 Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 223 KB/s], Decompressed: 4341 Downloaded: 4389 file(s) [attempted 4389/8459 = 51%, 427 KB/s], Decompressed: 4348 Downloaded: 4434 file(s) [attempted 4434/8459 = 52%, 124 KB/s], Decompressed: 4348 Downloaded: 4475 file(s) [attempted 4475/8459 = 52%, 184 KB/s], Decompressed: 4447 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 177 KB/s], Decompressed: 4447 Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 150 KB/s], Decompressed: 4454 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 154 KB/s], Decompressed: 4581 Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 93 KB/s], Decompressed: 4625 Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 1088 KB/s], Decompressed: 4659 Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 24 KB/s], Decompressed: 4697 Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 241 KB/s], Decompressed: 4697 Downloaded: 4783 file(s) [attempted 4783/8459 = 56%, 135 KB/s], Decompressed: 4697 Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 204 KB/s], Decompressed: 4820 Downloaded: 4860 file(s) [attempted 4860/8459 = 57%, 1421 KB/s], Decompressed: 4851 Downloaded: 4897 file(s) [attempted 4897/8459 = 57%, 515 KB/s], Decompressed: 4889 Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 353 KB/s], Decompressed: 4926 Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 68 KB/s], Decompressed: 4926 Downloaded: 5019 file(s) [attempted 5019/8459 = 59%, 39 KB/s], Decompressed: 4933 Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 52 KB/s], Decompressed: 4933 Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 548 KB/s], Decompressed: 4933 Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 348 KB/s], Decompressed: 5128 Downloaded: 5175 file(s) [attempted 5175/8459 = 61%, 157 KB/s], Decompressed: 5166 Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 178 KB/s], Decompressed: 5176 Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 137 KB/s], Decompressed: 5176 Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 378 KB/s], Decompressed: 5180 Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 690 KB/s], Decompressed: 5180 Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 670 KB/s], Decompressed: 5260 Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 230 KB/s], Decompressed: 5260 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 774 KB/s], Decompressed: 5440 Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 150 KB/s], Decompressed: 5481 Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 603 KB/s], Decompressed: 5518 Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 36 KB/s], Decompressed: 5563 Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 663 KB/s], Decompressed: 5601 Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 46 KB/s], Decompressed: 5607 Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 750 KB/s], Decompressed: 5607 Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 284 KB/s], Decompressed: 5611 Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 290 KB/s], Decompressed: 5611 Downloaded: 5803 file(s) [attempted 5803/8459 = 68%, 477 KB/s], Decompressed: 5792 Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 633 KB/s], Decompressed: 5826 Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 155 KB/s], Decompressed: 5874 Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 693 KB/s], Decompressed: 5888 Downloaded: 5958 file(s) [attempted 5958/8459 = 70%, 71 KB/s], Decompressed: 5888 Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 140 KB/s], Decompressed: 5977 Downloaded: 6035 file(s) [attempted 6035/8459 = 71%, 356 KB/s], Decompressed: 6001 Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 213 KB/s], Decompressed: 6001 Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 126 KB/s], Decompressed: 6104 Downloaded: 6146 file(s) [attempted 6146/8459 = 72%, 1041 KB/s], Decompressed: 6141 Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 653 KB/s], Decompressed: 6182 Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 127 KB/s], Decompressed: 6182 Downloaded: 6282 file(s) [attempted 6282/8459 = 74%, 50 KB/s], Decompressed: 6182 Downloaded: 6319 file(s) [attempted 6319/8459 = 74%, 332 KB/s], Decompressed: 6182 Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 307 KB/s], Decompressed: 6189 Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 67 KB/s], Decompressed: 6189 Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 301 KB/s], Decompressed: 6189 Downloaded: 6480 file(s) [attempted 6480/8459 = 76%, 227 KB/s], Decompressed: 6343 Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 109 KB/s], Decompressed: 6343 Downloaded: 6559 file(s) [attempted 6559/8459 = 77%, 157 KB/s], Decompressed: 6446 Downloaded: 6596 file(s) [attempted 6596/8459 = 77%, 127 KB/s], Decompressed: 6446 Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 245 KB/s], Decompressed: 6531 Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 131 KB/s], Decompressed: 6665 Downloaded: 6720 file(s) [attempted 6720/8459 = 79%, 153 KB/s], Decompressed: 6665 Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 435 KB/s], Decompressed: 6668 Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 548 KB/s], Decompressed: 6788 Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 233 KB/s], Decompressed: 6822 Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 200 KB/s], Decompressed: 6867 Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 210 KB/s], Decompressed: 6891 Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 163 KB/s], Decompressed: 6891 Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 155 KB/s], Decompressed: 6898 Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 310 KB/s], Decompressed: 6898 Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 153 KB/s], Decompressed: 6898 Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 71 KB/s], Decompressed: 6898 Downloaded: 7132 file(s) [attempted 7132/8459 = 84%, 325 KB/s], Decompressed: 6898 Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 287 KB/s], Decompressed: 6898 Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 644 KB/s], Decompressed: 6898 Downloaded: 7254 file(s) [attempted 7254/8459 = 85%, 1384 KB/s], Decompressed: 6980 Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 262 KB/s], Decompressed: 6980 Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 75 KB/s], Decompressed: 6980 Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 373 KB/s], Decompressed: 7219 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 112 KB/s], Decompressed: 7219 Downloaded: 7454 file(s) [attempted 7454/8459 = 88%, 223 KB/s], Decompressed: 7442 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 140 KB/s], Decompressed: 7486 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 47 KB/s], Decompressed: 7527 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 889 KB/s], Decompressed: 7551 Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 329 KB/s], Decompressed: 7551 Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 277 KB/s], Decompressed: 7633 Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 225 KB/s], Decompressed: 7633 Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 141 KB/s], Decompressed: 7633 Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 480 KB/s], Decompressed: 7647 Downloaded: 7805 file(s) [attempted 7805/8459 = 92%, 724 KB/s], Decompressed: 7647 Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 452 KB/s], Decompressed: 7818 Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 776 KB/s], Decompressed: 7876 Downloaded: 7928 file(s) [attempted 7928/8459 = 93%, 1059 KB/s], Decompressed: 7924 Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 93 KB/s], Decompressed: 7959 Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 150 KB/s], Decompressed: 7989 Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 28 KB/s], Decompressed: 7989 Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 455 KB/s], Decompressed: 7993 Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 357 KB/s], Decompressed: 8075 Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 627 KB/s], Decompressed: 8075 Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 229 KB/s], Decompressed: 8191 Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 272 KB/s], Decompressed: 8215 Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 266 KB/s], Decompressed: 8215 Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 159 KB/s], Decompressed: 8219 Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 1111 KB/s], Decompressed: 8219 Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 52 KB/s], Decompressed: 8219 Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 642 KB/s], Decompressed: 8219 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 263 KB/s], Decompressed: 8304 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 263 KB/s], Decompressed: 8304
lean_checker exit 1
lake build
ℹ [3536/3546] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3571] 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`
⚠ [3694/3715] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3816/3819] Building PrimeNumberTheoremAnd.IEANTN.Mertens (177s)
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
⚠ [3885/3895] 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`
⚠ [4125/4166] 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`
ℹ [4164/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.
⚠ [4166/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`
✔ [4173/4188] Built PrimeNumberTheoremAnd.LaplaceInversion (13s)
✔ [4185/4188] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (10s)
⚠ [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
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (4.5s)
✔ [25/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (538ms)
✔ [33/41] Built Cli:c.o (66ms)
ℹ [3603/3641] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3628/3680] 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`
⚠ [3764/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3890/3901] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3896/3901] Building PrimeNumberTheoremAnd.IEANTN.Mertens (13s)
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
⚠ [3963/3985] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4194/4211] 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`
⚠ [4270/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`
ℹ [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`
✔ [4367/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (7.7s)
✔ [4391/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (5.8s)
⚠ [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 (47s)
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