Verification run

Run 144

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via github_backfill

failed commit 9d0b6424f752 toolchain lean-v4-30-0 prover lean took 6m 28s · 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)

Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

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


$ git checkout 9d0b6424f75237a8ba38c51ef549dfdec69eff78
exit_code=Some(128) duration_ms=4
stderr:
fatal: reference is not a tree: 9d0b6424f75237a8ba38c51ef549dfdec69eff78


$ git fetch --depth 1 origin 9d0b6424f75237a8ba38c51ef549dfdec69eff78
exit_code=Some(0) duration_ms=933
stderr:
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            9d0b6424f75237a8ba38c51ef549dfdec69eff78 -> FETCH_HEAD


$ git checkout 9d0b6424f75237a8ba38c51ef549dfdec69eff78 (after fetch)
exit_code=Some(0) duration_ms=59
stderr:
Note: switching to '9d0b6424f75237a8ba38c51ef549dfdec69eff78'.

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 9d0b642 feat(Mertens): prove deriv_gamma_add_γ_eq_zero (#1320) (#1598)

Resolved source revision: 9d0b6424f75237a8ba38c51ef549dfdec69eff78

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=9d0b6424f75237a8ba38c51ef549dfdec69eff78 provenance={"branch":"main","checked_out_revision":"9d0b6424f75237a8ba38c51ef549dfdec69eff78","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"9d0b6424f75237a8ba38c51ef549dfdec69eff78","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=52243
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: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 13
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 15 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 338 KB/s], Decompressed: 59
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 293 KB/s], Decompressed: 82
Downloaded: 114 file(s) [attempted 114/8459 = 1%, 276 KB/s], Decompressed: 110
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 360 KB/s], Decompressed: 138
Downloaded: 176 file(s) [attempted 176/8459 = 2%, 134 KB/s], Decompressed: 172
Downloaded: 207 file(s) [attempted 207/8459 = 2%, 45 KB/s], Decompressed: 203
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 165 KB/s], Decompressed: 230
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 73 KB/s], Decompressed: 268
Downloaded: 307 file(s) [attempted 307/8459 = 3%, 150 KB/s], Decompressed: 302
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 654 KB/s], Decompressed: 336
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 413 KB/s], Decompressed: 371
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 160 KB/s], Decompressed: 408
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 166 KB/s], Decompressed: 446
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 249 KB/s], Decompressed: 487
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 166 KB/s], Decompressed: 526
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 229 KB/s], Decompressed: 556
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 339 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 206 KB/s], Decompressed: 638
Downloaded: 680 file(s) [attempted 680/8459 = 8%, 52 KB/s], Decompressed: 675
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 289 KB/s], Decompressed: 710
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 58 KB/s], Decompressed: 747
Downloaded: 790 file(s) [attempted 790/8459 = 9%, 1502 KB/s], Decompressed: 785
Downloaded: 830 file(s) [attempted 830/8459 = 9%, 793 KB/s], Decompressed: 826
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 424 KB/s], Decompressed: 860
Downloaded: 905 file(s) [attempted 905/8459 = 10%, 206 KB/s], Decompressed: 891
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 316 KB/s], Decompressed: 936
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 107 KB/s], Decompressed: 977
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 168 KB/s], Decompressed: 1011
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 1786 KB/s], Decompressed: 1052
Downloaded: 1094 file(s) [attempted 1094/8459 = 12%, 542 KB/s], Decompressed: 1086
Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 96 KB/s], Decompressed: 1131
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 86 KB/s], Decompressed: 1169
Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 181 KB/s], Decompressed: 1206
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 93 KB/s], Decompressed: 1244
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 823 KB/s], Decompressed: 1285
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 142 KB/s], Decompressed: 1326
Downloaded: 1373 file(s) [attempted 1373/8459 = 16%, 1122 KB/s], Decompressed: 1367
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 993 KB/s], Decompressed: 1401
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 153 KB/s], Decompressed: 1439
Downloaded: 1481 file(s) [attempted 1481/8459 = 17%, 119 KB/s], Decompressed: 1477
Downloaded: 1523 file(s) [attempted 1523/8459 = 18%, 393 KB/s], Decompressed: 1514
Downloaded: 1559 file(s) [attempted 1559/8459 = 18%, 99 KB/s], Decompressed: 1548
Downloaded: 1592 file(s) [attempted 1592/8459 = 18%, 263 KB/s], Decompressed: 1586
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 644 KB/s], Decompressed: 1627
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 115 KB/s], Decompressed: 1665
Downloaded: 1707 file(s) [attempted 1707/8459 = 20%, 651 KB/s], Decompressed: 1702
Downloaded: 1740 file(s) [attempted 1740/8459 = 20%, 49 KB/s], Decompressed: 1737
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 183 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 410 KB/s], Decompressed: 1815
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 23 KB/s], Decompressed: 1853
Downloaded: 1894 file(s) [attempted 1894/8459 = 22%, 305 KB/s], Decompressed: 1887
Downloaded: 1930 file(s) [attempted 1930/8459 = 22%, 72 KB/s], Decompressed: 1921
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 174 KB/s], Decompressed: 1966
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 63 KB/s], Decompressed: 2007
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 181 KB/s], Decompressed: 2041
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 31 KB/s], Decompressed: 2072
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 102 KB/s], Decompressed: 2117
Downloaded: 2164 file(s) [attempted 2164/8459 = 25%, 297 KB/s], Decompressed: 2161
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 253 KB/s], Decompressed: 2206
Downloaded: 2248 file(s) [attempted 2248/8459 = 26%, 381 KB/s], Decompressed: 2240
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 324 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 37 KB/s], Decompressed: 2315
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 99 KB/s], Decompressed: 2356
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 290 KB/s], Decompressed: 2394
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 1306 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 104 KB/s], Decompressed: 2469
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 129 KB/s], Decompressed: 2510
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 152 KB/s], Decompressed: 2548
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 416 KB/s], Decompressed: 2585
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 463 KB/s], Decompressed: 2626
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 129 KB/s], Decompressed: 2661
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 115 KB/s], Decompressed: 2702
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 93 KB/s], Decompressed: 2739
Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 51 KB/s], Decompressed: 2777
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 492 KB/s], Decompressed: 2811
Downloaded: 2857 file(s) [attempted 2857/8459 = 33%, 31 KB/s], Decompressed: 2849
Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 120 KB/s], Decompressed: 2893
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 105 KB/s], Decompressed: 2924
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 1063 KB/s], Decompressed: 2962
Downloaded: 3010 file(s) [attempted 3010/8459 = 35%, 150 KB/s], Decompressed: 3006
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 248 KB/s], Decompressed: 3044
Downloaded: 3086 file(s) [attempted 3086/8459 = 36%, 501 KB/s], Decompressed: 3082
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 263 KB/s], Decompressed: 3119
Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 669 KB/s], Decompressed: 3157
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 502 KB/s], Decompressed: 3198
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 253 KB/s], Decompressed: 3236
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 385 KB/s], Decompressed: 3273
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 270 KB/s], Decompressed: 3311
Downloaded: 3354 file(s) [attempted 3354/8459 = 39%, 354 KB/s], Decompressed: 3345
Downloaded: 3392 file(s) [attempted 3392/8459 = 40%, 581 KB/s], Decompressed: 3386
Downloaded: 3428 file(s) [attempted 3428/8459 = 40%, 478 KB/s], Decompressed: 3424
Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 167 KB/s], Decompressed: 3458
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 99 KB/s], Decompressed: 3496
Downloaded: 3540 file(s) [attempted 3540/8459 = 41%, 67 KB/s], Decompressed: 3533
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 434 KB/s], Decompressed: 3578
Downloaded: 3620 file(s) [attempted 3620/8459 = 42%, 738 KB/s], Decompressed: 3612
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 119 KB/s], Decompressed: 3650
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 231 KB/s], Decompressed: 3691
Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 265 KB/s], Decompressed: 3732
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 165 KB/s], Decompressed: 3773
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 212 KB/s], Decompressed: 3812
Downloaded: 3849 file(s) [attempted 3849/8459 = 45%, 219 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 529 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 217 KB/s], Decompressed: 3930
Downloaded: 3972 file(s) [attempted 3972/8459 = 46%, 341 KB/s], Decompressed: 3968
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 724 KB/s], Decompressed: 4006
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 541 KB/s], Decompressed: 4040
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 41 KB/s], Decompressed: 4084
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 114 KB/s], Decompressed: 4129
Downloaded: 4165 file(s) [attempted 4165/8459 = 49%, 184 KB/s], Decompressed: 4160
Downloaded: 4203 file(s) [attempted 4203/8459 = 49%, 189 KB/s], Decompressed: 4194
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 356 KB/s], Decompressed: 4235
Downloaded: 4280 file(s) [attempted 4280/8459 = 50%, 367 KB/s], Decompressed: 4270
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 807 KB/s], Decompressed: 4310
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 346 KB/s], Decompressed: 4351
Downloaded: 4393 file(s) [attempted 4393/8459 = 51%, 211 KB/s], Decompressed: 4386
Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 108 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 346 KB/s], Decompressed: 4464
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 376 KB/s], Decompressed: 4505
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 164 KB/s], Decompressed: 4546
Downloaded: 4585 file(s) [attempted 4585/8459 = 54%, 209 KB/s], Decompressed: 4577
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 251 KB/s], Decompressed: 4618
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 664 KB/s], Decompressed: 4659
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 35 KB/s], Decompressed: 4697
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 230 KB/s], Decompressed: 4735
Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 143 KB/s], Decompressed: 4772
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 75 KB/s], Decompressed: 4813
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 304 KB/s], Decompressed: 4851
Downloaded: 4895 file(s) [attempted 4895/8459 = 57%, 107 KB/s], Decompressed: 4885
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 128 KB/s], Decompressed: 4926
Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 172 KB/s], Decompressed: 4967
Downloaded: 5011 file(s) [attempted 5011/8459 = 59%, 292 KB/s], Decompressed: 5002
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 155 KB/s], Decompressed: 5039
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 107 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 48 KB/s], Decompressed: 5118
Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 94 KB/s], Decompressed: 5152
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 34 KB/s], Decompressed: 5193
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 301 KB/s], Decompressed: 5228
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 1491 KB/s], Decompressed: 5269
Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 1201 KB/s], Decompressed: 5313
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 828 KB/s], Decompressed: 5351
Downloaded: 5393 file(s) [attempted 5393/8459 = 63%, 193 KB/s], Decompressed: 5385
Downloaded: 5427 file(s) [attempted 5427/8459 = 64%, 271 KB/s], Decompressed: 5423
Downloaded: 5467 file(s) [attempted 5467/8459 = 64%, 878 KB/s], Decompressed: 5460
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 294 KB/s], Decompressed: 5498
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 37 KB/s], Decompressed: 5539
Downloaded: 5579 file(s) [attempted 5579/8459 = 65%, 68 KB/s], Decompressed: 5573
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 163 KB/s], Decompressed: 5614
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 149 KB/s], Decompressed: 5652
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 117 KB/s], Decompressed: 5690
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 98 KB/s], Decompressed: 5724
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 186 KB/s], Decompressed: 5768
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 23 KB/s], Decompressed: 5813
Downloaded: 5857 file(s) [attempted 5857/8459 = 69%, 87 KB/s], Decompressed: 5850
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 96 KB/s], Decompressed: 5892
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 800 KB/s], Decompressed: 5933
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 261 KB/s], Decompressed: 5974
Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 46 KB/s], Decompressed: 6008
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 351 KB/s], Decompressed: 6049
Downloaded: 6092 file(s) [attempted 6092/8459 = 72%, 1848 KB/s], Decompressed: 6087
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 216 KB/s], Decompressed: 6124
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 151 KB/s], Decompressed: 6162
Downloaded: 6205 file(s) [attempted 6205/8459 = 73%, 570 KB/s], Decompressed: 6200
Downloaded: 6241 file(s) [attempted 6241/8459 = 73%, 48 KB/s], Decompressed: 6237
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 283 KB/s], Decompressed: 6278
Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 628 KB/s], Decompressed: 6312
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 730 KB/s], Decompressed: 6347
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 129 KB/s], Decompressed: 6384
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 154 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 79 KB/s], Decompressed: 6463
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 52 KB/s], Decompressed: 6501
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 313 KB/s], Decompressed: 6542
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 420 KB/s], Decompressed: 6579
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 388 KB/s], Decompressed: 6614
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 210 KB/s], Decompressed: 6648
Downloaded: 6697 file(s) [attempted 6697/8459 = 79%, 1350 KB/s], Decompressed: 6689
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 30 KB/s], Decompressed: 6727
Downloaded: 6772 file(s) [attempted 6772/8459 = 80%, 104 KB/s], Decompressed: 6768
Downloaded: 6806 file(s) [attempted 6806/8459 = 80%, 528 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 81 KB/s], Decompressed: 6843
Downloaded: 6883 file(s) [attempted 6883/8459 = 81%, 857 KB/s], Decompressed: 6877
Downloaded: 6924 file(s) [attempted 6924/8459 = 81%, 301 KB/s], Decompressed: 6918
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 165 KB/s], Decompressed: 6956
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 168 KB/s], Decompressed: 6994
Downloaded: 7035 file(s) [attempted 7035/8459 = 83%, 77 KB/s], Decompressed: 7031
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 41 KB/s], Decompressed: 7072
Downloaded: 7113 file(s) [attempted 7113/8459 = 84%, 592 KB/s], Decompressed: 7107
Downloaded: 7151 file(s) [attempted 7151/8459 = 84%, 75 KB/s], Decompressed: 7148
Downloaded: 7187 file(s) [attempted 7187/8459 = 84%, 688 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 426 KB/s], Decompressed: 7223
Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 119 KB/s], Decompressed: 7257
Downloaded: 7302 file(s) [attempted 7302/8459 = 86%, 41 KB/s], Decompressed: 7295
Downloaded: 7337 file(s) [attempted 7337/8459 = 86%, 862 KB/s], Decompressed: 7332
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 499 KB/s], Decompressed: 7373
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 608 KB/s], Decompressed: 7408
Downloaded: 7450 file(s) [attempted 7450/8459 = 88%, 922 KB/s], Decompressed: 7445
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 136 KB/s], Decompressed: 7483
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 546 KB/s], Decompressed: 7527
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 431 KB/s], Decompressed: 7568
Downloaded: 7608 file(s) [attempted 7608/8459 = 89%, 131 KB/s], Decompressed: 7599
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 177 KB/s], Decompressed: 7633
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 48 KB/s], Decompressed: 7681
Downloaded: 7728 file(s) [attempted 7728/8459 = 91%, 73 KB/s], Decompressed: 7716
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 496 KB/s], Decompressed: 7764
Downloaded: 7805 file(s) [attempted 7805/8459 = 92%, 720 KB/s], Decompressed: 7798
Downloaded: 7839 file(s) [attempted 7839/8459 = 92%, 21 KB/s], Decompressed: 7835
Downloaded: 7882 file(s) [attempted 7882/8459 = 93%, 949 KB/s], Decompressed: 7876
Downloaded: 7918 file(s) [attempted 7918/8459 = 93%, 31 KB/s], Decompressed: 7907
Downloaded: 7952 file(s) [attempted 7952/8459 = 94%, 493 KB/s], Decompressed: 7942
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 220 KB/s], Decompressed: 7983
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 883 KB/s], Decompressed: 8024
Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 291 KB/s], Decompressed: 8068
Downloaded: 8113 file(s) [attempted 8113/8459 = 95%, 86 KB/s], Decompressed: 8109
Downloaded: 8152 file(s) [attempted 8152/8459 = 96%, 189 KB/s], Decompressed: 8143
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 1219 KB/s], Decompressed: 8181
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 459 KB/s], Decompressed: 8227
Downloaded: 8275 file(s) [attempted 8275/8459 = 97%, 78 KB/s], Decompressed: 8270
Downloaded: 8308 file(s) [attempted 8308/8459 = 98%, 52 KB/s], Decompressed: 8301
Downloaded: 8345 file(s) [attempted 8345/8459 = 98%, 932 KB/s], Decompressed: 8342
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 324 KB/s], Decompressed: 8380
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 596 KB/s], Decompressed: 8421
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(1) duration_ms=96911
stdout:
ℹ [3536/3547] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3572] 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`
⚠ [3693/3707] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3817/3828] Building PrimeNumberTheoremAnd.IEANTN.Mertens (69s)
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
⚠ [3884/3905] 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`
ℹ [4167/4187] 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.
⚠ [4169/4187] 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`
⚠ [4185/4187] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352: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=29549
stdout:
✔ [14/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 (510ms)
✔ [33/53] Built Cli:c.o (69ms)
ℹ [3603/3670] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3619/3670] 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/3853] 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`
✖ [3897/3916] 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
⚠ [3969/3992] 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/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [4278/4356] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
ℹ [4332/4395] 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.
⚠ [4351/4395] 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`
⚠ [4391/4396] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352: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


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_checkout exit 0 duration 933 ms · created 7/9/2026, 8:53:57 PM

git fetch --depth 1 origin 9d0b6424f75237a8ba38c51ef549dfdec69eff78

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

git_clone exit 0 duration 1s · created 7/9/2026, 8:53:57 PM

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

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

git_checkout exit 128 duration 4 ms · created 7/9/2026, 8:53:57 PM

git checkout 9d0b6424f75237a8ba38c51ef549dfdec69eff78

fatal: reference is not a tree: 9d0b6424f75237a8ba38c51ef549dfdec69eff78

git_checkout exit 0 duration 59 ms · created 7/9/2026, 8:53:57 PM

git checkout 9d0b6424f75237a8ba38c51ef549dfdec69eff78 (after fetch)

Note: switching to '9d0b6424f75237a8ba38c51ef549dfdec69eff78'.

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 9d0b642 feat(Mertens): prove deriv_gamma_add_γ_eq_zero (#1320) (#1598)

lake_cache exit 0 duration 52s · created 7/9/2026, 8:53:57 PM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 13
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 15 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 338 KB/s], Decompressed: 59
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 293 KB/s], Decompressed: 82
Downloaded: 114 file(s) [attempted 114/8459 = 1%, 276 KB/s], Decompressed: 110
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 360 KB/s], Decompressed: 138
Downloaded: 176 file(s) [attempted 176/8459 = 2%, 134 KB/s], Decompressed: 172
Downloaded: 207 file(s) [attempted 207/8459 = 2%, 45 KB/s], Decompressed: 203
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 165 KB/s], Decompressed: 230
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 73 KB/s], Decompressed: 268
Downloaded: 307 file(s) [attempted 307/8459 = 3%, 150 KB/s], Decompressed: 302
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 654 KB/s], Decompressed: 336
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 413 KB/s], Decompressed: 371
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 160 KB/s], Decompressed: 408
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 166 KB/s], Decompressed: 446
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 249 KB/s], Decompressed: 487
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 166 KB/s], Decompressed: 526
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 229 KB/s], Decompressed: 556
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 339 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 206 KB/s], Decompressed: 638
Downloaded: 680 file(s) [attempted 680/8459 = 8%, 52 KB/s], Decompressed: 675
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 289 KB/s], Decompressed: 710
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 58 KB/s], Decompressed: 747
Downloaded: 790 file(s) [attempted 790/8459 = 9%, 1502 KB/s], Decompressed: 785
Downloaded: 830 file(s) [attempted 830/8459 = 9%, 793 KB/s], Decompressed: 826
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 424 KB/s], Decompressed: 860
Downloaded: 905 file(s) [attempted 905/8459 = 10%, 206 KB/s], Decompressed: 891
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 316 KB/s], Decompressed: 936
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 107 KB/s], Decompressed: 977
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 168 KB/s], Decompressed: 1011
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 1786 KB/s], Decompressed: 1052
Downloaded: 1094 file(s) [attempted 1094/8459 = 12%, 542 KB/s], Decompressed: 1086
Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 96 KB/s], Decompressed: 1131
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 86 KB/s], Decompressed: 1169
Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 181 KB/s], Decompressed: 1206
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 93 KB/s], Decompressed: 1244
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 823 KB/s], Decompressed: 1285
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 142 KB/s], Decompressed: 1326
Downloaded: 1373 file(s) [attempted 1373/8459 = 16%, 1122 KB/s], Decompressed: 1367
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 993 KB/s], Decompressed: 1401
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 153 KB/s], Decompressed: 1439
Downloaded: 1481 file(s) [attempted 1481/8459 = 17%, 119 KB/s], Decompressed: 1477
Downloaded: 1523 file(s) [attempted 1523/8459 = 18%, 393 KB/s], Decompressed: 1514
Downloaded: 1559 file(s) [attempted 1559/8459 = 18%, 99 KB/s], Decompressed: 1548
Downloaded: 1592 file(s) [attempted 1592/8459 = 18%, 263 KB/s], Decompressed: 1586
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 644 KB/s], Decompressed: 1627
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 115 KB/s], Decompressed: 1665
Downloaded: 1707 file(s) [attempted 1707/8459 = 20%, 651 KB/s], Decompressed: 1702
Downloaded: 1740 file(s) [attempted 1740/8459 = 20%, 49 KB/s], Decompressed: 1737
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 183 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 410 KB/s], Decompressed: 1815
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 23 KB/s], Decompressed: 1853
Downloaded: 1894 file(s) [attempted 1894/8459 = 22%, 305 KB/s], Decompressed: 1887
Downloaded: 1930 file(s) [attempted 1930/8459 = 22%, 72 KB/s], Decompressed: 1921
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 174 KB/s], Decompressed: 1966
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 63 KB/s], Decompressed: 2007
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 181 KB/s], Decompressed: 2041
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 31 KB/s], Decompressed: 2072
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 102 KB/s], Decompressed: 2117
Downloaded: 2164 file(s) [attempted 2164/8459 = 25%, 297 KB/s], Decompressed: 2161
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 253 KB/s], Decompressed: 2206
Downloaded: 2248 file(s) [attempted 2248/8459 = 26%, 381 KB/s], Decompressed: 2240
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 324 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 37 KB/s], Decompressed: 2315
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 99 KB/s], Decompressed: 2356
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 290 KB/s], Decompressed: 2394
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 1306 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 104 KB/s], Decompressed: 2469
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 129 KB/s], Decompressed: 2510
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 152 KB/s], Decompressed: 2548
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 416 KB/s], Decompressed: 2585
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 463 KB/s], Decompressed: 2626
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 129 KB/s], Decompressed: 2661
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 115 KB/s], Decompressed: 2702
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 93 KB/s], Decompressed: 2739
Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 51 KB/s], Decompressed: 2777
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 492 KB/s], Decompressed: 2811
Downloaded: 2857 file(s) [attempted 2857/8459 = 33%, 31 KB/s], Decompressed: 2849
Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 120 KB/s], Decompressed: 2893
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 105 KB/s], Decompressed: 2924
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 1063 KB/s], Decompressed: 2962
Downloaded: 3010 file(s) [attempted 3010/8459 = 35%, 150 KB/s], Decompressed: 3006
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 248 KB/s], Decompressed: 3044
Downloaded: 3086 file(s) [attempted 3086/8459 = 36%, 501 KB/s], Decompressed: 3082
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 263 KB/s], Decompressed: 3119
Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 669 KB/s], Decompressed: 3157
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 502 KB/s], Decompressed: 3198
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 253 KB/s], Decompressed: 3236
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 385 KB/s], Decompressed: 3273
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 270 KB/s], Decompressed: 3311
Downloaded: 3354 file(s) [attempted 3354/8459 = 39%, 354 KB/s], Decompressed: 3345
Downloaded: 3392 file(s) [attempted 3392/8459 = 40%, 581 KB/s], Decompressed: 3386
Downloaded: 3428 file(s) [attempted 3428/8459 = 40%, 478 KB/s], Decompressed: 3424
Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 167 KB/s], Decompressed: 3458
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 99 KB/s], Decompressed: 3496
Downloaded: 3540 file(s) [attempted 3540/8459 = 41%, 67 KB/s], Decompressed: 3533
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 434 KB/s], Decompressed: 3578
Downloaded: 3620 file(s) [attempted 3620/8459 = 42%, 738 KB/s], Decompressed: 3612
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 119 KB/s], Decompressed: 3650
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 231 KB/s], Decompressed: 3691
Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 265 KB/s], Decompressed: 3732
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 165 KB/s], Decompressed: 3773
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 212 KB/s], Decompressed: 3812
Downloaded: 3849 file(s) [attempted 3849/8459 = 45%, 219 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 529 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 217 KB/s], Decompressed: 3930
Downloaded: 3972 file(s) [attempted 3972/8459 = 46%, 341 KB/s], Decompressed: 3968
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 724 KB/s], Decompressed: 4006
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 541 KB/s], Decompressed: 4040
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 41 KB/s], Decompressed: 4084
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 114 KB/s], Decompressed: 4129
Downloaded: 4165 file(s) [attempted 4165/8459 = 49%, 184 KB/s], Decompressed: 4160
Downloaded: 4203 file(s) [attempted 4203/8459 = 49%, 189 KB/s], Decompressed: 4194
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 356 KB/s], Decompressed: 4235
Downloaded: 4280 file(s) [attempted 4280/8459 = 50%, 367 KB/s], Decompressed: 4270
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 807 KB/s], Decompressed: 4310
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 346 KB/s], Decompressed: 4351
Downloaded: 4393 file(s) [attempted 4393/8459 = 51%, 211 KB/s], Decompressed: 4386
Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 108 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 346 KB/s], Decompressed: 4464
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 376 KB/s], Decompressed: 4505
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 164 KB/s], Decompressed: 4546
Downloaded: 4585 file(s) [attempted 4585/8459 = 54%, 209 KB/s], Decompressed: 4577
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 251 KB/s], Decompressed: 4618
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 664 KB/s], Decompressed: 4659
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 35 KB/s], Decompressed: 4697
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 230 KB/s], Decompressed: 4735
Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 143 KB/s], Decompressed: 4772
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 75 KB/s], Decompressed: 4813
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 304 KB/s], Decompressed: 4851
Downloaded: 4895 file(s) [attempted 4895/8459 = 57%, 107 KB/s], Decompressed: 4885
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 128 KB/s], Decompressed: 4926
Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 172 KB/s], Decompressed: 4967
Downloaded: 5011 file(s) [attempted 5011/8459 = 59%, 292 KB/s], Decompressed: 5002
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 155 KB/s], Decompressed: 5039
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 107 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 48 KB/s], Decompressed: 5118
Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 94 KB/s], Decompressed: 5152
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 34 KB/s], Decompressed: 5193
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 301 KB/s], Decompressed: 5228
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 1491 KB/s], Decompressed: 5269
Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 1201 KB/s], Decompressed: 5313
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 828 KB/s], Decompressed: 5351
Downloaded: 5393 file(s) [attempted 5393/8459 = 63%, 193 KB/s], Decompressed: 5385
Downloaded: 5427 file(s) [attempted 5427/8459 = 64%, 271 KB/s], Decompressed: 5423
Downloaded: 5467 file(s) [attempted 5467/8459 = 64%, 878 KB/s], Decompressed: 5460
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 294 KB/s], Decompressed: 5498
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 37 KB/s], Decompressed: 5539
Downloaded: 5579 file(s) [attempted 5579/8459 = 65%, 68 KB/s], Decompressed: 5573
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 163 KB/s], Decompressed: 5614
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 149 KB/s], Decompressed: 5652
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 117 KB/s], Decompressed: 5690
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 98 KB/s], Decompressed: 5724
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 186 KB/s], Decompressed: 5768
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 23 KB/s], Decompressed: 5813
Downloaded: 5857 file(s) [attempted 5857/8459 = 69%, 87 KB/s], Decompressed: 5850
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 96 KB/s], Decompressed: 5892
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 800 KB/s], Decompressed: 5933
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 261 KB/s], Decompressed: 5974
Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 46 KB/s], Decompressed: 6008
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 351 KB/s], Decompressed: 6049
Downloaded: 6092 file(s) [attempted 6092/8459 = 72%, 1848 KB/s], Decompressed: 6087
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 216 KB/s], Decompressed: 6124
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 151 KB/s], Decompressed: 6162
Downloaded: 6205 file(s) [attempted 6205/8459 = 73%, 570 KB/s], Decompressed: 6200
Downloaded: 6241 file(s) [attempted 6241/8459 = 73%, 48 KB/s], Decompressed: 6237
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 283 KB/s], Decompressed: 6278
Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 628 KB/s], Decompressed: 6312
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 730 KB/s], Decompressed: 6347
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 129 KB/s], Decompressed: 6384
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 154 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 79 KB/s], Decompressed: 6463
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 52 KB/s], Decompressed: 6501
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 313 KB/s], Decompressed: 6542
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 420 KB/s], Decompressed: 6579
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 388 KB/s], Decompressed: 6614
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 210 KB/s], Decompressed: 6648
Downloaded: 6697 file(s) [attempted 6697/8459 = 79%, 1350 KB/s], Decompressed: 6689
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 30 KB/s], Decompressed: 6727
Downloaded: 6772 file(s) [attempted 6772/8459 = 80%, 104 KB/s], Decompressed: 6768
Downloaded: 6806 file(s) [attempted 6806/8459 = 80%, 528 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 81 KB/s], Decompressed: 6843
Downloaded: 6883 file(s) [attempted 6883/8459 = 81%, 857 KB/s], Decompressed: 6877
Downloaded: 6924 file(s) [attempted 6924/8459 = 81%, 301 KB/s], Decompressed: 6918
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 165 KB/s], Decompressed: 6956
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 168 KB/s], Decompressed: 6994
Downloaded: 7035 file(s) [attempted 7035/8459 = 83%, 77 KB/s], Decompressed: 7031
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 41 KB/s], Decompressed: 7072
Downloaded: 7113 file(s) [attempted 7113/8459 = 84%, 592 KB/s], Decompressed: 7107
Downloaded: 7151 file(s) [attempted 7151/8459 = 84%, 75 KB/s], Decompressed: 7148
Downloaded: 7187 file(s) [attempted 7187/8459 = 84%, 688 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 426 KB/s], Decompressed: 7223
Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 119 KB/s], Decompressed: 7257
Downloaded: 7302 file(s) [attempted 7302/8459 = 86%, 41 KB/s], Decompressed: 7295
Downloaded: 7337 file(s) [attempted 7337/8459 = 86%, 862 KB/s], Decompressed: 7332
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 499 KB/s], Decompressed: 7373
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 608 KB/s], Decompressed: 7408
Downloaded: 7450 file(s) [attempted 7450/8459 = 88%, 922 KB/s], Decompressed: 7445
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 136 KB/s], Decompressed: 7483
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 546 KB/s], Decompressed: 7527
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 431 KB/s], Decompressed: 7568
Downloaded: 7608 file(s) [attempted 7608/8459 = 89%, 131 KB/s], Decompressed: 7599
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 177 KB/s], Decompressed: 7633
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 48 KB/s], Decompressed: 7681
Downloaded: 7728 file(s) [attempted 7728/8459 = 91%, 73 KB/s], Decompressed: 7716
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 496 KB/s], Decompressed: 7764
Downloaded: 7805 file(s) [attempted 7805/8459 = 92%, 720 KB/s], Decompressed: 7798
Downloaded: 7839 file(s) [attempted 7839/8459 = 92%, 21 KB/s], Decompressed: 7835
Downloaded: 7882 file(s) [attempted 7882/8459 = 93%, 949 KB/s], Decompressed: 7876
Downloaded: 7918 file(s) [attempted 7918/8459 = 93%, 31 KB/s], Decompressed: 7907
Downloaded: 7952 file(s) [attempted 7952/8459 = 94%, 493 KB/s], Decompressed: 7942
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 220 KB/s], Decompressed: 7983
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 883 KB/s], Decompressed: 8024
Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 291 KB/s], Decompressed: 8068
Downloaded: 8113 file(s) [attempted 8113/8459 = 95%, 86 KB/s], Decompressed: 8109
Downloaded: 8152 file(s) [attempted 8152/8459 = 96%, 189 KB/s], Decompressed: 8143
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 1219 KB/s], Decompressed: 8181
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 459 KB/s], Decompressed: 8227
Downloaded: 8275 file(s) [attempted 8275/8459 = 97%, 78 KB/s], Decompressed: 8270
Downloaded: 8308 file(s) [attempted 8308/8459 = 98%, 52 KB/s], Decompressed: 8301
Downloaded: 8345 file(s) [attempted 8345/8459 = 98%, 932 KB/s], Decompressed: 8342
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 324 KB/s], Decompressed: 8380
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 596 KB/s], Decompressed: 8421
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8455

lean_checker exit 1 duration 1m 37s · created 7/9/2026, 8:53:57 PM

lake build

ℹ [3536/3547] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3572] 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`
⚠ [3693/3707] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✖ [3817/3828] Building PrimeNumberTheoremAnd.IEANTN.Mertens (69s)
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
⚠ [3884/3905] 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`
ℹ [4167/4187] 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.
⚠ [4169/4187] 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`
⚠ [4185/4187] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens

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

blueprint_build exit 1 duration 30s · created 7/9/2026, 8:53:57 PM

lake build :blueprint

✔ [14/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 (510ms)
✔ [33/53] Built Cli:c.o (69ms)
ℹ [3603/3670] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3619/3670] 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/3853] 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`
✖ [3897/3916] 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
⚠ [3969/3992] 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/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [4278/4356] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
ℹ [4332/4395] 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.
⚠ [4351/4395] 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`
⚠ [4391/4396] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352: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