Run 1073

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

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

git checkout 81f0b9cbdedf11f5e134cc318400fcc087c1a8e5

Note: switching to '81f0b9cbdedf11f5e134cc318400fcc087c1a8e5'.

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 81f0b9c Thread Theorem 110 packet data

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%, 16 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 2 KB/s], Decompressed: 12
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 27 KB/s], Decompressed: 34
Downloaded: 62 file(s) [attempted 62/8459 = 0%, 38 KB/s], Decompressed: 58
Downloaded: 84 file(s) [attempted 84/8459 = 0%, 152 KB/s], Decompressed: 79
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 268 KB/s], Decompressed: 110
Downloaded: 152 file(s) [attempted 152/8459 = 1%, 382 KB/s], Decompressed: 145
Downloaded: 179 file(s) [attempted 179/8459 = 2%, 371 KB/s], Decompressed: 175
Downloaded: 210 file(s) [attempted 210/8459 = 2%, 202 KB/s], Decompressed: 203
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 32 KB/s], Decompressed: 240
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 75 KB/s], Decompressed: 278
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 108 KB/s], Decompressed: 316
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 30 KB/s], Decompressed: 353
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 314 KB/s], Decompressed: 388
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 116 KB/s], Decompressed: 422
Downloaded: 467 file(s) [attempted 467/8459 = 5%, 751 KB/s], Decompressed: 460
Downloaded: 505 file(s) [attempted 505/8459 = 5%, 233 KB/s], Decompressed: 501
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 28 KB/s], Decompressed: 542
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 46 KB/s], Decompressed: 576
Downloaded: 626 file(s) [attempted 626/8459 = 7%, 42 KB/s], Decompressed: 614
Downloaded: 658 file(s) [attempted 658/8459 = 7%, 50 KB/s], Decompressed: 651
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 329 KB/s], Decompressed: 696
Downloaded: 742 file(s) [attempted 742/8459 = 8%, 176 KB/s], Decompressed: 737
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 347 KB/s], Decompressed: 778
Downloaded: 812 file(s) [attempted 812/8459 = 9%, 211 KB/s], Decompressed: 809
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 163 KB/s], Decompressed: 854
Downloaded: 902 file(s) [attempted 902/8459 = 10%, 551 KB/s], Decompressed: 898
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 467 KB/s], Decompressed: 943
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 890 KB/s], Decompressed: 973
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 191 KB/s], Decompressed: 1008
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 330 KB/s], Decompressed: 1052
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 1983 KB/s], Decompressed: 1094
Downloaded: 1146 file(s) [attempted 1146/8459 = 13%, 159 KB/s], Decompressed: 1134
Downloaded: 1176 file(s) [attempted 1176/8459 = 13%, 89 KB/s], Decompressed: 1169
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 1744 KB/s], Decompressed: 1213
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 267 KB/s], Decompressed: 1251
Downloaded: 1297 file(s) [attempted 1297/8459 = 15%, 26 KB/s], Decompressed: 1292
Downloaded: 1335 file(s) [attempted 1335/8459 = 15%, 1225 KB/s], Decompressed: 1329
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 1148 KB/s], Decompressed: 1364
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 388 KB/s], Decompressed: 1401
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 264 KB/s], Decompressed: 1446
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 250 KB/s], Decompressed: 1483
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 1168 KB/s], Decompressed: 1524
Downloaded: 1571 file(s) [attempted 1571/8459 = 18%, 209 KB/s], Decompressed: 1562
Downloaded: 1604 file(s) [attempted 1604/8459 = 18%, 421 KB/s], Decompressed: 1600
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 329 KB/s], Decompressed: 1644
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 35 KB/s], Decompressed: 1685
Downloaded: 1732 file(s) [attempted 1732/8459 = 20%, 83 KB/s], Decompressed: 1726
Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 152 KB/s], Decompressed: 1764
Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 191 KB/s], Decompressed: 1798
Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 88 KB/s], Decompressed: 1843
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 407 KB/s], Decompressed: 1884
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 101 KB/s], Decompressed: 1925
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 254 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 77 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 114 KB/s], Decompressed: 2045
Downloaded: 2090 file(s) [attempted 2090/8459 = 24%, 74 KB/s], Decompressed: 2086
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 99 KB/s], Decompressed: 2123
Downloaded: 2163 file(s) [attempted 2163/8459 = 25%, 234 KB/s], Decompressed: 2154
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 87 KB/s], Decompressed: 2199
Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 187 KB/s], Decompressed: 2240
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 131 KB/s], Decompressed: 2284
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 158 KB/s], Decompressed: 2325
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 333 KB/s], Decompressed: 2360
Downloaded: 2402 file(s) [attempted 2402/8459 = 28%, 282 KB/s], Decompressed: 2397
Downloaded: 2442 file(s) [attempted 2442/8459 = 28%, 242 KB/s], Decompressed: 2438
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 283 KB/s], Decompressed: 2472
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 265 KB/s], Decompressed: 2510
Downloaded: 2552 file(s) [attempted 2552/8459 = 30%, 84 KB/s], Decompressed: 2548
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 359 KB/s], Decompressed: 2585
Downloaded: 2633 file(s) [attempted 2633/8459 = 31%, 1204 KB/s], Decompressed: 2630
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 170 KB/s], Decompressed: 2671
Downloaded: 2714 file(s) [attempted 2714/8459 = 32%, 72 KB/s], Decompressed: 2702
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 43 KB/s], Decompressed: 2739
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 418 KB/s], Decompressed: 2784
Downloaded: 2831 file(s) [attempted 2831/8459 = 33%, 211 KB/s], Decompressed: 2822
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 218 KB/s], Decompressed: 2866
Downloaded: 2908 file(s) [attempted 2908/8459 = 34%, 386 KB/s], Decompressed: 2900
Downloaded: 2945 file(s) [attempted 2945/8459 = 34%, 123 KB/s], Decompressed: 2941
Downloaded: 2986 file(s) [attempted 2986/8459 = 35%, 23 KB/s], Decompressed: 2979
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 22 KB/s], Decompressed: 3020
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 100 KB/s], Decompressed: 3054
Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 464 KB/s], Decompressed: 3099
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 142 KB/s], Decompressed: 3143
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 242 KB/s], Decompressed: 3188
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 397 KB/s], Decompressed: 3225
Downloaded: 3263 file(s) [attempted 3263/8459 = 38%, 180 KB/s], Decompressed: 3260
Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 273 KB/s], Decompressed: 3297
Downloaded: 3346 file(s) [attempted 3346/8459 = 39%, 446 KB/s], Decompressed: 3342
Downloaded: 3388 file(s) [attempted 3388/8459 = 40%, 1297 KB/s], Decompressed: 3379
Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 711 KB/s], Decompressed: 3420
Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 228 KB/s], Decompressed: 3458
Downloaded: 3504 file(s) [attempted 3504/8459 = 41%, 161 KB/s], Decompressed: 3499
Downloaded: 3540 file(s) [attempted 3540/8459 = 41%, 1286 KB/s], Decompressed: 3533
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 120 KB/s], Decompressed: 3574
Downloaded: 3617 file(s) [attempted 3617/8459 = 42%, 722 KB/s], Decompressed: 3612
Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 316 KB/s], Decompressed: 3653
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 1116 KB/s], Decompressed: 3694
Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 187 KB/s], Decompressed: 3735
Downloaded: 3780 file(s) [attempted 3780/8459 = 44%, 203 KB/s], Decompressed: 3776
Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 165 KB/s], Decompressed: 3811
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 457 KB/s], Decompressed: 3848
Downloaded: 3896 file(s) [attempted 3896/8459 = 46%, 418 KB/s], Decompressed: 3893
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 95 KB/s], Decompressed: 3934
Downloaded: 3982 file(s) [attempted 3982/8459 = 47%, 672 KB/s], Decompressed: 3975
Downloaded: 4015 file(s) [attempted 4015/8459 = 47%, 1804 KB/s], Decompressed: 4009
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 624 KB/s], Decompressed: 4043
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 222 KB/s], Decompressed: 4084
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 588 KB/s], Decompressed: 4129
Downloaded: 4175 file(s) [attempted 4175/8459 = 49%, 231 KB/s], Decompressed: 4167
Downloaded: 4211 file(s) [attempted 4211/8459 = 49%, 94 KB/s], Decompressed: 4201
Downloaded: 4246 file(s) [attempted 4246/8459 = 50%, 91 KB/s], Decompressed: 4238
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 1002 KB/s], Decompressed: 4279
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 175 KB/s], Decompressed: 4324
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 70 KB/s], Decompressed: 4368
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 103 KB/s], Decompressed: 4410
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 414 KB/s], Decompressed: 4444
Downloaded: 4489 file(s) [attempted 4489/8459 = 53%, 89 KB/s], Decompressed: 4485
Downloaded: 4531 file(s) [attempted 4531/8459 = 53%, 445 KB/s], Decompressed: 4526
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 60 KB/s], Decompressed: 4560
Downloaded: 4605 file(s) [attempted 4605/8459 = 54%, 44 KB/s], Decompressed: 4602
Downloaded: 4643 file(s) [attempted 4643/8459 = 54%, 96 KB/s], Decompressed: 4639
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 1021 KB/s], Decompressed: 4680
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 699 KB/s], Decompressed: 4721
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 184 KB/s], Decompressed: 4755
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 113 KB/s], Decompressed: 4796
Downloaded: 4840 file(s) [attempted 4840/8459 = 57%, 1687 KB/s], Decompressed: 4830
Downloaded: 4881 file(s) [attempted 4881/8459 = 57%, 139 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 213 KB/s], Decompressed: 4909
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 1328 KB/s], Decompressed: 4943
Downloaded: 4993 file(s) [attempted 4993/8459 = 59%, 1036 KB/s], Decompressed: 4985
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 61 KB/s], Decompressed: 5029
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 312 KB/s], Decompressed: 5073
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 212 KB/s], Decompressed: 5108
Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 124 KB/s], Decompressed: 5150
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 83 KB/s], Decompressed: 5193
Downloaded: 5231 file(s) [attempted 5231/8459 = 61%, 245 KB/s], Decompressed: 5221
Downloaded: 5266 file(s) [attempted 5266/8459 = 62%, 43 KB/s], Decompressed: 5262
Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 78 KB/s], Decompressed: 5303
Downloaded: 5347 file(s) [attempted 5347/8459 = 63%, 90 KB/s], Decompressed: 5344
Downloaded: 5389 file(s) [attempted 5389/8459 = 63%, 766 KB/s], Decompressed: 5382
Downloaded: 5428 file(s) [attempted 5428/8459 = 64%, 283 KB/s], Decompressed: 5419
Downloaded: 5464 file(s) [attempted 5464/8459 = 64%, 67 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 295 KB/s], Decompressed: 5494
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 189 KB/s], Decompressed: 5536
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 435 KB/s], Decompressed: 5580
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 508 KB/s], Decompressed: 5614
Downloaded: 5666 file(s) [attempted 5666/8459 = 66%, 227 KB/s], Decompressed: 5662
Downloaded: 5704 file(s) [attempted 5704/8459 = 67%, 775 KB/s], Decompressed: 5696
Downloaded: 5738 file(s) [attempted 5738/8459 = 67%, 579 KB/s], Decompressed: 5734
Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 398 KB/s], Decompressed: 5775
Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 171 KB/s], Decompressed: 5816
Downloaded: 5861 file(s) [attempted 5861/8459 = 69%, 433 KB/s], Decompressed: 5854
Downloaded: 5893 file(s) [attempted 5893/8459 = 69%, 329 KB/s], Decompressed: 5888
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 906 KB/s], Decompressed: 5933
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 258 KB/s], Decompressed: 5970
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 99 KB/s], Decompressed: 6011
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 172 KB/s], Decompressed: 6052
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 56 KB/s], Decompressed: 6090
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 985 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 127 KB/s], Decompressed: 6175
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 89 KB/s], Decompressed: 6206
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 36 KB/s], Decompressed: 6251
Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 26 KB/s], Decompressed: 6292
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 203 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 359 KB/s], Decompressed: 6377
Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 517 KB/s], Decompressed: 6415
Downloaded: 6458 file(s) [attempted 6458/8459 = 76%, 174 KB/s], Decompressed: 6453
Downloaded: 6501 file(s) [attempted 6501/8459 = 76%, 429 KB/s], Decompressed: 6497
Downloaded: 6542 file(s) [attempted 6542/8459 = 77%, 354 KB/s], Decompressed: 6531
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 470 KB/s], Decompressed: 6562
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 608 KB/s], Decompressed: 6603
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 481 KB/s], Decompressed: 6648
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 113 KB/s], Decompressed: 6692
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 432 KB/s], Decompressed: 6730
Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 117 KB/s], Decompressed: 6764
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 866 KB/s], Decompressed: 6809
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 113 KB/s], Decompressed: 6846
Downloaded: 6882 file(s) [attempted 6882/8459 = 81%, 1932 KB/s], Decompressed: 6874
Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 97 KB/s], Decompressed: 6915
Downloaded: 6958 file(s) [attempted 6958/8459 = 82%, 177 KB/s], Decompressed: 6952
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 446 KB/s], Decompressed: 6997
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 23 KB/s], Decompressed: 7037
Downloaded: 7080 file(s) [attempted 7080/8459 = 83%, 43 KB/s], Decompressed: 7076
Downloaded: 7113 file(s) [attempted 7113/8459 = 84%, 353 KB/s], Decompressed: 7110
Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 232 KB/s], Decompressed: 7154
Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 191 KB/s], Decompressed: 7192
Downloaded: 7237 file(s) [attempted 7237/8459 = 85%, 1125 KB/s], Decompressed: 7233
Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 224 KB/s], Decompressed: 7267
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 1871 KB/s], Decompressed: 7305
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 994 KB/s], Decompressed: 7343
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 256 KB/s], Decompressed: 7392
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 108 KB/s], Decompressed: 7435
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 110 KB/s], Decompressed: 7469
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 198 KB/s], Decompressed: 7506
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 566 KB/s], Decompressed: 7541
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 81 KB/s], Decompressed: 7582
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 202 KB/s], Decompressed: 7623
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 596 KB/s], Decompressed: 7661
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 185 KB/s], Decompressed: 7698
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 287 KB/s], Decompressed: 7743
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 125 KB/s], Decompressed: 7784
Downloaded: 7828 file(s) [attempted 7828/8459 = 92%, 423 KB/s], Decompressed: 7818
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 64 KB/s], Decompressed: 7859
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 115 KB/s], Decompressed: 7897
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 87 KB/s], Decompressed: 7938
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 293 KB/s], Decompressed: 7979
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 156 KB/s], Decompressed: 8020
Downloaded: 8062 file(s) [attempted 8062/8459 = 95%, 118 KB/s], Decompressed: 8054
Downloaded: 8094 file(s) [attempted 8094/8459 = 95%, 492 KB/s], Decompressed: 8085
Downloaded: 8136 file(s) [attempted 8136/8459 = 96%, 314 KB/s], Decompressed: 8133
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 1069 KB/s], Decompressed: 8171
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 806 KB/s], Decompressed: 8212
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 48 KB/s], Decompressed: 8253
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 265 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 79 KB/s], Decompressed: 8328
Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 572 KB/s], Decompressed: 8366
Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 33 KB/s], Decompressed: 8403
Downloaded: 8450 file(s) [attempted 8450/8459 = 99%, 81 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 81 KB/s], Decompressed: 8451

lake build

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

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

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

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

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

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

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

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (31s)
⚠ [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 (5.5s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.5s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.7s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (25s)
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 (154s)
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`