Run 1049

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

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

git checkout 069488bb49afaf5f1a1702af6e884a9949845dc4

Note: switching to '069488bb49afaf5f1a1702af6e884a9949845dc4'.

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 069488b Bundle valuation ball named HDD boundary

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%, 11 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 3
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 15 KB/s], Decompressed: 3
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 185 KB/s], Decompressed: 50
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 500 KB/s], Decompressed: 79
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 287 KB/s], Decompressed: 112
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 284 KB/s], Decompressed: 148
Downloaded: 186 file(s) [attempted 186/8459 = 2%, 516 KB/s], Decompressed: 179
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 608 KB/s], Decompressed: 179
Downloaded: 256 file(s) [attempted 256/8459 = 3%, 593 KB/s], Decompressed: 182
Downloaded: 289 file(s) [attempted 289/8459 = 3%, 131 KB/s], Decompressed: 282
Downloaded: 327 file(s) [attempted 327/8459 = 3%, 313 KB/s], Decompressed: 319
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 150 KB/s], Decompressed: 343
Downloaded: 405 file(s) [attempted 405/8459 = 4%, 473 KB/s], Decompressed: 343
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 245 KB/s], Decompressed: 353
Downloaded: 489 file(s) [attempted 489/8459 = 5%, 271 KB/s], Decompressed: 484
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 735 KB/s], Decompressed: 525
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 482 KB/s], Decompressed: 560
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 229 KB/s], Decompressed: 593
Downloaded: 642 file(s) [attempted 642/8459 = 7%, 247 KB/s], Decompressed: 638
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 135 KB/s], Decompressed: 682
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 69 KB/s], Decompressed: 689
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 830 KB/s], Decompressed: 689
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 130 KB/s], Decompressed: 802
Downloaded: 852 file(s) [attempted 852/8459 = 10%, 183 KB/s], Decompressed: 812
Downloaded: 891 file(s) [attempted 891/8459 = 10%, 142 KB/s], Decompressed: 812
Downloaded: 930 file(s) [attempted 930/8459 = 10%, 1014 KB/s], Decompressed: 925
Downloaded: 970 file(s) [attempted 970/8459 = 11%, 283 KB/s], Decompressed: 963
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 351 KB/s], Decompressed: 1004
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 345 KB/s], Decompressed: 1004
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 60 KB/s], Decompressed: 1004
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 181 KB/s], Decompressed: 1104
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 136 KB/s], Decompressed: 1104
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 230 KB/s], Decompressed: 1121
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 205 KB/s], Decompressed: 1251
Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 704 KB/s], Decompressed: 1281
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 51 KB/s], Decompressed: 1329
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1374
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 871 KB/s], Decompressed: 1377
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 338 KB/s], Decompressed: 1377
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 192 KB/s], Decompressed: 1494
Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 153 KB/s], Decompressed: 1531
Downloaded: 1579 file(s) [attempted 1579/8459 = 18%, 545 KB/s], Decompressed: 1576
Downloaded: 1624 file(s) [attempted 1624/8459 = 19%, 568 KB/s], Decompressed: 1620
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 573 KB/s], Decompressed: 1655
Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 500 KB/s], Decompressed: 1702
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 94 KB/s], Decompressed: 1733
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 371 KB/s], Decompressed: 1781
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 706 KB/s], Decompressed: 1826
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1862 KB/s], Decompressed: 1863
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 91 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 165 KB/s], Decompressed: 1939
Downloaded: 1980 file(s) [attempted 1980/8459 = 23%, 141 KB/s], Decompressed: 1976
Downloaded: 2018 file(s) [attempted 2018/8459 = 23%, 59 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 40 KB/s], Decompressed: 2051
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 298 KB/s], Decompressed: 2062
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 1747 KB/s], Decompressed: 2062
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 433 KB/s], Decompressed: 2178
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 88 KB/s], Decompressed: 2219
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 102 KB/s], Decompressed: 2260
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 123 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 116 KB/s], Decompressed: 2298
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 278 KB/s], Decompressed: 2298
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 37 KB/s], Decompressed: 2308
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 870 KB/s], Decompressed: 2308
Downloaded: 2510 file(s) [attempted 2510/8459 = 29%, 264 KB/s], Decompressed: 2390
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 229 KB/s], Decompressed: 2390
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 156 KB/s], Decompressed: 2490
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 418 KB/s], Decompressed: 2490
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 368 KB/s], Decompressed: 2490
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 667 KB/s], Decompressed: 2709
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 103 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 647 KB/s], Decompressed: 2787
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 2221 KB/s], Decompressed: 2832
Downloaded: 2877 file(s) [attempted 2877/8459 = 34%, 1006 KB/s], Decompressed: 2869
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 275 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 480 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 186 KB/s], Decompressed: 2965
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 108 KB/s], Decompressed: 2965
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 784 KB/s], Decompressed: 3068
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 36 KB/s], Decompressed: 3106
Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 143 KB/s], Decompressed: 3112
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 1363 KB/s], Decompressed: 3123
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 211 KB/s], Decompressed: 3123
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 131 KB/s], Decompressed: 3263
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 215 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 115 KB/s], Decompressed: 3359
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 172 KB/s], Decompressed: 3410
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 48 KB/s], Decompressed: 3448
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 112 KB/s], Decompressed: 3489
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 143 KB/s], Decompressed: 3526
Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 744 KB/s], Decompressed: 3574
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1030 KB/s], Decompressed: 3615
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 263 KB/s], Decompressed: 3650
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 327 KB/s], Decompressed: 3650
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 380 KB/s], Decompressed: 3657
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 102 KB/s], Decompressed: 3759
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 25 KB/s], Decompressed: 3759
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 223 KB/s], Decompressed: 3869
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 114 KB/s], Decompressed: 3882
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 372 KB/s], Decompressed: 3882
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 727 KB/s], Decompressed: 3886
Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 106 KB/s], Decompressed: 3978
Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 369 KB/s], Decompressed: 3978
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 169 KB/s], Decompressed: 3995
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 45 KB/s], Decompressed: 3995
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 2087 KB/s], Decompressed: 4081
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 707 KB/s], Decompressed: 4081
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 338 KB/s], Decompressed: 4262
Downloaded: 4322 file(s) [attempted 4322/8459 = 51%, 360 KB/s], Decompressed: 4314
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 579 KB/s], Decompressed: 4355
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 217 KB/s], Decompressed: 4368
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 286 KB/s], Decompressed: 4368
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 189 KB/s], Decompressed: 4375
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 25 KB/s], Decompressed: 4481
Downloaded: 4557 file(s) [attempted 4557/8459 = 53%, 289 KB/s], Decompressed: 4481
Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 558 KB/s], Decompressed: 4591
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 545 KB/s], Decompressed: 4615
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 141 KB/s], Decompressed: 4615
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 192 KB/s], Decompressed: 4704
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 769 KB/s], Decompressed: 4755
Downloaded: 4805 file(s) [attempted 4805/8459 = 56%, 397 KB/s], Decompressed: 4779
Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 233 KB/s], Decompressed: 4779
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 271 KB/s], Decompressed: 4786
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 269 KB/s], Decompressed: 4902
Downloaded: 4960 file(s) [attempted 4960/8459 = 58%, 481 KB/s], Decompressed: 4902
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 186 KB/s], Decompressed: 4906
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 418 KB/s], Decompressed: 4906
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 108 KB/s], Decompressed: 4906
Downloaded: 5122 file(s) [attempted 5122/8459 = 60%, 88 KB/s], Decompressed: 5118
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 46 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 26 KB/s], Decompressed: 5159
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 46 KB/s], Decompressed: 5166
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 719 KB/s], Decompressed: 5166
Downloaded: 5321 file(s) [attempted 5321/8459 = 62%, 1124 KB/s], Decompressed: 5224
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 747 KB/s], Decompressed: 5354
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 260 KB/s], Decompressed: 5395
Downloaded: 5441 file(s) [attempted 5441/8459 = 64%, 536 KB/s], Decompressed: 5436
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 67 KB/s], Decompressed: 5477
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 189 KB/s], Decompressed: 5518
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5542
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 188 KB/s], Decompressed: 5542
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 1156 KB/s], Decompressed: 5631
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 450 KB/s], Decompressed: 5686
Downloaded: 5729 file(s) [attempted 5729/8459 = 67%, 683 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 295 KB/s], Decompressed: 5761
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 428 KB/s], Decompressed: 5806
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 989 KB/s], Decompressed: 5843
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 316 KB/s], Decompressed: 5885
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 140 KB/s], Decompressed: 5885
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 93 KB/s], Decompressed: 5888
Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 1085 KB/s], Decompressed: 5888
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 2217 KB/s], Decompressed: 5888
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 41 KB/s], Decompressed: 6083
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 115 KB/s], Decompressed: 6083
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 291 KB/s], Decompressed: 6090
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 309 KB/s], Decompressed: 6090
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 88 KB/s], Decompressed: 6090
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 810 KB/s], Decompressed: 6288
Downloaded: 6338 file(s) [attempted 6338/8459 = 74%, 351 KB/s], Decompressed: 6329
Downloaded: 6370 file(s) [attempted 6370/8459 = 75%, 528 KB/s], Decompressed: 6367
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 87 KB/s], Decompressed: 6408
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 126 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 720 KB/s], Decompressed: 6490
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 426 KB/s], Decompressed: 6521
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 365 KB/s], Decompressed: 6521
Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 600 KB/s], Decompressed: 6524
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 132 KB/s], Decompressed: 6524
Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 146 KB/s], Decompressed: 6610
Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 73 KB/s], Decompressed: 6610
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 574 KB/s], Decompressed: 6696
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 44 KB/s], Decompressed: 6696
Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 143 KB/s], Decompressed: 6696
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 939 KB/s], Decompressed: 6880
Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 74 KB/s], Decompressed: 6904
Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 105 KB/s], Decompressed: 6904
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 461 KB/s], Decompressed: 6911
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 150 KB/s], Decompressed: 6911
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 358 KB/s], Decompressed: 7017
Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 1420 KB/s], Decompressed: 7017
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 66 KB/s], Decompressed: 7017
Downloaded: 7229 file(s) [attempted 7229/8459 = 85%, 425 KB/s], Decompressed: 7206
Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 79 KB/s], Decompressed: 7267
Downloaded: 7314 file(s) [attempted 7314/8459 = 86%, 192 KB/s], Decompressed: 7308
Downloaded: 7350 file(s) [attempted 7350/8459 = 86%, 107 KB/s], Decompressed: 7346
Downloaded: 7390 file(s) [attempted 7390/8459 = 87%, 178 KB/s], Decompressed: 7387
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 569 KB/s], Decompressed: 7421
Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 308 KB/s], Decompressed: 7421
Downloaded: 7514 file(s) [attempted 7514/8459 = 88%, 850 KB/s], Decompressed: 7421
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 344 KB/s], Decompressed: 7548
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 95 KB/s], Decompressed: 7585
Downloaded: 7633 file(s) [attempted 7633/8459 = 90%, 163 KB/s], Decompressed: 7630
Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 646 KB/s], Decompressed: 7674
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 44 KB/s], Decompressed: 7715
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 302 KB/s], Decompressed: 7750
Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 162 KB/s], Decompressed: 7787
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1131 KB/s], Decompressed: 7787
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 96 KB/s], Decompressed: 7794
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 35 KB/s], Decompressed: 7794
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 179 KB/s], Decompressed: 7794
Downloaded: 8001 file(s) [attempted 8001/8459 = 94%, 211 KB/s], Decompressed: 7993
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 443 KB/s], Decompressed: 8037
Downloaded: 8088 file(s) [attempted 8088/8459 = 95%, 177 KB/s], Decompressed: 8061
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 112 KB/s], Decompressed: 8061
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 438 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8208
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 492 KB/s], Decompressed: 8253
Downloaded: 8295 file(s) [attempted 8295/8459 = 98%, 419 KB/s], Decompressed: 8290
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 211 KB/s], Decompressed: 8331
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 562 KB/s], Decompressed: 8369
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 715 KB/s], Decompressed: 8369
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8373
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8373

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (95s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (81s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.3s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (111s)
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 (74s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
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 (11s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (26s)
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 (276s)
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

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`