Run 1207

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

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

git checkout 5c48653111f44f835827f76e22f4eaf9cf9c1b8f

Note: switching to '5c48653111f44f835827f76e22f4eaf9cf9c1b8f'.

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 5c48653 Complete connected finite-etale basepoint converse

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)

✔ [8/25] Built Cache.Lean (413ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.6s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (99ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (163ms)
✔ [13/25] Built Cache.Lean:c.o (129ms)
✔ [15/25] Built Cache.Init (330ms)
✔ [16/25] Built Cache.IO (1.9s)
✔ [17/25] Built Cache.Init:c.o (74ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (879ms)
✔ [20/25] Built Cache.Hashing:c.o (336ms)
✔ [21/25] Built Cache.Requests (1.0s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (969ms)
✔ [24/25] Built Cache.Main:c.o (530ms)
✔ [25/25] Built cache:exe (5.8s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 15 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 4 KB/s], Decompressed: 6
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 15 KB/s], Decompressed: 20
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 357 KB/s], Decompressed: 27
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 183 KB/s], Decompressed: 39
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 45 KB/s], Decompressed: 62
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 370 KB/s], Decompressed: 117
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 148 KB/s], Decompressed: 141
Downloaded: 209 file(s) [attempted 209/8459 = 2%, 47 KB/s], Decompressed: 165
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 293 KB/s], Decompressed: 165
Downloaded: 281 file(s) [attempted 281/8459 = 3%, 608 KB/s], Decompressed: 202
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 196 KB/s], Decompressed: 250
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 250
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 125 KB/s], Decompressed: 305
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 538 KB/s], Decompressed: 357
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 761 KB/s], Decompressed: 398
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 655 KB/s], Decompressed: 439
Downloaded: 548 file(s) [attempted 548/8459 = 6%, 297 KB/s], Decompressed: 480
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 792 KB/s], Decompressed: 518
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 157 KB/s], Decompressed: 559
Downloaded: 668 file(s) [attempted 668/8459 = 7%, 671 KB/s], Decompressed: 603
Downloaded: 709 file(s) [attempted 709/8459 = 8%, 1152 KB/s], Decompressed: 651
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 219 KB/s], Decompressed: 689
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 344 KB/s], Decompressed: 733
Downloaded: 833 file(s) [attempted 833/8459 = 9%, 345 KB/s], Decompressed: 733
Downloaded: 874 file(s) [attempted 874/8459 = 10%, 155 KB/s], Decompressed: 785
Downloaded: 918 file(s) [attempted 918/8459 = 10%, 395 KB/s], Decompressed: 836
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 225 KB/s], Decompressed: 894
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 25 KB/s], Decompressed: 949
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 885 KB/s], Decompressed: 997
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 440 KB/s], Decompressed: 997
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 469 KB/s], Decompressed: 1045
Downloaded: 1168 file(s) [attempted 1168/8459 = 13%, 230 KB/s], Decompressed: 1093
Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 497 KB/s], Decompressed: 1148
Downloaded: 1250 file(s) [attempted 1250/8459 = 14%, 592 KB/s], Decompressed: 1203
Downloaded: 1291 file(s) [attempted 1291/8459 = 15%, 856 KB/s], Decompressed: 1247
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 88 KB/s], Decompressed: 1291
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 347 KB/s], Decompressed: 1329
Downloaded: 1411 file(s) [attempted 1411/8459 = 16%, 108 KB/s], Decompressed: 1370
Downloaded: 1452 file(s) [attempted 1452/8459 = 17%, 435 KB/s], Decompressed: 1370
Downloaded: 1493 file(s) [attempted 1493/8459 = 17%, 313 KB/s], Decompressed: 1411
Downloaded: 1534 file(s) [attempted 1534/8459 = 18%, 388 KB/s], Decompressed: 1466
Downloaded: 1579 file(s) [attempted 1579/8459 = 18%, 427 KB/s], Decompressed: 1466
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 336 KB/s], Decompressed: 1534
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 131 KB/s], Decompressed: 1534
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 61 KB/s], Decompressed: 1603
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 89 KB/s], Decompressed: 1603
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 26 KB/s], Decompressed: 1682
Downloaded: 1825 file(s) [attempted 1825/8459 = 21%, 211 KB/s], Decompressed: 1682
Downloaded: 1866 file(s) [attempted 1866/8459 = 22%, 1455 KB/s], Decompressed: 1682
Downloaded: 1907 file(s) [attempted 1907/8459 = 22%, 41 KB/s], Decompressed: 1682
Downloaded: 1945 file(s) [attempted 1945/8459 = 22%, 24 KB/s], Decompressed: 1760
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 121 KB/s], Decompressed: 1760
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 121 KB/s], Decompressed: 1760
Downloaded: 2062 file(s) [attempted 2062/8459 = 24%, 404 KB/s], Decompressed: 1921
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 52 KB/s], Decompressed: 1921
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 337 KB/s], Decompressed: 1921
Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 33 KB/s], Decompressed: 2062
Downloaded: 2222 file(s) [attempted 2222/8459 = 26%, 41 KB/s], Decompressed: 2062
Downloaded: 2263 file(s) [attempted 2263/8459 = 26%, 351 KB/s], Decompressed: 2062
Downloaded: 2304 file(s) [attempted 2304/8459 = 27%, 1404 KB/s], Decompressed: 2185
Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 424 KB/s], Decompressed: 2185
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 272 KB/s], Decompressed: 2287
Downloaded: 2424 file(s) [attempted 2424/8459 = 28%, 144 KB/s], Decompressed: 2287
Downloaded: 2465 file(s) [attempted 2465/8459 = 29%, 56 KB/s], Decompressed: 2380
Downloaded: 2506 file(s) [attempted 2506/8459 = 29%, 149 KB/s], Decompressed: 2380
Downloaded: 2547 file(s) [attempted 2547/8459 = 30%, 438 KB/s], Decompressed: 2465
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 232 KB/s], Decompressed: 2534
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 149 KB/s], Decompressed: 2534
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 421 KB/s], Decompressed: 2585
Downloaded: 2708 file(s) [attempted 2708/8459 = 32%, 248 KB/s], Decompressed: 2636
Downloaded: 2749 file(s) [attempted 2749/8459 = 32%, 610 KB/s], Decompressed: 2636
Downloaded: 2790 file(s) [attempted 2790/8459 = 32%, 1840 KB/s], Decompressed: 2698
Downloaded: 2832 file(s) [attempted 2832/8459 = 33%, 71 KB/s], Decompressed: 2760
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 1000 KB/s], Decompressed: 2760
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 672 KB/s], Decompressed: 2825
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 2342 KB/s], Decompressed: 2883
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 184 KB/s], Decompressed: 2934
Downloaded: 3033 file(s) [attempted 3033/8459 = 35%, 110 KB/s], Decompressed: 2982
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 515 KB/s], Decompressed: 2982
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 191 KB/s], Decompressed: 3030
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 225 KB/s], Decompressed: 3085
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 215 KB/s], Decompressed: 3085
Downloaded: 3234 file(s) [attempted 3234/8459 = 38%, 150 KB/s], Decompressed: 3150
Downloaded: 3276 file(s) [attempted 3276/8459 = 38%, 966 KB/s], Decompressed: 3218
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 860 KB/s], Decompressed: 3218
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 369 KB/s], Decompressed: 3273
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 1122 KB/s], Decompressed: 3324
Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 112 KB/s], Decompressed: 3372
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 366 KB/s], Decompressed: 3420
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 123 KB/s], Decompressed: 3468
Downloaded: 3560 file(s) [attempted 3560/8459 = 42%, 212 KB/s], Decompressed: 3509
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 36 KB/s], Decompressed: 3557
Downloaded: 3643 file(s) [attempted 3643/8459 = 43%, 106 KB/s], Decompressed: 3595
Downloaded: 3680 file(s) [attempted 3680/8459 = 43%, 255 KB/s], Decompressed: 3626
Downloaded: 3721 file(s) [attempted 3721/8459 = 43%, 298 KB/s], Decompressed: 3663
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 1092 KB/s], Decompressed: 3704
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 416 KB/s], Decompressed: 3738
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 929 KB/s], Decompressed: 3738
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 144 KB/s], Decompressed: 3773
Downloaded: 3923 file(s) [attempted 3923/8459 = 46%, 331 KB/s], Decompressed: 3773
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 102 KB/s], Decompressed: 3869
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 308 KB/s], Decompressed: 3869
Downloaded: 4053 file(s) [attempted 4053/8459 = 47%, 131 KB/s], Decompressed: 3964
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 52 KB/s], Decompressed: 3964
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 611 KB/s], Decompressed: 4046
Downloaded: 4170 file(s) [attempted 4170/8459 = 49%, 232 KB/s], Decompressed: 4046
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 94 KB/s], Decompressed: 4125
Downloaded: 4255 file(s) [attempted 4255/8459 = 50%, 883 KB/s], Decompressed: 4125
Downloaded: 4289 file(s) [attempted 4289/8459 = 50%, 54 KB/s], Decompressed: 4207
Downloaded: 4331 file(s) [attempted 4331/8459 = 51%, 184 KB/s], Decompressed: 4207
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 624 KB/s], Decompressed: 4283
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 103 KB/s], Decompressed: 4283
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 451 KB/s], Decompressed: 4358
Downloaded: 4508 file(s) [attempted 4508/8459 = 53%, 192 KB/s], Decompressed: 4426
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 141 KB/s], Decompressed: 4426
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 163 KB/s], Decompressed: 4502
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 242 KB/s], Decompressed: 4567
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 535 KB/s], Decompressed: 4567
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 25 KB/s], Decompressed: 4621
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 110 KB/s], Decompressed: 4676
Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 60 KB/s], Decompressed: 4728
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 77 KB/s], Decompressed: 4728
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 190 KB/s], Decompressed: 4786
Downloaded: 4905 file(s) [attempted 4905/8459 = 57%, 392 KB/s], Decompressed: 4786
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 51 KB/s], Decompressed: 4861
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 56 KB/s], Decompressed: 4861
Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 108 KB/s], Decompressed: 4936
Downloaded: 5066 file(s) [attempted 5066/8459 = 59%, 63 KB/s], Decompressed: 4936
Downloaded: 5107 file(s) [attempted 5107/8459 = 60%, 113 KB/s], Decompressed: 5008
Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 446 KB/s], Decompressed: 5008
Downloaded: 5193 file(s) [attempted 5193/8459 = 61%, 154 KB/s], Decompressed: 5080
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 887 KB/s], Decompressed: 5080
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 79 KB/s], Decompressed: 5162
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 1285 KB/s], Decompressed: 5162
Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 245 KB/s], Decompressed: 5255
Downloaded: 5398 file(s) [attempted 5398/8459 = 63%, 62 KB/s], Decompressed: 5255
Downloaded: 5439 file(s) [attempted 5439/8459 = 64%, 1125 KB/s], Decompressed: 5333
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 196 KB/s], Decompressed: 5405
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 538 KB/s], Decompressed: 5405
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 436 KB/s], Decompressed: 5470
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 787 KB/s], Decompressed: 5532
Downloaded: 5641 file(s) [attempted 5641/8459 = 66%, 29 KB/s], Decompressed: 5532
Downloaded: 5682 file(s) [attempted 5682/8459 = 67%, 261 KB/s], Decompressed: 5590
Downloaded: 5723 file(s) [attempted 5723/8459 = 67%, 214 KB/s], Decompressed: 5590
Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 106 KB/s], Decompressed: 5648
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 809 KB/s], Decompressed: 5648
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 1021 KB/s], Decompressed: 5758
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 492 KB/s], Decompressed: 5758
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 136 KB/s], Decompressed: 5850
Downloaded: 5973 file(s) [attempted 5973/8459 = 70%, 425 KB/s], Decompressed: 5850
Downloaded: 6014 file(s) [attempted 6014/8459 = 71%, 289 KB/s], Decompressed: 5929
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 326 KB/s], Decompressed: 5929
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1228 KB/s], Decompressed: 6001
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 143 KB/s], Decompressed: 6001
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 43 KB/s], Decompressed: 6001
Downloaded: 6209 file(s) [attempted 6209/8459 = 73%, 1225 KB/s], Decompressed: 6001
Downloaded: 6250 file(s) [attempted 6250/8459 = 73%, 87 KB/s], Decompressed: 6073
Downloaded: 6292 file(s) [attempted 6292/8459 = 74%, 64 KB/s], Decompressed: 6073
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 355 KB/s], Decompressed: 6073
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 497 KB/s], Decompressed: 6073
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 307 KB/s], Decompressed: 6237
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 1278 KB/s], Decompressed: 6237
Downloaded: 6500 file(s) [attempted 6500/8459 = 76%, 579 KB/s], Decompressed: 6237
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 617 KB/s], Decompressed: 6237
Downloaded: 6582 file(s) [attempted 6582/8459 = 77%, 464 KB/s], Decompressed: 6404
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 90 KB/s], Decompressed: 6404
Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 186 KB/s], Decompressed: 6404
Downloaded: 6702 file(s) [attempted 6702/8459 = 79%, 61 KB/s], Decompressed: 6555
Downloaded: 6743 file(s) [attempted 6743/8459 = 79%, 731 KB/s], Decompressed: 6555
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 534 KB/s], Decompressed: 6555
Downloaded: 6825 file(s) [attempted 6825/8459 = 80%, 957 KB/s], Decompressed: 6689
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 115 KB/s], Decompressed: 6689
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 439 KB/s], Decompressed: 6801
Downloaded: 6949 file(s) [attempted 6949/8459 = 82%, 201 KB/s], Decompressed: 6801
Downloaded: 6986 file(s) [attempted 6986/8459 = 82%, 2354 KB/s], Decompressed: 6897
Downloaded: 7027 file(s) [attempted 7027/8459 = 83%, 1078 KB/s], Decompressed: 6897
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 619 KB/s], Decompressed: 6976
Downloaded: 7109 file(s) [attempted 7109/8459 = 84%, 51 KB/s], Decompressed: 7044
Downloaded: 7151 file(s) [attempted 7151/8459 = 84%, 593 KB/s], Decompressed: 7044
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 68 KB/s], Decompressed: 7109
Downloaded: 7228 file(s) [attempted 7228/8459 = 85%, 156 KB/s], Decompressed: 7164
Downloaded: 7263 file(s) [attempted 7263/8459 = 85%, 607 KB/s], Decompressed: 7164
Downloaded: 7311 file(s) [attempted 7311/8459 = 86%, 182 KB/s], Decompressed: 7226
Downloaded: 7356 file(s) [attempted 7356/8459 = 86%, 42 KB/s], Decompressed: 7287
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 266 KB/s], Decompressed: 7342
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 115 KB/s], Decompressed: 7342
Downloaded: 7479 file(s) [attempted 7479/8459 = 88%, 330 KB/s], Decompressed: 7394
Downloaded: 7517 file(s) [attempted 7517/8459 = 88%, 297 KB/s], Decompressed: 7441
Downloaded: 7558 file(s) [attempted 7558/8459 = 89%, 228 KB/s], Decompressed: 7441
Downloaded: 7595 file(s) [attempted 7595/8459 = 89%, 305 KB/s], Decompressed: 7503
Downloaded: 7636 file(s) [attempted 7636/8459 = 90%, 149 KB/s], Decompressed: 7503
Downloaded: 7684 file(s) [attempted 7684/8459 = 90%, 47 KB/s], Decompressed: 7571
Downloaded: 7725 file(s) [attempted 7725/8459 = 91%, 34 KB/s], Decompressed: 7643
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 331 KB/s], Decompressed: 7643
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 616 KB/s], Decompressed: 7719
Downloaded: 7845 file(s) [attempted 7845/8459 = 92%, 221 KB/s], Decompressed: 7719
Downloaded: 7886 file(s) [attempted 7886/8459 = 93%, 848 KB/s], Decompressed: 7787
Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 324 KB/s], Decompressed: 7852
Downloaded: 7975 file(s) [attempted 7975/8459 = 94%, 870 KB/s], Decompressed: 7914
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 242 KB/s], Decompressed: 7914
Downloaded: 8064 file(s) [attempted 8064/8459 = 95%, 80 KB/s], Decompressed: 7975
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 345 KB/s], Decompressed: 8033
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 76 KB/s], Decompressed: 8033
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 116 KB/s], Decompressed: 8088
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 79 KB/s], Decompressed: 8143
Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 164 KB/s], Decompressed: 8191
Downloaded: 8309 file(s) [attempted 8309/8459 = 98%, 55 KB/s], Decompressed: 8246
Downloaded: 8348 file(s) [attempted 8348/8459 = 98%, 199 KB/s], Decompressed: 8246
Downloaded: 8389 file(s) [attempted 8389/8459 = 99%, 52 KB/s], Decompressed: 8307
Downloaded: 8430 file(s) [attempted 8430/8459 = 99%, 1272 KB/s], Decompressed: 8372
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 156 KB/s], Decompressed: 8372
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 156 KB/s], Decompressed: 8372

apx-runtime-resource-v1	apx-verifier-job-1526-runtime-lake_cache-606529-1785499096802121265-0	921600	1429504	21474836480	0	0	0	0	0	0	8688357376	9019949056	21474836480	0	0	0	0	0	0

lake build

✔ [1/140] Built Iut.Foundations.Species (443ms)
✔ [753/760] Built Iut.Foundations.RealLineCopy (1.7s)
✔ [754/760] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [755/760] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [756/760] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [757/760] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [758/760] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [759/801] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3505/3510] Built Iut.Foundations.EtaleThetaQuotient (18s)
✔ [3506/3524] Built Iut.Foundations.Orbicurve (4.1s)
✔ [3953/3966] Built Iut.Foundations.InitialThetaData (20s)
✔ [3962/3973] Built Iut.Foundations.OrbicurvePullback (3.8s)
✔ [3965/3973] Built Iut.Foundations.SourceSemiGraph (2.1s)
✔ [3966/3974] Built Iut.Foundations.EtaleThetaCovers (4.2s)
✔ [3968/3974] Built Iut.Foundations.SourceSemiGraphAction (2.5s)
✔ [3969/3974] Built Iut.Foundations.SourceInitialThetaData (36s)
✔ [3971/3974] Built Iut.Foundations.SourceSemiGraphOfSubgroups (2.4s)
✔ [3972/3974] Built Iut.Foundations.SourceProfiniteCosetSystem (2.0s)
✔ [3973/3995] Built Iut.Foundations.SourceProfiniteSemiGraphSystem (73s)
✔ [4007/4012] Built Iut.Foundations.KummerFaithfulness (1.0s)
✔ [4008/4013] Built Iut.Foundations.SourceTemperedSemigraph (4.8s)
✔ [4010/4013] Built Iut.Foundations.SourceMonoThetaEnvironment (7.8s)
✔ [4012/4023] Built Iut.Foundations.ContinuousH1 (6.6s)
✔ [4020/4027] Built Iut.Foundations.Procession (2.6s)
✔ [4023/4027] Built Iut.Foundations.SourceMLFKummerFaithfulness (2.9s)
✔ [4024/4027] Built Iut.Foundations.Frobenioid (5.7s)
✔ [4025/4027] Built Iut.Foundations.SourceThetaHodgeTheater (18s)
✔ [4026/4057] Built Iut.Foundations.SourceProcession (6.4s)
✔ [4038/4057] Built Iut.Foundations.SourceModelFrobenioid (5.4s)
✔ [4045/4065] Built Iut.Foundations.SourceAnabelioid (4.0s)
⚠ [4050/4066] Built Iut.Foundations.SourceThetaEvaluation (61s)
warning: Iut/Foundations/SourceThetaEvaluation.lean:1780:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.algebraicClosure_isFractionRing`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1827:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.groupificationToAlgebraicClosureUnits_of`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1906:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.groupificationToAlgebraicClosureUnits_injective`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1973:10: Try `simp at underlying` instead of `simpa using underlying`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1980:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:1985:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:2344:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.unitToAlgebraicClosureUnit_injective`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:2357:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFIntegralMonoid.unitToAlgebraicClosureUnit_torsionUnit`:
  [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
  [CharZero K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:3826:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:5486:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFGaloisTMPair.KummerRootTheory.chosen_rootSystem`:
  [IsMulCommutative A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [IsMulCommutative A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Foundations/SourceThetaEvaluation.lean:5732:0: automatically included section variable(s) unused in theorem `Iut.SourceMLFGaloisTMPair.LocalKummerRootTheory.chosen_rootSystem`:
  [IsMulCommutative A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [IsMulCommutative A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [4053/4075] Built Iut.Foundations.SourceTopologicalActionPairCategory (3.2s)
✔ [4054/4075] Built Iut.Foundations.SourceConjugateSynchronization (3.9s)
✔ [4055/4075] Built Iut.Foundations.SourceThetaSplitting (6.3s)
✔ [4056/4075] Built Iut.Foundations.SourceSplitKummerFrobenioid (7.5s)
✔ [4060/4075] Built Iut.Foundations.SourceAnabelioidEquivalence (2.8s)
✔ [4061/4075] Built Iut.Foundations.SourceSemiGraphOfAnabelioids (3.1s)
✔ [4062/4075] Built Iut.Foundations.SourceAutHolomorphic (2.6s)
✔ [4063/4075] Built Iut.Foundations.SourceHodgeArakelovEvaluation (3.8s)
✔ [4064/4075] Built Iut.Foundations.SourceArchimedeanKummerSystem (5.8s)
✔ [4066/4075] Built Iut.Foundations.SourceTimesMuPrimeStrip (9.5s)
✔ [4067/4075] Built Iut.Foundations.SourceContinuousAnabelioid (4.7s)
✔ [4068/4075] Built Iut.Foundations.SourceTimesMuPrimeStripIsomorphism (15s)
✔ [4069/4078] Built Iut.Foundations.SourceAnabelioidSlice (18s)
✔ [4070/4081] Built Iut.Foundations.SourceTimesMuPrimeStripFullPolyIsomorphism (8.0s)
✔ [4071/4081] Built Iut.Foundations.SourceAnabelioidComponents (7.8s)
✔ [4073/4081] Built Iut.Foundations.SourceTimesMuReconstructionAlgorithm (7.8s)
✔ [4074/4085] Built Iut.Foundations.SourceConnectedAnabelioidSlice (3.9s)
✔ [4076/4095] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.6s)
✔ [4087/4095] Built Iut.Foundations.SourceFThetaBridge (3.8s)
✔ [4088/4095] Built Iut.Foundations.SourceTopologicalPseudoMonoid (4.6s)
✔ [4089/4096] Built Iut.Foundations.SourceArchimedeanSemiGerm (2.8s)
✔ [4095/4182] Built Iut.Foundations.SourceAutHolomorphicRigidity (2.6s)
✔ [4143/4182] Built Iut.Foundations.ThetaHodgeTheater (6.9s)
✔ [4144/4182] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [4145/4182] Built Iut.SourceTrace.M1M3PaperLedger (8.8s)
✔ [4147/4182] Built Iut.Stage1.PilotComparison (1.5s)
✔ [4149/4183] Built Iut.Stage1.IUTStage1HodgeTheaterSource (3.2s)
✔ [4150/4183] Built Iut.Foundations.AlgorithmicBridge (2.9s)
⚠ [4151/4183] Built Iut.Foundations.SourceTheorem311 (119s)
warning: Iut/Foundations/SourceTheorem311.lean:771:4: try 'simp' instead of 'simpa'

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:1021:43: unused variable `map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:3204:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:3223:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:3878:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:4956:7: unused variable `factor`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:4956:30: unused variable `place`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:5112:8: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  have : automorphism value ∈ automorphism '' (core.invariantLattice subgroup : Set M) := ⟨value, hvalue, rfl⟩
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: Iut/Foundations/SourceTheorem311.lean:5115:8: The following tactic starts with 2 goals and ends with 1 goal, 1 of which is not operated on.
  simpa only [hautomorphism.2 subgroup] using this
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: Iut/Foundations/SourceTheorem311.lean:5771:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:7547:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:7548:54: 'norm_num' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Iut/Foundations/SourceTheorem311.lean:7548:54: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Iut/Foundations/SourceTheorem311.lean:8148:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` 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/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8143:6: `rintro ⟨source, hsource, hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` 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/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8144:6: `exact ⟨source, hsource, by simpa using hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` 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/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8145:6: `rintro ⟨source, hsource, hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:8140:4: `simp [Set.mem_smul_set, nnrealPacketScale, packetScale,
      Equiv.mulLeft₀, mul_comm]` 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/Foundations/SourceTheorem311.lean:8140:4: Try this:
  [apply] simp only [mem_image, mem_image_equiv]
info: Iut/Foundations/SourceTheorem311.lean:8146:6: `exact ⟨source, hsource, by simpa using hvalue⟩` uses `⊢`!
warning: Iut/Foundations/SourceTheorem311.lean:12454:7: unused variable `map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12459:7: unused variable `map`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12901:12: unused variable `first`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12901:18: unused variable `second`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12904:12: unused variable `value`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12927:12: unused variable `first`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12927:18: unused variable `second`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:12931:12: unused variable `value`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Foundations/SourceTheorem311.lean:14042:8: `simp [stripMap, CategoryCapsule.FullMemberMorphism.id]` 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/Foundations/SourceTheorem311.lean:14042:8: Try this:
  [apply] simp only [Cat.of_α]
info: Iut/Foundations/SourceTheorem311.lean:14043:8: `exact Category.comp_id _` uses `⊢`!
✔ [4153/4183] Built Iut.Stage1.CorollarySchema (2.5s)
✔ [4154/4183] Built Iut.Foundations.SourceTheorem311Horizontal (10s)
✔ [4155/4183] Built Iut.Foundations.SourceVerticalLogLink (5.4s)
✔ [4156/4183] Built Iut.Foundations.SourceFiniteLocalMLFComparison (9.6s)
✔ [4157/4186] Built Iut.Stage1.SourceObligations (2.0s)
✔ [4159/4195] Built Iut.Foundations.SourceDefinition52LocalReconstruction (27s)
✔ [4160/4195] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [4162/4195] Built Iut.Foundations.SourceDefinition52LocalContinuity (14s)
✔ [4164/4195] Built Iut.Stage1.IUTStage1Data (3.3s)
✔ [4166/4195] Built Iut.Foundations.SourceDefinition52LocalJointContinuity (4.8s)
⚠ [4167/4195] Built Iut.Stage1.IUTStage1SourceCore (74s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:20826: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:21074: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:21141: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:21239:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.ComponentwiseEqual.toResidueModuleQuotientCosetHaarCharacterNormalizationSource`:
  [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:21283:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.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:21359:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueSubmoduleQuotientCosetHaarCharacterNormalizationSource.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:21638: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:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21640:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638: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:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21641:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21638: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:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21645: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:21638: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:21638:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:21655:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678: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:21680:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678: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:21681:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678: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:21684:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678: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:21685:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:21678: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:21686:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [4169/4195] Built Iut.Foundations.SourceDefinition52IndSystem (9.5s)
✔ [4170/4195] Built Iut.Stage1.IUTStage1Remark312Absorption (2.8s)
⚠ [4172/4195] Built Iut.Stage1.IUTStage1IUTIVAlgebra (17s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4161: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:4180: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:4194: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:4236:10: Try `simp at hkind` instead of `simpa using hkind`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4246:10: Try `simp at hkind` instead of `simpa using hkind`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:4267: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:4323: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:4782: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:4863: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:6238: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:6316: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:6362: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:6483: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:6531: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:6640:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [4174/4195] Built Iut.Stage1.IUTStage1FiniteLabels (4.2s)
✔ [4175/4195] Built Iut.Foundations.SourceDefinition52Sequential (6.6s)
⚠ [4176/4195] Built Iut.Stage1.IUTStage1StepX (5.3s)
warning: Iut/Stage1/IUTStage1StepX.lean:552:6: try 'simp' instead of 'simpa'

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

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4177/4195] Built Iut.Foundations.SourceTheorem311Assembly (7.3s)
✔ [4178/4195] Built Iut.Stage1.IUTStage1Gaussian (7.8s)
✔ [4179/4195] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
✔ [4180/4195] Built Iut.Stage1.IUTStage1HodgeArakelovPilots (6.4s)
⚠ [4181/4195] Built Iut.Stage1.IUTStage1Theorem311 (23s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4640: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:4645: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:4799: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:4831: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:4836: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:4879: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:4933: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:4968: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:4973: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:5105: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:5139: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:5144: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:5282: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:5316: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:5321: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:5464: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:5496: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:5501: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:5614: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:7746:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15549: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:16085:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16426:6: unused variable `choice`

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

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

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

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

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [4182/4195] Built Iut.Stage1.IUTStage1ConstructedTheorem311 (8.7s)
ℹ [4183/4195] Built Iut.Stage1.IUTStage1StepXI.Core (504s)
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7497d9dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7497d9dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7497d9dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7497d9ceba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7497d9cebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7497d9dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7497d9c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7497d9c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7497d9c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7497d9c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7497d9dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7497d9a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7497d9dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7497d9dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7497d9d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7497d9a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7497d4e22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7497d4c0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7497d4769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7497d4769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7497d164524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7497d1645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5831232548da]
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7497d9dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7497d9dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7497d9dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7497d9cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7497d9cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7497d9dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7497d9c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7497d9c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7497d9c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7497d9c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7497d9dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7497d9a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7497d9dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7497d9dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7497d9d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7497d9a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7497d4e22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7497d4c0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7497d4769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7497d4769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7497d164524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7497d1645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5831232548da]
✔ [4184/4195] Built Iut.Stage1.IUTStage1StepXI (2.6s)
ℹ [4185/4195] Built Iut.Stage1.IUTStage1FrobenioidShift (227s)
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7cfc98dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7cfc98dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7cfc98dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7cfc98cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7cfc98cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7cfc98dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7cfc98c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7cfc98c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7cfc98c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7cfc98c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7cfc98dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7cfc98a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cfc98dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cfc98dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7cfc98d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7cfc98a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7cfc93e22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7cfc93c0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7cfc93769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7cfc93769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7cfc9064524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7cfc90645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x57483050e8da]
✔ [4186/4195] Built Iut.Stage1.IUTStage1EndpointAudit (3.6s)
✔ [4187/4195] Built Iut.Stage1.IUTStage1Source (3.5s)
✔ [4188/4195] Built Iut.Stage1.IUTStage1Experiments.Diagnostics (46s)
✔ [4189/4195] Built Iut.Stage1.IUTStage1Experiments.ClosedEndpoints (4.2s)
⚠ [4190/4195] Built Iut.Stage1.IUTStage1Experiments.AdditiveHaar (164s)
warning: Iut/Stage1/IUTStage1Experiments/AdditiveHaar.lean:41363:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x70062e7c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x70062e7bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x70062e7bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x70062e6eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x70062e6ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x70062e7caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x70062e632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x70062e632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x70062e633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x70062e6341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x70062e7c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x70062e415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70062e7c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70062e7c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x70062e79b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x70062e415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x700629822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x70062960cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x700629169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x700629169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x70062604524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x700626045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5c0b4abff8da]
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x70062e7c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x70062e7bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x70062e7bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x70062e6f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x70062e6f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x70062e7caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x70062e632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x70062e632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x70062e633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x70062e6341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x70062e7c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x70062e415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70062e7c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70062e7c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x70062e79b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x70062e415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x700629822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x70062960cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x700629169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x700629169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x70062604524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x700626045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5c0b4abff8da]
✔ [4191/4195] Built Iut.Stage1.IUTStage1StepXI.AdditiveHaarBridge (10s)
ℹ [4192/4195] Built Iut.Stage1.IUTStage1StepXIDependencyAudit (16s)
info: Iut/Stage1/IUTStage1StepXIDependencyAudit.lean:3961:0: 'Iut.Stage1.IUTStage1SourcePackage.IUTStage1Theorem311HullDetSourceConstructor.IUTStage1Theorem311OneSidedMultiradialConstructionSource.IUTStage1ConcreteTheorem311PrimitiveSourcePacket.ofSourceSpineDataOneSidedComponentSHECodomainSelectedLabelQPilotBridgeAlignmentOutputFlagCalibrationSource_packetConstructionAudit' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
✔ [4193/4195] Built Iut.Basic (3.2s)
✔ [4194/4195] Built Iut (2.9s)
Build completed successfully (4195 jobs).

apx-runtime-resource-v1	apx-verifier-job-1526-runtime-lean_checker-606529-1785499157417836329-1	1101824	1335296	21474836480	0	0	0	0	0	0	784789504	12090720256	21474836480	0	0	0	0	0	0

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1526-runtime-blueprint_build-606529-1785501008039852649-2	1028096	1536000	21474836480	0	0	0	0	0	0	3153920	107470848	21474836480	0	0	0	0	0	0