Verification run
Run 1072
failed commit
19bbebf0838d toolchain lean-v4-30-0 prover lean took 11m 17s · 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)
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-1374-source
exit_code=Some(0) duration_ms=3204
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1374-source'...
$ git checkout 19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525
exit_code=Some(0) duration_ms=67
stderr:
Note: switching to '19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525'.
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 19bbebf Thread IUT IV localized packet data
Resolved source revision: 19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525 provenance={"branch":"master","checked_out_revision":"19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525","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=33670
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%, 12 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 7 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 23 KB/s], Decompressed: 39
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 32 KB/s], Decompressed: 61
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 53 KB/s], Decompressed: 89
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 164 KB/s], Decompressed: 121
Downloaded: 152 file(s) [attempted 152/8459 = 1%, 125 KB/s], Decompressed: 145
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 387 KB/s], Decompressed: 186
Downloaded: 227 file(s) [attempted 227/8459 = 2%, 277 KB/s], Decompressed: 220
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 1388 KB/s], Decompressed: 264
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 774 KB/s], Decompressed: 299
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 36 KB/s], Decompressed: 340
Downloaded: 385 file(s) [attempted 385/8459 = 4%, 40 KB/s], Decompressed: 374
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 86 KB/s], Decompressed: 412
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 203 KB/s], Decompressed: 453
Downloaded: 497 file(s) [attempted 497/8459 = 5%, 421 KB/s], Decompressed: 490
Downloaded: 535 file(s) [attempted 535/8459 = 6%, 344 KB/s], Decompressed: 528
Downloaded: 576 file(s) [attempted 576/8459 = 6%, 548 KB/s], Decompressed: 569
Downloaded: 614 file(s) [attempted 614/8459 = 7%, 434 KB/s], Decompressed: 607
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 244 KB/s], Decompressed: 645
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 199 KB/s], Decompressed: 682
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 71 KB/s], Decompressed: 723
Downloaded: 768 file(s) [attempted 768/8459 = 9%, 1139 KB/s], Decompressed: 761
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 31 KB/s], Decompressed: 802
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 981 KB/s], Decompressed: 840
Downloaded: 888 file(s) [attempted 888/8459 = 10%, 1340 KB/s], Decompressed: 884
Downloaded: 929 file(s) [attempted 929/8459 = 10%, 19 KB/s], Decompressed: 925
Downloaded: 971 file(s) [attempted 971/8459 = 11%, 86 KB/s], Decompressed: 963
Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 63 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 101 KB/s], Decompressed: 1042
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 204 KB/s], Decompressed: 1076
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 142 KB/s], Decompressed: 1117
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 280 KB/s], Decompressed: 1158
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 104 KB/s], Decompressed: 1196
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 33 KB/s], Decompressed: 1237
Downloaded: 1283 file(s) [attempted 1283/8459 = 15%, 201 KB/s], Decompressed: 1278
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 92 KB/s], Decompressed: 1319
Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 243 KB/s], Decompressed: 1364
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 228 KB/s], Decompressed: 1401
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 53 KB/s], Decompressed: 1435
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 56 KB/s], Decompressed: 1480
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 310 KB/s], Decompressed: 1524
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 156 KB/s], Decompressed: 1569
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 85 KB/s], Decompressed: 1603
Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 195 KB/s], Decompressed: 1641
Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 27 KB/s], Decompressed: 1678
Downloaded: 1725 file(s) [attempted 1725/8459 = 20%, 157 KB/s], Decompressed: 1720
Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 142 KB/s], Decompressed: 1757
Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 277 KB/s], Decompressed: 1798
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 399 KB/s], Decompressed: 1832
Downloaded: 1878 file(s) [attempted 1878/8459 = 22%, 121 KB/s], Decompressed: 1874
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 65 KB/s], Decompressed: 1911
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 74 KB/s], Decompressed: 1952
Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 48 KB/s], Decompressed: 1993
Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 626 KB/s], Decompressed: 2031
Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 22 KB/s], Decompressed: 2072
Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 344 KB/s], Decompressed: 2110
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 171 KB/s], Decompressed: 2147
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 705 KB/s], Decompressed: 2192
Downloaded: 2234 file(s) [attempted 2234/8459 = 26%, 149 KB/s], Decompressed: 2229
Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 351 KB/s], Decompressed: 2267
Downloaded: 2316 file(s) [attempted 2316/8459 = 27%, 407 KB/s], Decompressed: 2308
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 375 KB/s], Decompressed: 2349
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 475 KB/s], Decompressed: 2390
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 581 KB/s], Decompressed: 2428
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 449 KB/s], Decompressed: 2476
Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 137 KB/s], Decompressed: 2507
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 96 KB/s], Decompressed: 2551
Downloaded: 2594 file(s) [attempted 2594/8459 = 30%, 134 KB/s], Decompressed: 2589
Downloaded: 2633 file(s) [attempted 2633/8459 = 31%, 68 KB/s], Decompressed: 2630
Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 171 KB/s], Decompressed: 2664
Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 431 KB/s], Decompressed: 2705
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 121 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 158 KB/s], Decompressed: 2787
Downloaded: 2829 file(s) [attempted 2829/8459 = 33%, 922 KB/s], Decompressed: 2825
Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 24 KB/s], Decompressed: 2866
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 133 KB/s], Decompressed: 2907
Downloaded: 2952 file(s) [attempted 2952/8459 = 34%, 645 KB/s], Decompressed: 2948
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 205 KB/s], Decompressed: 2986
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 112 KB/s], Decompressed: 3027
Downloaded: 3074 file(s) [attempted 3074/8459 = 36%, 900 KB/s], Decompressed: 3068
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 206 KB/s], Decompressed: 3109
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 320 KB/s], Decompressed: 3140
Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 206 KB/s], Decompressed: 3184
Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 161 KB/s], Decompressed: 3219
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 256 KB/s], Decompressed: 3266
Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 686 KB/s], Decompressed: 3304
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 556 KB/s], Decompressed: 3338
Downloaded: 3385 file(s) [attempted 3385/8459 = 40%, 43 KB/s], Decompressed: 3379
Downloaded: 3424 file(s) [attempted 3424/8459 = 40%, 185 KB/s], Decompressed: 3420
Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 592 KB/s], Decompressed: 3462
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 874 KB/s], Decompressed: 3506
Downloaded: 3550 file(s) [attempted 3550/8459 = 41%, 756 KB/s], Decompressed: 3547
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 394 KB/s], Decompressed: 3581
Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 1671 KB/s], Decompressed: 3619
Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 231 KB/s], Decompressed: 3663
Downloaded: 3708 file(s) [attempted 3708/8459 = 43%, 605 KB/s], Decompressed: 3705
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 381 KB/s], Decompressed: 3732
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 354 KB/s], Decompressed: 3766
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 126 KB/s], Decompressed: 3817
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 55 KB/s], Decompressed: 3859
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 63 KB/s], Decompressed: 3900
Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 216 KB/s], Decompressed: 3941
Downloaded: 3989 file(s) [attempted 3989/8459 = 47%, 26 KB/s], Decompressed: 3985
Downloaded: 4025 file(s) [attempted 4025/8459 = 47%, 621 KB/s], Decompressed: 4019
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 101 KB/s], Decompressed: 4057
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 39 KB/s], Decompressed: 4098
Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 523 KB/s], Decompressed: 4139
Downloaded: 4186 file(s) [attempted 4186/8459 = 49%, 956 KB/s], Decompressed: 4177
Downloaded: 4226 file(s) [attempted 4226/8459 = 49%, 267 KB/s], Decompressed: 4218
Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 75 KB/s], Decompressed: 4256
Downloaded: 4295 file(s) [attempted 4295/8459 = 50%, 87 KB/s], Decompressed: 4290
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 163 KB/s], Decompressed: 4338
Downloaded: 4388 file(s) [attempted 4388/8459 = 51%, 354 KB/s], Decompressed: 4382
Downloaded: 4429 file(s) [attempted 4429/8459 = 52%, 113 KB/s], Decompressed: 4423
Downloaded: 4462 file(s) [attempted 4462/8459 = 52%, 150 KB/s], Decompressed: 4454
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 852 KB/s], Decompressed: 4492
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 22 KB/s], Decompressed: 4536
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 160 KB/s], Decompressed: 4581
Downloaded: 4630 file(s) [attempted 4630/8459 = 54%, 43 KB/s], Decompressed: 4615
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 55 KB/s], Decompressed: 4656
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 317 KB/s], Decompressed: 4697
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 239 KB/s], Decompressed: 4738
Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 134 KB/s], Decompressed: 4783
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 79 KB/s], Decompressed: 4817
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 67 KB/s], Decompressed: 4854
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 568 KB/s], Decompressed: 4902
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 414 KB/s], Decompressed: 4940
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 331 KB/s], Decompressed: 4971
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 147 KB/s], Decompressed: 5015
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 46 KB/s], Decompressed: 5056
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 115 KB/s], Decompressed: 5097
Downloaded: 5143 file(s) [attempted 5143/8459 = 60%, 200 KB/s], Decompressed: 5139
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 93 KB/s], Decompressed: 5180
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 823 KB/s], Decompressed: 5217
Downloaded: 5262 file(s) [attempted 5262/8459 = 62%, 390 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 742 KB/s], Decompressed: 5296
Downloaded: 5338 file(s) [attempted 5338/8459 = 63%, 195 KB/s], Decompressed: 5334
Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 25 KB/s], Decompressed: 5371
Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 219 KB/s], Decompressed: 5402
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 875 KB/s], Decompressed: 5453
Downloaded: 5495 file(s) [attempted 5495/8459 = 64%, 214 KB/s], Decompressed: 5491
Downloaded: 5534 file(s) [attempted 5534/8459 = 65%, 632 KB/s], Decompressed: 5529
Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 71 KB/s], Decompressed: 5573
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 712 KB/s], Decompressed: 5601
Downloaded: 5654 file(s) [attempted 5654/8459 = 66%, 48 KB/s], Decompressed: 5648
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 128 KB/s], Decompressed: 5689
Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 280 KB/s], Decompressed: 5718
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 113 KB/s], Decompressed: 5751
Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 580 KB/s], Decompressed: 5796
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 337 KB/s], Decompressed: 5823
Downloaded: 5881 file(s) [attempted 5881/8459 = 69%, 53 KB/s], Decompressed: 5878
Downloaded: 5921 file(s) [attempted 5921/8459 = 69%, 215 KB/s], Decompressed: 5909
Downloaded: 5949 file(s) [attempted 5949/8459 = 70%, 484 KB/s], Decompressed: 5940
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 153 KB/s], Decompressed: 5981
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 779 KB/s], Decompressed: 6029
Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 465 KB/s], Decompressed: 6073
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 201 KB/s], Decompressed: 6107
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 973 KB/s], Decompressed: 6138
Downloaded: 6183 file(s) [attempted 6183/8459 = 73%, 143 KB/s], Decompressed: 6179
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 209 KB/s], Decompressed: 6224
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 552 KB/s], Decompressed: 6275
Downloaded: 6323 file(s) [attempted 6323/8459 = 74%, 370 KB/s], Decompressed: 6319
Downloaded: 6367 file(s) [attempted 6367/8459 = 75%, 673 KB/s], Decompressed: 6360
Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 219 KB/s], Decompressed: 6395
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 205 KB/s], Decompressed: 6432
Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 49 KB/s], Decompressed: 6473
Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 116 KB/s], Decompressed: 6514
Downloaded: 6559 file(s) [attempted 6559/8459 = 77%, 369 KB/s], Decompressed: 6556
Downloaded: 6602 file(s) [attempted 6602/8459 = 78%, 595 KB/s], Decompressed: 6593
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 29 KB/s], Decompressed: 6627
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 62 KB/s], Decompressed: 6672
Downloaded: 6717 file(s) [attempted 6717/8459 = 79%, 366 KB/s], Decompressed: 6713
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 232 KB/s], Decompressed: 6751
Downloaded: 6795 file(s) [attempted 6795/8459 = 80%, 191 KB/s], Decompressed: 6781
Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 273 KB/s], Decompressed: 6809
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 348 KB/s], Decompressed: 6864
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 202 KB/s], Decompressed: 6905
Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 88 KB/s], Decompressed: 6949
Downloaded: 6995 file(s) [attempted 6995/8459 = 82%, 579 KB/s], Decompressed: 6973
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 334 KB/s], Decompressed: 7021
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1215 KB/s], Decompressed: 7055
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 179 KB/s], Decompressed: 7096
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1188 KB/s], Decompressed: 7137
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 87 KB/s], Decompressed: 7168
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 740 KB/s], Decompressed: 7213
Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 1008 KB/s], Decompressed: 7250
Downloaded: 7298 file(s) [attempted 7298/8459 = 86%, 579 KB/s], Decompressed: 7295
Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 503 KB/s], Decompressed: 7332
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 366 KB/s], Decompressed: 7374
Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 316 KB/s], Decompressed: 7408
Downloaded: 7456 file(s) [attempted 7456/8459 = 88%, 76 KB/s], Decompressed: 7449
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 128 KB/s], Decompressed: 7486
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 88 KB/s], Decompressed: 7528
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 67 KB/s], Decompressed: 7569
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 483 KB/s], Decompressed: 7610
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 125 KB/s], Decompressed: 7651
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 1035 KB/s], Decompressed: 7685
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 101 KB/s], Decompressed: 7728
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 81 KB/s], Decompressed: 7767
Downloaded: 7812 file(s) [attempted 7812/8459 = 92%, 301 KB/s], Decompressed: 7808
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 77 KB/s], Decompressed: 7842
Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 800 KB/s], Decompressed: 7883
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 215 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 215 KB/s], Decompressed: 7962
Downloaded: 8007 file(s) [attempted 8007/8459 = 94%, 254 KB/s], Decompressed: 8003
Downloaded: 8046 file(s) [attempted 8046/8459 = 95%, 369 KB/s], Decompressed: 8037
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 528 KB/s], Decompressed: 8082
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 153 KB/s], Decompressed: 8126
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 106 KB/s], Decompressed: 8157
Downloaded: 8202 file(s) [attempted 8202/8459 = 96%, 313 KB/s], Decompressed: 8198
Downloaded: 8244 file(s) [attempted 8244/8459 = 97%, 74 KB/s], Decompressed: 8239
Downloaded: 8284 file(s) [attempted 8284/8459 = 97%, 1034 KB/s], Decompressed: 8270
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 174 KB/s], Decompressed: 8321
Downloaded: 8368 file(s) [attempted 8368/8459 = 98%, 293 KB/s], Decompressed: 8359
Downloaded: 8404 file(s) [attempted 8404/8459 = 99%, 616 KB/s], Decompressed: 8400
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 831 KB/s], Decompressed: 8434
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 831 KB/s], Decompressed: 8452
$ lake build
exit_code=Some(1) duration_ms=456343
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (85s)
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 (24s)
⚠ [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.8s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.8s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (9.3s)
⚠ [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 (175s)
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=1182
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
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1374-source
Cloning into '/var/lib/apodeixis/repos/job-1374-source'...
git_checkout exit 0
git checkout 19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525
Note: switching to '19bbebf0838dc7d100ca8e8a4fc4d9c9f31fe525'. 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 19bbebf Thread IUT IV localized packet data
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 12 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 7 KB/s], Decompressed: 14 Downloaded: 41 file(s) [attempted 41/8459 = 0%, 23 KB/s], Decompressed: 39 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 32 KB/s], Decompressed: 61 Downloaded: 92 file(s) [attempted 92/8459 = 1%, 53 KB/s], Decompressed: 89 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 164 KB/s], Decompressed: 121 Downloaded: 152 file(s) [attempted 152/8459 = 1%, 125 KB/s], Decompressed: 145 Downloaded: 189 file(s) [attempted 189/8459 = 2%, 387 KB/s], Decompressed: 186 Downloaded: 227 file(s) [attempted 227/8459 = 2%, 277 KB/s], Decompressed: 220 Downloaded: 268 file(s) [attempted 268/8459 = 3%, 1388 KB/s], Decompressed: 264 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 774 KB/s], Decompressed: 299 Downloaded: 343 file(s) [attempted 343/8459 = 4%, 36 KB/s], Decompressed: 340 Downloaded: 385 file(s) [attempted 385/8459 = 4%, 40 KB/s], Decompressed: 374 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 86 KB/s], Decompressed: 412 Downloaded: 456 file(s) [attempted 456/8459 = 5%, 203 KB/s], Decompressed: 453 Downloaded: 497 file(s) [attempted 497/8459 = 5%, 421 KB/s], Decompressed: 490 Downloaded: 535 file(s) [attempted 535/8459 = 6%, 344 KB/s], Decompressed: 528 Downloaded: 576 file(s) [attempted 576/8459 = 6%, 548 KB/s], Decompressed: 569 Downloaded: 614 file(s) [attempted 614/8459 = 7%, 434 KB/s], Decompressed: 607 Downloaded: 648 file(s) [attempted 648/8459 = 7%, 244 KB/s], Decompressed: 645 Downloaded: 689 file(s) [attempted 689/8459 = 8%, 199 KB/s], Decompressed: 682 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 71 KB/s], Decompressed: 723 Downloaded: 768 file(s) [attempted 768/8459 = 9%, 1139 KB/s], Decompressed: 761 Downloaded: 806 file(s) [attempted 806/8459 = 9%, 31 KB/s], Decompressed: 802 Downloaded: 847 file(s) [attempted 847/8459 = 10%, 981 KB/s], Decompressed: 840 Downloaded: 888 file(s) [attempted 888/8459 = 10%, 1340 KB/s], Decompressed: 884 Downloaded: 929 file(s) [attempted 929/8459 = 10%, 19 KB/s], Decompressed: 925 Downloaded: 971 file(s) [attempted 971/8459 = 11%, 86 KB/s], Decompressed: 963 Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 63 KB/s], Decompressed: 997 Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 101 KB/s], Decompressed: 1042 Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 204 KB/s], Decompressed: 1076 Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 142 KB/s], Decompressed: 1117 Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 280 KB/s], Decompressed: 1158 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 104 KB/s], Decompressed: 1196 Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 33 KB/s], Decompressed: 1237 Downloaded: 1283 file(s) [attempted 1283/8459 = 15%, 201 KB/s], Decompressed: 1278 Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 92 KB/s], Decompressed: 1319 Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 243 KB/s], Decompressed: 1364 Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 228 KB/s], Decompressed: 1401 Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 53 KB/s], Decompressed: 1435 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 56 KB/s], Decompressed: 1480 Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 310 KB/s], Decompressed: 1524 Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 156 KB/s], Decompressed: 1569 Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 85 KB/s], Decompressed: 1603 Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 195 KB/s], Decompressed: 1641 Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 27 KB/s], Decompressed: 1678 Downloaded: 1725 file(s) [attempted 1725/8459 = 20%, 157 KB/s], Decompressed: 1720 Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 142 KB/s], Decompressed: 1757 Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 277 KB/s], Decompressed: 1798 Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 399 KB/s], Decompressed: 1832 Downloaded: 1878 file(s) [attempted 1878/8459 = 22%, 121 KB/s], Decompressed: 1874 Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 65 KB/s], Decompressed: 1911 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 74 KB/s], Decompressed: 1952 Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 48 KB/s], Decompressed: 1993 Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 626 KB/s], Decompressed: 2031 Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 22 KB/s], Decompressed: 2072 Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 344 KB/s], Decompressed: 2110 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 171 KB/s], Decompressed: 2147 Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 705 KB/s], Decompressed: 2192 Downloaded: 2234 file(s) [attempted 2234/8459 = 26%, 149 KB/s], Decompressed: 2229 Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 351 KB/s], Decompressed: 2267 Downloaded: 2316 file(s) [attempted 2316/8459 = 27%, 407 KB/s], Decompressed: 2308 Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 375 KB/s], Decompressed: 2349 Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 475 KB/s], Decompressed: 2390 Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 581 KB/s], Decompressed: 2428 Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 449 KB/s], Decompressed: 2476 Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 137 KB/s], Decompressed: 2507 Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 96 KB/s], Decompressed: 2551 Downloaded: 2594 file(s) [attempted 2594/8459 = 30%, 134 KB/s], Decompressed: 2589 Downloaded: 2633 file(s) [attempted 2633/8459 = 31%, 68 KB/s], Decompressed: 2630 Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 171 KB/s], Decompressed: 2664 Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 431 KB/s], Decompressed: 2705 Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 121 KB/s], Decompressed: 2750 Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 158 KB/s], Decompressed: 2787 Downloaded: 2829 file(s) [attempted 2829/8459 = 33%, 922 KB/s], Decompressed: 2825 Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 24 KB/s], Decompressed: 2866 Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 133 KB/s], Decompressed: 2907 Downloaded: 2952 file(s) [attempted 2952/8459 = 34%, 645 KB/s], Decompressed: 2948 Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 205 KB/s], Decompressed: 2986 Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 112 KB/s], Decompressed: 3027 Downloaded: 3074 file(s) [attempted 3074/8459 = 36%, 900 KB/s], Decompressed: 3068 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 206 KB/s], Decompressed: 3109 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 320 KB/s], Decompressed: 3140 Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 206 KB/s], Decompressed: 3184 Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 161 KB/s], Decompressed: 3219 Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 256 KB/s], Decompressed: 3266 Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 686 KB/s], Decompressed: 3304 Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 556 KB/s], Decompressed: 3338 Downloaded: 3385 file(s) [attempted 3385/8459 = 40%, 43 KB/s], Decompressed: 3379 Downloaded: 3424 file(s) [attempted 3424/8459 = 40%, 185 KB/s], Decompressed: 3420 Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 592 KB/s], Decompressed: 3462 Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 874 KB/s], Decompressed: 3506 Downloaded: 3550 file(s) [attempted 3550/8459 = 41%, 756 KB/s], Decompressed: 3547 Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 394 KB/s], Decompressed: 3581 Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 1671 KB/s], Decompressed: 3619 Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 231 KB/s], Decompressed: 3663 Downloaded: 3708 file(s) [attempted 3708/8459 = 43%, 605 KB/s], Decompressed: 3705 Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 381 KB/s], Decompressed: 3732 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 354 KB/s], Decompressed: 3766 Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 126 KB/s], Decompressed: 3817 Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 55 KB/s], Decompressed: 3859 Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 63 KB/s], Decompressed: 3900 Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 216 KB/s], Decompressed: 3941 Downloaded: 3989 file(s) [attempted 3989/8459 = 47%, 26 KB/s], Decompressed: 3985 Downloaded: 4025 file(s) [attempted 4025/8459 = 47%, 621 KB/s], Decompressed: 4019 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 101 KB/s], Decompressed: 4057 Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 39 KB/s], Decompressed: 4098 Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 523 KB/s], Decompressed: 4139 Downloaded: 4186 file(s) [attempted 4186/8459 = 49%, 956 KB/s], Decompressed: 4177 Downloaded: 4226 file(s) [attempted 4226/8459 = 49%, 267 KB/s], Decompressed: 4218 Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 75 KB/s], Decompressed: 4256 Downloaded: 4295 file(s) [attempted 4295/8459 = 50%, 87 KB/s], Decompressed: 4290 Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 163 KB/s], Decompressed: 4338 Downloaded: 4388 file(s) [attempted 4388/8459 = 51%, 354 KB/s], Decompressed: 4382 Downloaded: 4429 file(s) [attempted 4429/8459 = 52%, 113 KB/s], Decompressed: 4423 Downloaded: 4462 file(s) [attempted 4462/8459 = 52%, 150 KB/s], Decompressed: 4454 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 852 KB/s], Decompressed: 4492 Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 22 KB/s], Decompressed: 4536 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 160 KB/s], Decompressed: 4581 Downloaded: 4630 file(s) [attempted 4630/8459 = 54%, 43 KB/s], Decompressed: 4615 Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 55 KB/s], Decompressed: 4656 Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 317 KB/s], Decompressed: 4697 Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 239 KB/s], Decompressed: 4738 Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 134 KB/s], Decompressed: 4783 Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 79 KB/s], Decompressed: 4817 Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 67 KB/s], Decompressed: 4854 Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 568 KB/s], Decompressed: 4902 Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 414 KB/s], Decompressed: 4940 Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 331 KB/s], Decompressed: 4971 Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 147 KB/s], Decompressed: 5015 Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 46 KB/s], Decompressed: 5056 Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 115 KB/s], Decompressed: 5097 Downloaded: 5143 file(s) [attempted 5143/8459 = 60%, 200 KB/s], Decompressed: 5139 Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 93 KB/s], Decompressed: 5180 Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 823 KB/s], Decompressed: 5217 Downloaded: 5262 file(s) [attempted 5262/8459 = 62%, 390 KB/s], Decompressed: 5255 Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 742 KB/s], Decompressed: 5296 Downloaded: 5338 file(s) [attempted 5338/8459 = 63%, 195 KB/s], Decompressed: 5334 Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 25 KB/s], Decompressed: 5371 Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 219 KB/s], Decompressed: 5402 Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 875 KB/s], Decompressed: 5453 Downloaded: 5495 file(s) [attempted 5495/8459 = 64%, 214 KB/s], Decompressed: 5491 Downloaded: 5534 file(s) [attempted 5534/8459 = 65%, 632 KB/s], Decompressed: 5529 Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 71 KB/s], Decompressed: 5573 Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 712 KB/s], Decompressed: 5601 Downloaded: 5654 file(s) [attempted 5654/8459 = 66%, 48 KB/s], Decompressed: 5648 Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 128 KB/s], Decompressed: 5689 Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 280 KB/s], Decompressed: 5718 Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 113 KB/s], Decompressed: 5751 Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 580 KB/s], Decompressed: 5796 Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 337 KB/s], Decompressed: 5823 Downloaded: 5881 file(s) [attempted 5881/8459 = 69%, 53 KB/s], Decompressed: 5878 Downloaded: 5921 file(s) [attempted 5921/8459 = 69%, 215 KB/s], Decompressed: 5909 Downloaded: 5949 file(s) [attempted 5949/8459 = 70%, 484 KB/s], Decompressed: 5940 Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 153 KB/s], Decompressed: 5981 Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 779 KB/s], Decompressed: 6029 Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 465 KB/s], Decompressed: 6073 Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 201 KB/s], Decompressed: 6107 Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 973 KB/s], Decompressed: 6138 Downloaded: 6183 file(s) [attempted 6183/8459 = 73%, 143 KB/s], Decompressed: 6179 Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 209 KB/s], Decompressed: 6224 Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 552 KB/s], Decompressed: 6275 Downloaded: 6323 file(s) [attempted 6323/8459 = 74%, 370 KB/s], Decompressed: 6319 Downloaded: 6367 file(s) [attempted 6367/8459 = 75%, 673 KB/s], Decompressed: 6360 Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 219 KB/s], Decompressed: 6395 Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 205 KB/s], Decompressed: 6432 Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 49 KB/s], Decompressed: 6473 Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 116 KB/s], Decompressed: 6514 Downloaded: 6559 file(s) [attempted 6559/8459 = 77%, 369 KB/s], Decompressed: 6556 Downloaded: 6602 file(s) [attempted 6602/8459 = 78%, 595 KB/s], Decompressed: 6593 Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 29 KB/s], Decompressed: 6627 Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 62 KB/s], Decompressed: 6672 Downloaded: 6717 file(s) [attempted 6717/8459 = 79%, 366 KB/s], Decompressed: 6713 Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 232 KB/s], Decompressed: 6751 Downloaded: 6795 file(s) [attempted 6795/8459 = 80%, 191 KB/s], Decompressed: 6781 Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 273 KB/s], Decompressed: 6809 Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 348 KB/s], Decompressed: 6864 Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 202 KB/s], Decompressed: 6905 Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 88 KB/s], Decompressed: 6949 Downloaded: 6995 file(s) [attempted 6995/8459 = 82%, 579 KB/s], Decompressed: 6973 Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 334 KB/s], Decompressed: 7021 Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1215 KB/s], Decompressed: 7055 Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 179 KB/s], Decompressed: 7096 Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1188 KB/s], Decompressed: 7137 Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 87 KB/s], Decompressed: 7168 Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 740 KB/s], Decompressed: 7213 Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 1008 KB/s], Decompressed: 7250 Downloaded: 7298 file(s) [attempted 7298/8459 = 86%, 579 KB/s], Decompressed: 7295 Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 503 KB/s], Decompressed: 7332 Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 366 KB/s], Decompressed: 7374 Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 316 KB/s], Decompressed: 7408 Downloaded: 7456 file(s) [attempted 7456/8459 = 88%, 76 KB/s], Decompressed: 7449 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 128 KB/s], Decompressed: 7486 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 88 KB/s], Decompressed: 7528 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 67 KB/s], Decompressed: 7569 Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 483 KB/s], Decompressed: 7610 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 125 KB/s], Decompressed: 7651 Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 1035 KB/s], Decompressed: 7685 Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 101 KB/s], Decompressed: 7728 Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 81 KB/s], Decompressed: 7767 Downloaded: 7812 file(s) [attempted 7812/8459 = 92%, 301 KB/s], Decompressed: 7808 Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 77 KB/s], Decompressed: 7842 Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 800 KB/s], Decompressed: 7883 Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 215 KB/s], Decompressed: 7928 Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 215 KB/s], Decompressed: 7962 Downloaded: 8007 file(s) [attempted 8007/8459 = 94%, 254 KB/s], Decompressed: 8003 Downloaded: 8046 file(s) [attempted 8046/8459 = 95%, 369 KB/s], Decompressed: 8037 Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 528 KB/s], Decompressed: 8082 Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 153 KB/s], Decompressed: 8126 Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 106 KB/s], Decompressed: 8157 Downloaded: 8202 file(s) [attempted 8202/8459 = 96%, 313 KB/s], Decompressed: 8198 Downloaded: 8244 file(s) [attempted 8244/8459 = 97%, 74 KB/s], Decompressed: 8239 Downloaded: 8284 file(s) [attempted 8284/8459 = 97%, 1034 KB/s], Decompressed: 8270 Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 174 KB/s], Decompressed: 8321 Downloaded: 8368 file(s) [attempted 8368/8459 = 98%, 293 KB/s], Decompressed: 8359 Downloaded: 8404 file(s) [attempted 8404/8459 = 99%, 616 KB/s], Decompressed: 8400 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 831 KB/s], Decompressed: 8434 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 831 KB/s], Decompressed: 8452
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (85s)
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 (24s)
⚠ [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.8s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.8s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (9.3s)
⚠ [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 (175s)
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
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`