Verification run

Run 1068

promachina/iut-lean branch master triggered via poller

failed commit a5257f7d7b4a toolchain lean-v4-30-0 prover lean took 11m 14s · finished 3d 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 master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1370-source
exit_code=Some(0) duration_ms=3764
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1370-source'...


$ git checkout a5257f7d7b4a0e3a64866ecbcb8743de6796c22f
exit_code=Some(0) duration_ms=175
stderr:
Note: switching to 'a5257f7d7b4a0e3a64866ecbcb8743de6796c22f'.

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 a5257f7 Lower final goal evidence through packet

Resolved source revision: a5257f7d7b4a0e3a64866ecbcb8743de6796c22f

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=a5257f7d7b4a0e3a64866ecbcb8743de6796c22f provenance={"branch":"master","checked_out_revision":"a5257f7d7b4a0e3a64866ecbcb8743de6796c22f","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"a5257f7d7b4a0e3a64866ecbcb8743de6796c22f","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 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=34227
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%, 2 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 28 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 345 KB/s], Decompressed: 61
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 241 KB/s], Decompressed: 86
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 281 KB/s], Decompressed: 117
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 82 KB/s], Decompressed: 148
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 397 KB/s], Decompressed: 179
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 595 KB/s], Decompressed: 216
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 214 KB/s], Decompressed: 240
Downloaded: 292 file(s) [attempted 292/8459 = 3%, 180 KB/s], Decompressed: 275
Downloaded: 331 file(s) [attempted 331/8459 = 3%, 133 KB/s], Decompressed: 326
Downloaded: 367 file(s) [attempted 367/8459 = 4%, 292 KB/s], Decompressed: 364
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 459 KB/s], Decompressed: 405
Downloaded: 449 file(s) [attempted 449/8459 = 5%, 588 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 247 KB/s], Decompressed: 480
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 208 KB/s], Decompressed: 525
Downloaded: 568 file(s) [attempted 568/8459 = 6%, 164 KB/s], Decompressed: 562
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 150 KB/s], Decompressed: 604
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 170 KB/s], Decompressed: 645
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 253 KB/s], Decompressed: 665
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 97 KB/s], Decompressed: 723
Downloaded: 762 file(s) [attempted 762/8459 = 9%, 513 KB/s], Decompressed: 758
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 857 KB/s], Decompressed: 795
Downloaded: 840 file(s) [attempted 840/8459 = 9%, 166 KB/s], Decompressed: 836
Downloaded: 878 file(s) [attempted 878/8459 = 10%, 70 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 149 KB/s], Decompressed: 915
Downloaded: 958 file(s) [attempted 958/8459 = 11%, 134 KB/s], Decompressed: 949
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 147 KB/s], Decompressed: 991
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 536 KB/s], Decompressed: 1035
Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 877 KB/s], Decompressed: 1069
Downloaded: 1115 file(s) [attempted 1115/8459 = 13%, 79 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 2000 KB/s], Decompressed: 1148
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 618 KB/s], Decompressed: 1186
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 84 KB/s], Decompressed: 1223
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 603 KB/s], Decompressed: 1261
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 511 KB/s], Decompressed: 1295
Downloaded: 1341 file(s) [attempted 1341/8459 = 15%, 42 KB/s], Decompressed: 1336
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1370
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 76 KB/s], Decompressed: 1415
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 44 KB/s], Decompressed: 1456
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 165 KB/s], Decompressed: 1490
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 473 KB/s], Decompressed: 1531
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 264 KB/s], Decompressed: 1569
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 458 KB/s], Decompressed: 1613
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 129 KB/s], Decompressed: 1651
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 459 KB/s], Decompressed: 1692
Downloaded: 1741 file(s) [attempted 1741/8459 = 20%, 50 KB/s], Decompressed: 1733
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 1090 KB/s], Decompressed: 1774
Downloaded: 1821 file(s) [attempted 1821/8459 = 21%, 325 KB/s], Decompressed: 1812
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 32 KB/s], Decompressed: 1850
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 41 KB/s], Decompressed: 1894
Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 337 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 38 KB/s], Decompressed: 1966
Downloaded: 2011 file(s) [attempted 2011/8459 = 23%, 415 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 408 KB/s], Decompressed: 2041
Downloaded: 2087 file(s) [attempted 2087/8459 = 24%, 78 KB/s], Decompressed: 2082
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 104 KB/s], Decompressed: 2127
Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 54 KB/s], Decompressed: 2158
Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 230 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 302 KB/s], Decompressed: 2240
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 311 KB/s], Decompressed: 2281
Downloaded: 2324 file(s) [attempted 2324/8459 = 27%, 40 KB/s], Decompressed: 2318
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 1254 KB/s], Decompressed: 2356
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 314 KB/s], Decompressed: 2390
Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 395 KB/s], Decompressed: 2435
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 143 KB/s], Decompressed: 2483
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 239 KB/s], Decompressed: 2517
Downloaded: 2566 file(s) [attempted 2566/8459 = 30%, 312 KB/s], Decompressed: 2561
Downloaded: 2604 file(s) [attempted 2604/8459 = 30%, 22 KB/s], Decompressed: 2596
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 724 KB/s], Decompressed: 2609
Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 60 KB/s], Decompressed: 2674
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 1205 KB/s], Decompressed: 2712
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 22 KB/s], Decompressed: 2753
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1187 KB/s], Decompressed: 2794
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 50 KB/s], Decompressed: 2825
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 526 KB/s], Decompressed: 2873
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 87 KB/s], Decompressed: 2907
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 42 KB/s], Decompressed: 2952
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 445 KB/s], Decompressed: 2996
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 156 KB/s], Decompressed: 3030
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 209 KB/s], Decompressed: 3071
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 74 KB/s], Decompressed: 3112
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 250 KB/s], Decompressed: 3150
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 24 KB/s], Decompressed: 3174
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 395 KB/s], Decompressed: 3229
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 505 KB/s], Decompressed: 3270
Downloaded: 3312 file(s) [attempted 3312/8459 = 39%, 1163 KB/s], Decompressed: 3304
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 233 KB/s], Decompressed: 3345
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 93 KB/s], Decompressed: 3376
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 111 KB/s], Decompressed: 3424
Downloaded: 3470 file(s) [attempted 3470/8459 = 41%, 690 KB/s], Decompressed: 3462
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 281 KB/s], Decompressed: 3503
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 513 KB/s], Decompressed: 3547
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 272 KB/s], Decompressed: 3581
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 926 KB/s], Decompressed: 3619
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 333 KB/s], Decompressed: 3657
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 188 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 361 KB/s], Decompressed: 3739
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 427 KB/s], Decompressed: 3783
Downloaded: 3818 file(s) [attempted 3818/8459 = 45%, 514 KB/s], Decompressed: 3814
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 466 KB/s], Decompressed: 3855
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 61 KB/s], Decompressed: 3900
Downloaded: 3945 file(s) [attempted 3945/8459 = 46%, 262 KB/s], Decompressed: 3937
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 85 KB/s], Decompressed: 3982
Downloaded: 4023 file(s) [attempted 4023/8459 = 47%, 42 KB/s], Decompressed: 4009
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 379 KB/s], Decompressed: 4057
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 150 KB/s], Decompressed: 4098
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 90 KB/s], Decompressed: 4139
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 451 KB/s], Decompressed: 4180
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 291 KB/s], Decompressed: 4214
Downloaded: 4256 file(s) [attempted 4256/8459 = 50%, 609 KB/s], Decompressed: 4252
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 367 KB/s], Decompressed: 4297
Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 49 KB/s], Decompressed: 4341
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 806 KB/s], Decompressed: 4379
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 135 KB/s], Decompressed: 4396
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 106 KB/s], Decompressed: 4454
Downloaded: 4502 file(s) [attempted 4502/8459 = 53%, 861 KB/s], Decompressed: 4481
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 963 KB/s], Decompressed: 4536
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 161 KB/s], Decompressed: 4581
Downloaded: 4622 file(s) [attempted 4622/8459 = 54%, 162 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 1192 KB/s], Decompressed: 4656
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 201 KB/s], Decompressed: 4697
Downloaded: 4743 file(s) [attempted 4743/8459 = 56%, 277 KB/s], Decompressed: 4738
Downloaded: 4788 file(s) [attempted 4788/8459 = 56%, 598 KB/s], Decompressed: 4783
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 188 KB/s], Decompressed: 4813
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 71 KB/s], Decompressed: 4854
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 232 KB/s], Decompressed: 4899
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 20 KB/s], Decompressed: 4940
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 55 KB/s], Decompressed: 4967
Downloaded: 5026 file(s) [attempted 5026/8459 = 59%, 148 KB/s], Decompressed: 5019
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 386 KB/s], Decompressed: 5056
Downloaded: 5103 file(s) [attempted 5103/8459 = 60%, 750 KB/s], Decompressed: 5097
Downloaded: 5139 file(s) [attempted 5139/8459 = 60%, 97 KB/s], Decompressed: 5135
Downloaded: 5180 file(s) [attempted 5180/8459 = 61%, 340 KB/s], Decompressed: 5173
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 57 KB/s], Decompressed: 5217
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 734 KB/s], Decompressed: 5250
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 60 KB/s], Decompressed: 5293
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 389 KB/s], Decompressed: 5327
Downloaded: 5377 file(s) [attempted 5377/8459 = 63%, 159 KB/s], Decompressed: 5371
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 483 KB/s], Decompressed: 5405
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 461 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 113 KB/s], Decompressed: 5481
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 115 KB/s], Decompressed: 5525
Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 171 KB/s], Decompressed: 5566
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 187 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 134 KB/s], Decompressed: 5631
Downloaded: 5683 file(s) [attempted 5683/8459 = 67%, 69 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 284 KB/s], Decompressed: 5720
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 389 KB/s], Decompressed: 5751
Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 103 KB/s], Decompressed: 5799
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 226 KB/s], Decompressed: 5837
Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 56 KB/s], Decompressed: 5878
Downloaded: 5926 file(s) [attempted 5926/8459 = 70%, 129 KB/s], Decompressed: 5922
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 231 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 542 KB/s], Decompressed: 5994
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 655 KB/s], Decompressed: 6035
Downloaded: 6082 file(s) [attempted 6082/8459 = 71%, 140 KB/s], Decompressed: 6073
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 757 KB/s], Decompressed: 6117
Downloaded: 6158 file(s) [attempted 6158/8459 = 72%, 70 KB/s], Decompressed: 6152
Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 441 KB/s], Decompressed: 6189
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 1021 KB/s], Decompressed: 6227
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 278 KB/s], Decompressed: 6271
Downloaded: 6313 file(s) [attempted 6313/8459 = 74%, 487 KB/s], Decompressed: 6306
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 321 KB/s], Decompressed: 6350
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 68 KB/s], Decompressed: 6388
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 271 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 79 KB/s], Decompressed: 6463
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 436 KB/s], Decompressed: 6504
Downloaded: 6549 file(s) [attempted 6549/8459 = 77%, 110 KB/s], Decompressed: 6542
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 79 KB/s], Decompressed: 6579
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 822 KB/s], Decompressed: 6614
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 163 KB/s], Decompressed: 6651
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 104 KB/s], Decompressed: 6696
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 273 KB/s], Decompressed: 6740
Downloaded: 6783 file(s) [attempted 6783/8459 = 80%, 24 KB/s], Decompressed: 6774
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 163 KB/s], Decompressed: 6812
Downloaded: 6853 file(s) [attempted 6853/8459 = 81%, 261 KB/s], Decompressed: 6850
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 112 KB/s], Decompressed: 6898
Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 392 KB/s], Decompressed: 6942
Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 332 KB/s], Decompressed: 6976
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 78 KB/s], Decompressed: 7011
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 101 KB/s], Decompressed: 7055
Downloaded: 7101 file(s) [attempted 7101/8459 = 83%, 978 KB/s], Decompressed: 7093
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1598 KB/s], Decompressed: 7117
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 119 KB/s], Decompressed: 7158
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 330 KB/s], Decompressed: 7212
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 36 KB/s], Decompressed: 7250
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 542 KB/s], Decompressed: 7295
Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 862 KB/s], Decompressed: 7338
Downloaded: 7382 file(s) [attempted 7382/8459 = 87%, 61 KB/s], Decompressed: 7377
Downloaded: 7412 file(s) [attempted 7412/8459 = 87%, 164 KB/s], Decompressed: 7408
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 929 KB/s], Decompressed: 7449
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 463 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 2211 KB/s], Decompressed: 7531
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 266 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 201 KB/s], Decompressed: 7603
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 43 KB/s], Decompressed: 7644
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 22 KB/s], Decompressed: 7685
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 74 KB/s], Decompressed: 7722
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 321 KB/s], Decompressed: 7750
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 453 KB/s], Decompressed: 7805
Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 48 KB/s], Decompressed: 7835
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 399 KB/s], Decompressed: 7880
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 99 KB/s], Decompressed: 7917
Downloaded: 7960 file(s) [attempted 7960/8459 = 94%, 816 KB/s], Decompressed: 7955
Downloaded: 7994 file(s) [attempted 7994/8459 = 94%, 1342 KB/s], Decompressed: 7989
Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 148 KB/s], Decompressed: 8027
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 307 KB/s], Decompressed: 8058
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 639 KB/s], Decompressed: 8109
Downloaded: 8163 file(s) [attempted 8163/8459 = 96%, 24 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 142 KB/s], Decompressed: 8191
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 194 KB/s], Decompressed: 8236
Downloaded: 8277 file(s) [attempted 8277/8459 = 97%, 111 KB/s], Decompressed: 8270
Downloaded: 8318 file(s) [attempted 8318/8459 = 98%, 369 KB/s], Decompressed: 8314
Downloaded: 8357 file(s) [attempted 8357/8459 = 98%, 415 KB/s], Decompressed: 8352
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 532 KB/s], Decompressed: 8390
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 696 KB/s], Decompressed: 8431
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 110 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 110 KB/s], Decompressed: 8451


$ lake build
exit_code=Some(1) duration_ms=448624
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (84s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
  simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
    hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (19s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.5s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (24s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (169s)
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/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI

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=1262
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`


blueprint_build failed; continuing (non-fatal phase).

Command runs

lake_cache exit 0 duration 34s · created 7/13/2026, 8:32:26 AM

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%, 2 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 28 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 345 KB/s], Decompressed: 61
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 241 KB/s], Decompressed: 86
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 281 KB/s], Decompressed: 117
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 82 KB/s], Decompressed: 148
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 397 KB/s], Decompressed: 179
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 595 KB/s], Decompressed: 216
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 214 KB/s], Decompressed: 240
Downloaded: 292 file(s) [attempted 292/8459 = 3%, 180 KB/s], Decompressed: 275
Downloaded: 331 file(s) [attempted 331/8459 = 3%, 133 KB/s], Decompressed: 326
Downloaded: 367 file(s) [attempted 367/8459 = 4%, 292 KB/s], Decompressed: 364
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 459 KB/s], Decompressed: 405
Downloaded: 449 file(s) [attempted 449/8459 = 5%, 588 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 247 KB/s], Decompressed: 480
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 208 KB/s], Decompressed: 525
Downloaded: 568 file(s) [attempted 568/8459 = 6%, 164 KB/s], Decompressed: 562
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 150 KB/s], Decompressed: 604
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 170 KB/s], Decompressed: 645
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 253 KB/s], Decompressed: 665
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 97 KB/s], Decompressed: 723
Downloaded: 762 file(s) [attempted 762/8459 = 9%, 513 KB/s], Decompressed: 758
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 857 KB/s], Decompressed: 795
Downloaded: 840 file(s) [attempted 840/8459 = 9%, 166 KB/s], Decompressed: 836
Downloaded: 878 file(s) [attempted 878/8459 = 10%, 70 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 149 KB/s], Decompressed: 915
Downloaded: 958 file(s) [attempted 958/8459 = 11%, 134 KB/s], Decompressed: 949
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 147 KB/s], Decompressed: 991
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 536 KB/s], Decompressed: 1035
Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 877 KB/s], Decompressed: 1069
Downloaded: 1115 file(s) [attempted 1115/8459 = 13%, 79 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 2000 KB/s], Decompressed: 1148
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 618 KB/s], Decompressed: 1186
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 84 KB/s], Decompressed: 1223
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 603 KB/s], Decompressed: 1261
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 511 KB/s], Decompressed: 1295
Downloaded: 1341 file(s) [attempted 1341/8459 = 15%, 42 KB/s], Decompressed: 1336
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1370
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 76 KB/s], Decompressed: 1415
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 44 KB/s], Decompressed: 1456
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 165 KB/s], Decompressed: 1490
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 473 KB/s], Decompressed: 1531
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 264 KB/s], Decompressed: 1569
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 458 KB/s], Decompressed: 1613
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 129 KB/s], Decompressed: 1651
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 459 KB/s], Decompressed: 1692
Downloaded: 1741 file(s) [attempted 1741/8459 = 20%, 50 KB/s], Decompressed: 1733
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 1090 KB/s], Decompressed: 1774
Downloaded: 1821 file(s) [attempted 1821/8459 = 21%, 325 KB/s], Decompressed: 1812
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 32 KB/s], Decompressed: 1850
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 41 KB/s], Decompressed: 1894
Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 337 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 38 KB/s], Decompressed: 1966
Downloaded: 2011 file(s) [attempted 2011/8459 = 23%, 415 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 408 KB/s], Decompressed: 2041
Downloaded: 2087 file(s) [attempted 2087/8459 = 24%, 78 KB/s], Decompressed: 2082
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 104 KB/s], Decompressed: 2127
Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 54 KB/s], Decompressed: 2158
Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 230 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 302 KB/s], Decompressed: 2240
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 311 KB/s], Decompressed: 2281
Downloaded: 2324 file(s) [attempted 2324/8459 = 27%, 40 KB/s], Decompressed: 2318
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 1254 KB/s], Decompressed: 2356
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 314 KB/s], Decompressed: 2390
Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 395 KB/s], Decompressed: 2435
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 143 KB/s], Decompressed: 2483
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 239 KB/s], Decompressed: 2517
Downloaded: 2566 file(s) [attempted 2566/8459 = 30%, 312 KB/s], Decompressed: 2561
Downloaded: 2604 file(s) [attempted 2604/8459 = 30%, 22 KB/s], Decompressed: 2596
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 724 KB/s], Decompressed: 2609
Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 60 KB/s], Decompressed: 2674
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 1205 KB/s], Decompressed: 2712
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 22 KB/s], Decompressed: 2753
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1187 KB/s], Decompressed: 2794
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 50 KB/s], Decompressed: 2825
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 526 KB/s], Decompressed: 2873
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 87 KB/s], Decompressed: 2907
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 42 KB/s], Decompressed: 2952
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 445 KB/s], Decompressed: 2996
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 156 KB/s], Decompressed: 3030
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 209 KB/s], Decompressed: 3071
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 74 KB/s], Decompressed: 3112
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 250 KB/s], Decompressed: 3150
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 24 KB/s], Decompressed: 3174
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 395 KB/s], Decompressed: 3229
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 505 KB/s], Decompressed: 3270
Downloaded: 3312 file(s) [attempted 3312/8459 = 39%, 1163 KB/s], Decompressed: 3304
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 233 KB/s], Decompressed: 3345
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 93 KB/s], Decompressed: 3376
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 111 KB/s], Decompressed: 3424
Downloaded: 3470 file(s) [attempted 3470/8459 = 41%, 690 KB/s], Decompressed: 3462
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 281 KB/s], Decompressed: 3503
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 513 KB/s], Decompressed: 3547
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 272 KB/s], Decompressed: 3581
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 926 KB/s], Decompressed: 3619
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 333 KB/s], Decompressed: 3657
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 188 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 361 KB/s], Decompressed: 3739
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 427 KB/s], Decompressed: 3783
Downloaded: 3818 file(s) [attempted 3818/8459 = 45%, 514 KB/s], Decompressed: 3814
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 466 KB/s], Decompressed: 3855
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 61 KB/s], Decompressed: 3900
Downloaded: 3945 file(s) [attempted 3945/8459 = 46%, 262 KB/s], Decompressed: 3937
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 85 KB/s], Decompressed: 3982
Downloaded: 4023 file(s) [attempted 4023/8459 = 47%, 42 KB/s], Decompressed: 4009
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 379 KB/s], Decompressed: 4057
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 150 KB/s], Decompressed: 4098
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 90 KB/s], Decompressed: 4139
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 451 KB/s], Decompressed: 4180
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 291 KB/s], Decompressed: 4214
Downloaded: 4256 file(s) [attempted 4256/8459 = 50%, 609 KB/s], Decompressed: 4252
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 367 KB/s], Decompressed: 4297
Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 49 KB/s], Decompressed: 4341
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 806 KB/s], Decompressed: 4379
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 135 KB/s], Decompressed: 4396
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 106 KB/s], Decompressed: 4454
Downloaded: 4502 file(s) [attempted 4502/8459 = 53%, 861 KB/s], Decompressed: 4481
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 963 KB/s], Decompressed: 4536
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 161 KB/s], Decompressed: 4581
Downloaded: 4622 file(s) [attempted 4622/8459 = 54%, 162 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 1192 KB/s], Decompressed: 4656
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 201 KB/s], Decompressed: 4697
Downloaded: 4743 file(s) [attempted 4743/8459 = 56%, 277 KB/s], Decompressed: 4738
Downloaded: 4788 file(s) [attempted 4788/8459 = 56%, 598 KB/s], Decompressed: 4783
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 188 KB/s], Decompressed: 4813
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 71 KB/s], Decompressed: 4854
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 232 KB/s], Decompressed: 4899
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 20 KB/s], Decompressed: 4940
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 55 KB/s], Decompressed: 4967
Downloaded: 5026 file(s) [attempted 5026/8459 = 59%, 148 KB/s], Decompressed: 5019
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 386 KB/s], Decompressed: 5056
Downloaded: 5103 file(s) [attempted 5103/8459 = 60%, 750 KB/s], Decompressed: 5097
Downloaded: 5139 file(s) [attempted 5139/8459 = 60%, 97 KB/s], Decompressed: 5135
Downloaded: 5180 file(s) [attempted 5180/8459 = 61%, 340 KB/s], Decompressed: 5173
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 57 KB/s], Decompressed: 5217
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 734 KB/s], Decompressed: 5250
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 60 KB/s], Decompressed: 5293
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 389 KB/s], Decompressed: 5327
Downloaded: 5377 file(s) [attempted 5377/8459 = 63%, 159 KB/s], Decompressed: 5371
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 483 KB/s], Decompressed: 5405
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 461 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 113 KB/s], Decompressed: 5481
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 115 KB/s], Decompressed: 5525
Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 171 KB/s], Decompressed: 5566
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 187 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 134 KB/s], Decompressed: 5631
Downloaded: 5683 file(s) [attempted 5683/8459 = 67%, 69 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 284 KB/s], Decompressed: 5720
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 389 KB/s], Decompressed: 5751
Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 103 KB/s], Decompressed: 5799
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 226 KB/s], Decompressed: 5837
Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 56 KB/s], Decompressed: 5878
Downloaded: 5926 file(s) [attempted 5926/8459 = 70%, 129 KB/s], Decompressed: 5922
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 231 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 542 KB/s], Decompressed: 5994
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 655 KB/s], Decompressed: 6035
Downloaded: 6082 file(s) [attempted 6082/8459 = 71%, 140 KB/s], Decompressed: 6073
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 757 KB/s], Decompressed: 6117
Downloaded: 6158 file(s) [attempted 6158/8459 = 72%, 70 KB/s], Decompressed: 6152
Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 441 KB/s], Decompressed: 6189
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 1021 KB/s], Decompressed: 6227
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 278 KB/s], Decompressed: 6271
Downloaded: 6313 file(s) [attempted 6313/8459 = 74%, 487 KB/s], Decompressed: 6306
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 321 KB/s], Decompressed: 6350
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 68 KB/s], Decompressed: 6388
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 271 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 79 KB/s], Decompressed: 6463
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 436 KB/s], Decompressed: 6504
Downloaded: 6549 file(s) [attempted 6549/8459 = 77%, 110 KB/s], Decompressed: 6542
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 79 KB/s], Decompressed: 6579
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 822 KB/s], Decompressed: 6614
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 163 KB/s], Decompressed: 6651
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 104 KB/s], Decompressed: 6696
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 273 KB/s], Decompressed: 6740
Downloaded: 6783 file(s) [attempted 6783/8459 = 80%, 24 KB/s], Decompressed: 6774
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 163 KB/s], Decompressed: 6812
Downloaded: 6853 file(s) [attempted 6853/8459 = 81%, 261 KB/s], Decompressed: 6850
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 112 KB/s], Decompressed: 6898
Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 392 KB/s], Decompressed: 6942
Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 332 KB/s], Decompressed: 6976
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 78 KB/s], Decompressed: 7011
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 101 KB/s], Decompressed: 7055
Downloaded: 7101 file(s) [attempted 7101/8459 = 83%, 978 KB/s], Decompressed: 7093
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1598 KB/s], Decompressed: 7117
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 119 KB/s], Decompressed: 7158
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 330 KB/s], Decompressed: 7212
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 36 KB/s], Decompressed: 7250
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 542 KB/s], Decompressed: 7295
Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 862 KB/s], Decompressed: 7338
Downloaded: 7382 file(s) [attempted 7382/8459 = 87%, 61 KB/s], Decompressed: 7377
Downloaded: 7412 file(s) [attempted 7412/8459 = 87%, 164 KB/s], Decompressed: 7408
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 929 KB/s], Decompressed: 7449
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 463 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 2211 KB/s], Decompressed: 7531
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 266 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 201 KB/s], Decompressed: 7603
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 43 KB/s], Decompressed: 7644
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 22 KB/s], Decompressed: 7685
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 74 KB/s], Decompressed: 7722
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 321 KB/s], Decompressed: 7750
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 453 KB/s], Decompressed: 7805
Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 48 KB/s], Decompressed: 7835
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 399 KB/s], Decompressed: 7880
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 99 KB/s], Decompressed: 7917
Downloaded: 7960 file(s) [attempted 7960/8459 = 94%, 816 KB/s], Decompressed: 7955
Downloaded: 7994 file(s) [attempted 7994/8459 = 94%, 1342 KB/s], Decompressed: 7989
Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 148 KB/s], Decompressed: 8027
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 307 KB/s], Decompressed: 8058
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 639 KB/s], Decompressed: 8109
Downloaded: 8163 file(s) [attempted 8163/8459 = 96%, 24 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 142 KB/s], Decompressed: 8191
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 194 KB/s], Decompressed: 8236
Downloaded: 8277 file(s) [attempted 8277/8459 = 97%, 111 KB/s], Decompressed: 8270
Downloaded: 8318 file(s) [attempted 8318/8459 = 98%, 369 KB/s], Decompressed: 8314
Downloaded: 8357 file(s) [attempted 8357/8459 = 98%, 415 KB/s], Decompressed: 8352
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 532 KB/s], Decompressed: 8390
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 696 KB/s], Decompressed: 8431
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 110 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 110 KB/s], Decompressed: 8451

lean_checker exit 1 duration 7m 29s · created 7/13/2026, 8:32:26 AM

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (84s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
  simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
    hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (19s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.5s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (24s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (169s)
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/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI

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 1s · created 7/13/2026, 8:32:26 AM

lake build :blueprint

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`

git_clone exit 0 duration 4s · created 7/13/2026, 8:32:26 AM

git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1370-source

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

git_checkout exit 0 duration 175 ms · created 7/13/2026, 8:32:26 AM

git checkout a5257f7d7b4a0e3a64866ecbcb8743de6796c22f

Note: switching to 'a5257f7d7b4a0e3a64866ecbcb8743de6796c22f'.

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 a5257f7 Lower final goal evidence through packet