Run 1301

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

Cloning into '/var/lib/apodeixis/repos/job-1792-source'...
error: unable to read askpass response from '/usr/bin/false'
fatal: could not read Username for 'https://github.com': terminal prompts disabled

git clone (github installation auth fallback)

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

git checkout 8959a85e8073553935e4d052f02326f65c391aec

Note: switching to '8959a85e8073553935e4d052f02326f65c391aec'.

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 8959a85 Merge pull request #978 from promachina/e21-924-complete

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 (440ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.1s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (112ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (159ms)
✔ [13/25] Built Cache.Lean:c.o (131ms)
✔ [15/25] Built Cache.Init (298ms)
✔ [16/25] Built Cache.IO (1.8s)
✔ [17/25] Built Cache.Init:c.o (91ms)
✔ [18/25] Built Cache.IO:c.o (1.3s)
✔ [19/25] Built Cache.Hashing (913ms)
✔ [20/25] Built Cache.Hashing:c.o (357ms)
✔ [21/25] Built Cache.Requests (2.2s)
✔ [22/25] Built Cache.Requests:c.o (1.9s)
✔ [23/25] Built Cache.Main (910ms)
✔ [24/25] Built Cache.Main:c.o (627ms)
✔ [25/25] Built cache:exe (4.8s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 16 KB/s], Decompressed: 0
Downloaded: 12 file(s) [attempted 12/8459 = 0%, 18 KB/s], Decompressed: 7
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 15 KB/s], Decompressed: 23
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 55 KB/s], Decompressed: 36
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 151 KB/s], Decompressed: 36
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 77 KB/s], Decompressed: 57
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 51 KB/s], Decompressed: 86
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 630 KB/s], Decompressed: 86
Downloaded: 209 file(s) [attempted 209/8459 = 2%, 98 KB/s], Decompressed: 86
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 24 KB/s], Decompressed: 134
Downloaded: 274 file(s) [attempted 274/8459 = 3%, 76 KB/s], Decompressed: 134
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 151 KB/s], Decompressed: 134
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 213 KB/s], Decompressed: 213
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 115 KB/s], Decompressed: 213
Downloaded: 435 file(s) [attempted 435/8459 = 5%, 84 KB/s], Decompressed: 329
Downloaded: 476 file(s) [attempted 476/8459 = 5%, 40 KB/s], Decompressed: 329
Downloaded: 512 file(s) [attempted 512/8459 = 6%, 67 KB/s], Decompressed: 329
Downloaded: 548 file(s) [attempted 548/8459 = 6%, 564 KB/s], Decompressed: 329
Downloaded: 589 file(s) [attempted 589/8459 = 6%, 280 KB/s], Decompressed: 435
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 327 KB/s], Decompressed: 435
Downloaded: 671 file(s) [attempted 671/8459 = 7%, 25 KB/s], Decompressed: 552
Downloaded: 716 file(s) [attempted 716/8459 = 8%, 393 KB/s], Decompressed: 552
Downloaded: 760 file(s) [attempted 760/8459 = 8%, 171 KB/s], Decompressed: 552
Downloaded: 798 file(s) [attempted 798/8459 = 9%, 894 KB/s], Decompressed: 552
Downloaded: 839 file(s) [attempted 839/8459 = 9%, 1335 KB/s], Decompressed: 671
Downloaded: 877 file(s) [attempted 877/8459 = 10%, 74 KB/s], Decompressed: 671
Downloaded: 921 file(s) [attempted 921/8459 = 10%, 251 KB/s], Decompressed: 671
Downloaded: 962 file(s) [attempted 962/8459 = 11%, 195 KB/s], Decompressed: 671
Downloaded: 1003 file(s) [attempted 1003/8459 = 11%, 26 KB/s], Decompressed: 832
Downloaded: 1048 file(s) [attempted 1048/8459 = 12%, 258 KB/s], Decompressed: 832
Downloaded: 1082 file(s) [attempted 1082/8459 = 12%, 268 KB/s], Decompressed: 832
Downloaded: 1123 file(s) [attempted 1123/8459 = 13%, 367 KB/s], Decompressed: 832
Downloaded: 1161 file(s) [attempted 1161/8459 = 13%, 432 KB/s], Decompressed: 832
Downloaded: 1205 file(s) [attempted 1205/8459 = 14%, 323 KB/s], Decompressed: 1003
Downloaded: 1250 file(s) [attempted 1250/8459 = 14%, 575 KB/s], Decompressed: 1003
Downloaded: 1291 file(s) [attempted 1291/8459 = 15%, 252 KB/s], Decompressed: 1003
Downloaded: 1328 file(s) [attempted 1328/8459 = 15%, 91 KB/s], Decompressed: 1003
Downloaded: 1369 file(s) [attempted 1369/8459 = 16%, 766 KB/s], Decompressed: 1003
Downloaded: 1407 file(s) [attempted 1407/8459 = 16%, 241 KB/s], Decompressed: 1192
Downloaded: 1448 file(s) [attempted 1448/8459 = 17%, 277 KB/s], Decompressed: 1192
Downloaded: 1489 file(s) [attempted 1489/8459 = 17%, 49 KB/s], Decompressed: 1192
Downloaded: 1527 file(s) [attempted 1527/8459 = 18%, 1221 KB/s], Decompressed: 1192
Downloaded: 1564 file(s) [attempted 1564/8459 = 18%, 64 KB/s], Decompressed: 1380
Downloaded: 1609 file(s) [attempted 1609/8459 = 19%, 338 KB/s], Decompressed: 1380
Downloaded: 1643 file(s) [attempted 1643/8459 = 19%, 267 KB/s], Decompressed: 1380
Downloaded: 1687 file(s) [attempted 1687/8459 = 19%, 1976 KB/s], Decompressed: 1380
Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 1706 KB/s], Decompressed: 1380
Downloaded: 1769 file(s) [attempted 1769/8459 = 20%, 1090 KB/s], Decompressed: 1557
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 329 KB/s], Decompressed: 1557
Downloaded: 1848 file(s) [attempted 1848/8459 = 21%, 854 KB/s], Decompressed: 1557
Downloaded: 1889 file(s) [attempted 1889/8459 = 22%, 301 KB/s], Decompressed: 1557
Downloaded: 1927 file(s) [attempted 1927/8459 = 22%, 72 KB/s], Decompressed: 1557
Downloaded: 1968 file(s) [attempted 1968/8459 = 23%, 169 KB/s], Decompressed: 1741
Downloaded: 2005 file(s) [attempted 2005/8459 = 23%, 796 KB/s], Decompressed: 1741
Downloaded: 2050 file(s) [attempted 2050/8459 = 24%, 186 KB/s], Decompressed: 1741
Downloaded: 2091 file(s) [attempted 2091/8459 = 24%, 98 KB/s], Decompressed: 1741
Downloaded: 2128 file(s) [attempted 2128/8459 = 25%, 1346 KB/s], Decompressed: 1741
Downloaded: 2166 file(s) [attempted 2166/8459 = 25%, 590 KB/s], Decompressed: 1944
Downloaded: 2211 file(s) [attempted 2211/8459 = 26%, 262 KB/s], Decompressed: 1944
Downloaded: 2252 file(s) [attempted 2252/8459 = 26%, 858 KB/s], Decompressed: 1944
Downloaded: 2293 file(s) [attempted 2293/8459 = 27%, 642 KB/s], Decompressed: 1944
Downloaded: 2330 file(s) [attempted 2330/8459 = 27%, 469 KB/s], Decompressed: 1944
Downloaded: 2368 file(s) [attempted 2368/8459 = 27%, 316 KB/s], Decompressed: 1944
Downloaded: 2412 file(s) [attempted 2412/8459 = 28%, 846 KB/s], Decompressed: 2152
Downloaded: 2447 file(s) [attempted 2447/8459 = 28%, 252 KB/s], Decompressed: 2152
Downloaded: 2491 file(s) [attempted 2491/8459 = 29%, 186 KB/s], Decompressed: 2152
Downloaded: 2525 file(s) [attempted 2525/8459 = 29%, 106 KB/s], Decompressed: 2152
Downloaded: 2570 file(s) [attempted 2570/8459 = 30%, 623 KB/s], Decompressed: 2152
Downloaded: 2614 file(s) [attempted 2614/8459 = 30%, 415 KB/s], Decompressed: 2152
Downloaded: 2655 file(s) [attempted 2655/8459 = 31%, 252 KB/s], Decompressed: 2152
Downloaded: 2696 file(s) [attempted 2696/8459 = 31%, 36 KB/s], Decompressed: 2412
Downloaded: 2734 file(s) [attempted 2734/8459 = 32%, 602 KB/s], Decompressed: 2412
Downloaded: 2771 file(s) [attempted 2771/8459 = 32%, 888 KB/s], Decompressed: 2412
Downloaded: 2812 file(s) [attempted 2812/8459 = 33%, 221 KB/s], Decompressed: 2412
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 333 KB/s], Decompressed: 2412
Downloaded: 2898 file(s) [attempted 2898/8459 = 34%, 182 KB/s], Decompressed: 2412
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 41 KB/s], Decompressed: 2412
Downloaded: 2976 file(s) [attempted 2976/8459 = 35%, 96 KB/s], Decompressed: 2412
Downloaded: 3014 file(s) [attempted 3014/8459 = 35%, 656 KB/s], Decompressed: 2412
Downloaded: 3055 file(s) [attempted 3055/8459 = 36%, 300 KB/s], Decompressed: 2676
Downloaded: 3096 file(s) [attempted 3096/8459 = 36%, 552 KB/s], Decompressed: 2676
Downloaded: 3141 file(s) [attempted 3141/8459 = 37%, 58 KB/s], Decompressed: 2676
Downloaded: 3182 file(s) [attempted 3182/8459 = 37%, 206 KB/s], Decompressed: 2676
Downloaded: 3219 file(s) [attempted 3219/8459 = 38%, 452 KB/s], Decompressed: 2676
Downloaded: 3260 file(s) [attempted 3260/8459 = 38%, 228 KB/s], Decompressed: 2676
Downloaded: 3305 file(s) [attempted 3305/8459 = 39%, 262 KB/s], Decompressed: 2676
Downloaded: 3346 file(s) [attempted 3346/8459 = 39%, 355 KB/s], Decompressed: 2676
Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 610 KB/s], Decompressed: 2676
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 908 KB/s], Decompressed: 3041
Downloaded: 3469 file(s) [attempted 3469/8459 = 41%, 293 KB/s], Decompressed: 3041
Downloaded: 3515 file(s) [attempted 3515/8459 = 41%, 288 KB/s], Decompressed: 3041
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 144 KB/s], Decompressed: 3041
Downloaded: 3585 file(s) [attempted 3585/8459 = 42%, 105 KB/s], Decompressed: 3041
Downloaded: 3630 file(s) [attempted 3630/8459 = 42%, 342 KB/s], Decompressed: 3041
Downloaded: 3671 file(s) [attempted 3671/8459 = 43%, 437 KB/s], Decompressed: 3041
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 343 KB/s], Decompressed: 3041
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 671 KB/s], Decompressed: 3418
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 71 KB/s], Decompressed: 3418
Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 358 KB/s], Decompressed: 3418
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 83 KB/s], Decompressed: 3418
Downloaded: 3924 file(s) [attempted 3924/8459 = 46%, 333 KB/s], Decompressed: 3418
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 125 KB/s], Decompressed: 3418
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 1090 KB/s], Decompressed: 3418
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 75 KB/s], Decompressed: 3418
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 845 KB/s], Decompressed: 3418
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 102 KB/s], Decompressed: 3736
Downloaded: 4166 file(s) [attempted 4166/8459 = 49%, 192 KB/s], Decompressed: 3736
Downloaded: 4207 file(s) [attempted 4207/8459 = 49%, 166 KB/s], Decompressed: 3736
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 31 KB/s], Decompressed: 3736
Downloaded: 4290 file(s) [attempted 4290/8459 = 50%, 330 KB/s], Decompressed: 3736
Downloaded: 4337 file(s) [attempted 4337/8459 = 51%, 308 KB/s], Decompressed: 3736
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 169 KB/s], Decompressed: 3736
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 205 KB/s], Decompressed: 4088
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 1948 KB/s], Decompressed: 4088
Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 601 KB/s], Decompressed: 4088
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 945 KB/s], Decompressed: 4088
Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 530 KB/s], Decompressed: 4088
Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 969 KB/s], Decompressed: 4088
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 782 KB/s], Decompressed: 4088
Downloaded: 4696 file(s) [attempted 4696/8459 = 55%, 35 KB/s], Decompressed: 4416
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 247 KB/s], Decompressed: 4416
Downloaded: 4785 file(s) [attempted 4785/8459 = 56%, 66 KB/s], Decompressed: 4416
Downloaded: 4826 file(s) [attempted 4826/8459 = 57%, 203 KB/s], Decompressed: 4416
Downloaded: 4867 file(s) [attempted 4867/8459 = 57%, 581 KB/s], Decompressed: 4416
Downloaded: 4908 file(s) [attempted 4908/8459 = 58%, 280 KB/s], Decompressed: 4416
Downloaded: 4946 file(s) [attempted 4946/8459 = 58%, 479 KB/s], Decompressed: 4416
Downloaded: 4987 file(s) [attempted 4987/8459 = 58%, 272 KB/s], Decompressed: 4696
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 251 KB/s], Decompressed: 4696
Downloaded: 5076 file(s) [attempted 5076/8459 = 60%, 488 KB/s], Decompressed: 4696
Downloaded: 5114 file(s) [attempted 5114/8459 = 60%, 100 KB/s], Decompressed: 4696
Downloaded: 5155 file(s) [attempted 5155/8459 = 60%, 1255 KB/s], Decompressed: 4696
Downloaded: 5196 file(s) [attempted 5196/8459 = 61%, 301 KB/s], Decompressed: 4696
Downloaded: 5233 file(s) [attempted 5233/8459 = 61%, 253 KB/s], Decompressed: 4696
Downloaded: 5278 file(s) [attempted 5278/8459 = 62%, 381 KB/s], Decompressed: 4984
Downloaded: 5319 file(s) [attempted 5319/8459 = 62%, 460 KB/s], Decompressed: 4984
Downloaded: 5356 file(s) [attempted 5356/8459 = 63%, 173 KB/s], Decompressed: 4984
Downloaded: 5398 file(s) [attempted 5398/8459 = 63%, 190 KB/s], Decompressed: 4984
Downloaded: 5439 file(s) [attempted 5439/8459 = 64%, 628 KB/s], Decompressed: 4984
Downloaded: 5480 file(s) [attempted 5480/8459 = 64%, 194 KB/s], Decompressed: 4984
Downloaded: 5527 file(s) [attempted 5527/8459 = 65%, 150 KB/s], Decompressed: 5250
Downloaded: 5565 file(s) [attempted 5565/8459 = 65%, 128 KB/s], Decompressed: 5250
Downloaded: 5606 file(s) [attempted 5606/8459 = 66%, 673 KB/s], Decompressed: 5250
Downloaded: 5644 file(s) [attempted 5644/8459 = 66%, 641 KB/s], Decompressed: 5250
Downloaded: 5688 file(s) [attempted 5688/8459 = 67%, 133 KB/s], Decompressed: 5250
Downloaded: 5729 file(s) [attempted 5729/8459 = 67%, 1770 KB/s], Decompressed: 5500
Downloaded: 5770 file(s) [attempted 5770/8459 = 68%, 47 KB/s], Decompressed: 5500
Downloaded: 5808 file(s) [attempted 5808/8459 = 68%, 439 KB/s], Decompressed: 5500
Downloaded: 5851 file(s) [attempted 5851/8459 = 69%, 305 KB/s], Decompressed: 5500
Downloaded: 5890 file(s) [attempted 5890/8459 = 69%, 244 KB/s], Decompressed: 5500
Downloaded: 5931 file(s) [attempted 5931/8459 = 70%, 1223 KB/s], Decompressed: 5500
Downloaded: 5969 file(s) [attempted 5969/8459 = 70%, 541 KB/s], Decompressed: 5500
Downloaded: 6006 file(s) [attempted 6006/8459 = 71%, 92 KB/s], Decompressed: 5500
Downloaded: 6047 file(s) [attempted 6047/8459 = 71%, 39 KB/s], Decompressed: 5709
Downloaded: 6092 file(s) [attempted 6092/8459 = 72%, 293 KB/s], Decompressed: 5709
Downloaded: 6133 file(s) [attempted 6133/8459 = 72%, 63 KB/s], Decompressed: 5709
Downloaded: 6170 file(s) [attempted 6170/8459 = 72%, 54 KB/s], Decompressed: 5709
Downloaded: 6208 file(s) [attempted 6208/8459 = 73%, 749 KB/s], Decompressed: 5709
Downloaded: 6246 file(s) [attempted 6246/8459 = 73%, 70 KB/s], Decompressed: 5709
Downloaded: 6293 file(s) [attempted 6293/8459 = 74%, 705 KB/s], Decompressed: 5709
Downloaded: 6341 file(s) [attempted 6341/8459 = 74%, 2747 KB/s], Decompressed: 5709
Downloaded: 6386 file(s) [attempted 6386/8459 = 75%, 384 KB/s], Decompressed: 6040
Downloaded: 6430 file(s) [attempted 6430/8459 = 76%, 325 KB/s], Decompressed: 6040
Downloaded: 6471 file(s) [attempted 6471/8459 = 76%, 191 KB/s], Decompressed: 6040
Downloaded: 6516 file(s) [attempted 6516/8459 = 77%, 520 KB/s], Decompressed: 6040
Downloaded: 6553 file(s) [attempted 6553/8459 = 77%, 602 KB/s], Decompressed: 6040
Downloaded: 6587 file(s) [attempted 6587/8459 = 77%, 266 KB/s], Decompressed: 6040
Downloaded: 6632 file(s) [attempted 6632/8459 = 78%, 2733 KB/s], Decompressed: 6040
Downloaded: 6673 file(s) [attempted 6673/8459 = 78%, 26 KB/s], Decompressed: 6040
Downloaded: 6721 file(s) [attempted 6721/8459 = 79%, 242 KB/s], Decompressed: 6382
Downloaded: 6755 file(s) [attempted 6755/8459 = 79%, 476 KB/s], Decompressed: 6382
Downloaded: 6789 file(s) [attempted 6789/8459 = 80%, 511 KB/s], Decompressed: 6382
Downloaded: 6834 file(s) [attempted 6834/8459 = 80%, 335 KB/s], Decompressed: 6382
Downloaded: 6875 file(s) [attempted 6875/8459 = 81%, 584 KB/s], Decompressed: 6382
Downloaded: 6923 file(s) [attempted 6923/8459 = 81%, 78 KB/s], Decompressed: 6382
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 41 KB/s], Decompressed: 6382
Downloaded: 7011 file(s) [attempted 7011/8459 = 82%, 503 KB/s], Decompressed: 6382
Downloaded: 7046 file(s) [attempted 7046/8459 = 83%, 379 KB/s], Decompressed: 6382
Downloaded: 7083 file(s) [attempted 7083/8459 = 83%, 1994 KB/s], Decompressed: 6382
Downloaded: 7128 file(s) [attempted 7128/8459 = 84%, 1043 KB/s], Decompressed: 6721
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 36 KB/s], Decompressed: 6721
Downloaded: 7214 file(s) [attempted 7214/8459 = 85%, 42 KB/s], Decompressed: 6721
Downloaded: 7251 file(s) [attempted 7251/8459 = 85%, 36 KB/s], Decompressed: 6721
Downloaded: 7285 file(s) [attempted 7285/8459 = 86%, 158 KB/s], Decompressed: 6721
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 163 KB/s], Decompressed: 6721
Downloaded: 7374 file(s) [attempted 7374/8459 = 87%, 246 KB/s], Decompressed: 6721
Downloaded: 7412 file(s) [attempted 7412/8459 = 87%, 124 KB/s], Decompressed: 6721
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 267 KB/s], Decompressed: 6721
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 293 KB/s], Decompressed: 6721
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 90 KB/s], Decompressed: 7121
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 279 KB/s], Decompressed: 7121
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 199 KB/s], Decompressed: 7121
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 288 KB/s], Decompressed: 7121
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 110 KB/s], Decompressed: 7121
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 156 KB/s], Decompressed: 7121
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 111 KB/s], Decompressed: 7121
Downloaded: 7822 file(s) [attempted 7822/8459 = 92%, 137 KB/s], Decompressed: 7121
Downloaded: 7860 file(s) [attempted 7860/8459 = 92%, 21 KB/s], Decompressed: 7121
Downloaded: 7904 file(s) [attempted 7904/8459 = 93%, 78 KB/s], Decompressed: 7121
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 36 KB/s], Decompressed: 7121
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 221 KB/s], Decompressed: 7121
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 420 KB/s], Decompressed: 7514
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 314 KB/s], Decompressed: 7514
Downloaded: 8113 file(s) [attempted 8113/8459 = 95%, 284 KB/s], Decompressed: 7514
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 67 KB/s], Decompressed: 7514
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 370 KB/s], Decompressed: 7514
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 421 KB/s], Decompressed: 7514
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 119 KB/s], Decompressed: 7514
Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 53 KB/s], Decompressed: 7514
Downloaded: 8348 file(s) [attempted 8348/8459 = 98%, 224 KB/s], Decompressed: 7514
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 337 KB/s], Decompressed: 7514
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 751 KB/s], Decompressed: 7514
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 751 KB/s], Decompressed: 7514

apx-runtime-resource-v1	apx-verifier-job-1792-runtime-lake_cache-2488807-1789160222531850712-0	884736	1392640	21474836480	0	0	0	0	0	0	8558080000	8870973440	21474836480	0	0	0	0	0	0

lake build

ease merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3759:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3785:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3877:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3884:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3895:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3903:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3929:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:3946:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4140:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4155:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4176:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4191:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4193:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4216:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4531:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4560:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4562:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4615:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4757:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4786:6: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4788:8: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4841:8: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:4911:4: This simp argument is unused:
  reindexCompCatHom_app_torsorIso_hom

Hint: Omit it from the simp argument list.
  simp only [category_comp_torsorIso_hom,̵
  ̵ ̵ ̵ ̵ ̵r̵e̵i̵n̵d̵e̵x̵C̵o̵m̵p̵C̵a̵t̵H̵o̵m̵_̵a̵p̵p̵_̵t̵o̵r̵s̵o̵r̵I̵s̵o̵_̵h̵o̵m̵] at componentInverse

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5163:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5188:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5284:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5300:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5315:4: This central dot `·` is isolated; please merge it with the next line.

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:7977:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:8145:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
✔ [4604/6594] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverFiniteCoproducts (3.4s)
✔ [4605/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInv (2.8s)
✔ [4607/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.4s)
✔ [4608/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (118s)
✔ [4610/6595] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4611/6595] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.4s)
✔ [4612/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.8s)
✔ [4613/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.2s)
✔ [4614/6595] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.5s)
✔ [4615/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.9s)
✔ [4616/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.9s)
✔ [4617/6595] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.7s)
✔ [4618/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (3.1s)
⚠ [4619/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (164s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2163:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2166:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2169:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2448:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2451:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2454:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2460:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2463:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2466:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4620/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (42s)
✔ [4621/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (2.0s)
✔ [4622/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.7s)
✔ [4623/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.9s)
✔ [4624/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.8s)
✔ [4626/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4627/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.8s)
✔ [4628/6595] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.4s)
✔ [4629/6595] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.8s)
✔ [4630/6595] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (3.1s)
✔ [4631/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.4s)
✔ [4632/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.9s)
⚠ [4633/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverCollapse (10s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverCollapse.lean:1268:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4634/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackCriterion (3.0s)
✔ [4635/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.7s)
✔ [4636/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.3s)
✔ [4637/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.9s)
✔ [4638/6598] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.8s)
✔ [4639/6598] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.0s)
✔ [4640/6599] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.0s)
✔ [4641/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.4s)
✔ [4642/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (3.0s)
⚠ [4643/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (897s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1177:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1268:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1329:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1409:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2812:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2917:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3052:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3103:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3150:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3191:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3572:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3699:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3826:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3958:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4089:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4266:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4420:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4586:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5027:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5159:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5333:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5438:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5573:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5687:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 4000000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5764:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5813:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5904:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5965:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6033:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6088:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6128:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6211:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6460: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/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6815:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4644/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasBaseChange (17s)
✔ [4645/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.9s)
✔ [4646/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.4s)
✔ [4647/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.8s)
✔ [4649/6599] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.7s)
✔ [4650/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (3.2s)
✔ [4651/6599] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (3.9s)
✔ [4653/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (128s)
✔ [4654/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (124s)
✔ [4655/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.6s)
✔ [4656/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.2s)
✔ [4657/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.7s)
✔ [4658/6600] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.0s)
✔ [4660/6600] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.2s)
✔ [4661/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.6s)
✔ [4662/6600] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (2.9s)
✔ [4663/6600] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (3.1s)
✔ [4664/6600] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.2s)
✔ [4665/6600] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.5s)
✔ [4666/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.3s)
✔ [4667/6600] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.8s)
✔ [4668/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (104s)
✔ [4669/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.1s)
✔ [4670/6602] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.8s)
✔ [4671/6602] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.3s)
✔ [4672/6604] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.2s)
✔ [4675/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.3s)
✔ [4676/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (3.0s)
✔ [4677/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.2s)
✔ [4678/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.0s)
✔ [4679/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.9s)
✔ [4680/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.9s)
✔ [4681/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.4s)
✔ [4682/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (3.0s)
✔ [4683/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.1s)
✔ [4684/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.3s)
✔ [4685/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.9s)
✔ [4686/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.0s)
✔ [4687/6604] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineRefinement (3.8s)
✔ [4688/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLift (3.1s)
✔ [4690/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantComponent (26s)
✔ [4691/6604] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.3s)
✔ [4692/6605] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphism (3.4s)
✔ [4694/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (3.2s)
✔ [4695/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.9s)
✔ [4696/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.3s)
✔ [4697/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentConstruction (44s)
✔ [4698/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairMiddleIso (3.0s)
✔ [4699/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoValue (3.1s)
✔ [4700/6605] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHomComparison (2.8s)
✔ [4701/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (3.0s)
✔ [4702/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (13s)
✔ [4704/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (19s)
✔ [4705/6605] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (3.0s)
✔ [4706/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.6s)
✔ [4708/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.2s)
✔ [4709/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.3s)
✔ [4710/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.2s)
✔ [4711/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.9s)
✔ [4712/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (14s)
✔ [4713/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4714/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (3.0s)
✔ [4715/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4716/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (298s)
✔ [4717/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (14s)
✔ [4719/6607] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.4s)
✔ [4720/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.7s)
✔ [4722/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (3.3s)
✔ [4723/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (3.1s)
✔ [4724/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (3.1s)
✔ [4725/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.1s)
✔ [4726/6609] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.1s)
✔ [4727/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (3.2s)
✔ [4728/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.8s)
✔ [4729/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.8s)
✔ [4730/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.8s)
✔ [4731/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.1s)
✔ [4732/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.9s)
✔ [4733/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.8s)
⚠ [4734/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransHom (2.0s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransHom.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4735/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceCompatibility (3.2s)
✔ [4736/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceAssociator (3.0s)
✔ [4737/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCoverOverlapComparisonLeft (2.9s)
✔ [4738/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparison (2.9s)
✔ [4739/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (3.1s)
✔ [4740/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.3s)
✔ [4741/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.6s)
✔ [4742/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (18s)
✔ [4743/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.8s)
✔ [4744/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.7s)
✔ [4746/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (3.1s)
✔ [4747/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.9s)
✔ [4749/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (3.1s)
✔ [4750/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (3.1s)
⚠ [4751/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport (3.0s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:44:13: This simp argument is unused:
  Category.assoc

Hint: Omit it from the simp argument list.
  simp only [C̵a̵t̵e̵g̵o̵r̵y̵.̵a̵s̵s̵o̵c̵,̵ ̵Iso.inv_hom_id_assoc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4752/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftInv (3.0s)
✔ [4753/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (3.0s)
✔ [4754/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.0s)
✔ [4755/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (3.0s)
✔ [4756/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (4.1s)
✔ [4757/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.5s)
✔ [4758/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (2.9s)
✔ [4759/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (3.1s)
⚠ [4760/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransInv (3.1s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransInv.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4761/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonHom (3.1s)
✔ [4762/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (3.0s)
✔ [4763/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.9s)
✔ [4764/6610] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (3.1s)
✔ [4765/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.8s)
✔ [4766/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.9s)
✔ [4767/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4768/6610] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.1s)
✔ [4769/6610] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.9s)
✔ [4770/6610] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4771/6610] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (3.8s)
✔ [4772/6635] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.7s)
✔ [4773/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (3.0s)
✔ [4774/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (2.9s)
✔ [4776/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.2s)
✔ [4778/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (3.1s)
✔ [4779/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4780/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmHom (2.9s)
⚠ [4781/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects (3.4s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:59:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4782/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (2.0s)
✔ [4783/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (2.0s)
✔ [4784/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.4s)
✔ [4785/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (3.1s)
⚠ [4786/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints (3.1s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:45:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4787/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.9s)
✔ [4788/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (3.0s)
✔ [4789/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.1s)
✔ [4790/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (2.9s)
✔ [4791/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (3.1s)
✔ [4792/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.2s)
✔ [4793/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.1s)
✔ [4794/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.8s)
✔ [4795/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (3.1s)
✔ [4796/6750] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (549s)
✔ [4797/6750] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.9s)
✔ [4798/6750] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (200s)
✔ [4799/6750] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.3s)
✔ [4800/6750] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.8s)
✔ [4802/6750] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.7s)
✔ [4803/6750] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.4s)
✔ [4804/6750] Built Iut.Foundations.SourceFiniteEtaleInvariantAlgHomOrbit (2.5s)
✔ [4805/7786] Built Iut.Foundations.SourceSingleObjTypesOrbitColimit (1.7s)
✔ [4806/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.1s)
✔ [4808/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.0s)
✔ [4809/8799] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (2.9s)
✔ [4810/8799] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.5s)
✔ [4811/8799] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.9s)
✔ [4812/8799] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.5s)
✔ [4813/8799] Built Iut.Foundations.SourceChosenPullbackFunctoriality (1.9s)
✔ [4814/8799] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsEtaleSite (2.7s)
✔ [4815/8799] Built Iut.Foundations.SourceOrbicurveEtaleFundamentalGroupTransport (3.1s)
✔ [4816/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverSliceEquivalence (3.1s)
✔ [4817/8799] Built Iut.Foundations.SourceEquivalenceMateNaturality (1.6s)
✔ [4818/8799] Built Iut.Foundations.SourcePseudofunctorStrongTransIsoOfComponents (3.1s)
✔ [4819/8799] Built Iut.Foundations.SourceAnabelioidEquivalence (2.9s)
✔ [4820/8799] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.8s)
✔ [4821/8799] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.3s)
✔ [4822/8799] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.0s)
✔ [4823/8799] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.8s)
✔ [4824/8921] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.8s)
✔ [4825/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (2.9s)
⚠ [4826/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4827/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCompositor (3.0s)
⚠ [4828/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell (3.3s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4829/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHomProjection (3.1s)
✔ [4830/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalHom (2.0s)
✔ [4831/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleHom (2.8s)
✔ [4832/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeConeIso (3.2s)
⚠ [4833/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom (3.1s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4834/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapCompositeTargetToCocycleHom (2.9s)
✔ [4835/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToZeroValueIsoHom (3.1s)
✔ [4836/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectMiddleFactor (3.1s)
✔ [4837/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMapped (2.0s)
✔ [4838/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightSymmInv (2.9s)
✔ [4839/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInverseSolve (3.1s)
✔ [4840/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInv (2.9s)
✔ [4841/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvAbsorbPointTransport (2.9s)
✔ [4842/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedFirstWhiskeredHom (3.2s)
✔ [4843/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCocycle (3.2s)
✔ [4844/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionCoherence (3.9s)
✔ [4845/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedProjection (3.1s)
✔ [4846/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientSchemeAtlas (3.2s)
✔ [4847/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientInvariantTargetDescent (5.5s)
✔ [4848/8991] Built Iut.Foundations.SourceFiniteEtaleTensorAction (3.7s)
✔ [4849/8991] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTargetToY (2.9s)
✔ [4851/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberPullbacks (2.6s)
✔ [4853/8991] Built Iut.Foundations.SourceFiniteEtaleClopenIdempotentQuotient (2.0s)
✔ [4854/8991] Built Iut.Foundations.SourceTensorProductScalarTowerQuotient (1.8s)
✔ [4855/8991] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionTensor (7.3s)
✔ [4856/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteLimits (2.8s)
✔ [4857/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeBinaryCoproducts (12s)
✔ [4858/8991] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantObject (3.1s)
✔ [4859/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverMonoCharacteristicIdempotent (2.9s)
✔ [4860/8991] Built Iut.Foundations.SourceRingEquivConjugationData (1.5s)
✔ [4861/8991] Built Iut.Foundations.SourceInvariantIdealQuotientInvolution (1.9s)
✔ [4862/8991] Built Iut.Foundations.SourceAffineScalarExtensionReversedTensorNaturality (16s)
✔ [4863/8991] Built Iut.Foundations.SourceTensorProductRightAlgEquiv (1.7s)
✔ [4864/8991] Built Iut.Foundations.SourceTensorProductTmulMulInclusions (1.8s)
✔ [4865/8991] Built Iut.Foundations.SourceRingHomRangeActionMul (1.6s)
✔ [4866/8991] Built Iut.Foundations.SourceRingHomRangeEquiv (1.6s)
✔ [4867/8991] Built Iut.Foundations.SourceRingEquivApplyHEqOfCarrierEq (1.4s)
✔ [4868/8991] Built Iut.Foundations.SourceEquivTransportApplyBack (746ms)
✔ [4869/8991] Built Iut.Foundations.SourceTensorProductSpecHomExt (2.4s)
✔ [4870/8991] Built Iut.Foundations.SourceCategoryFourfoldReassociation (1.4s)
✔ [4871/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverIdentitySectionLift (3.2s)
✔ [4872/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCompProjection (1.9s)
✔ [4873/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentNormalizedMultiplicationHom (3.0s)
✔ [4874/8991] Built Iut.Foundations.SourceCategoryIsoConjugationCancel (2.8s)
✔ [4875/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasFirstSheetProjection (2.9s)
✔ [4876/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftReassociation (3.1s)
✔ [4877/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasTotalSpaceNormalization (15s)
✔ [4878/8991] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHom (2.7s)
✔ [4879/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInversionIsoFirstSheetTotalSpace (4.0s)
✔ [4880/8991] Built Iut.Foundations.SourceEtalePseudofunctorInvolutionConePasting (3.0s)
✔ [4881/8991] Built Iut.Foundations.SourceCategoryIsoFactorCancellation (2.6s)
✔ [4882/8991] Built Iut.Foundations.SourceCategoryThreeCompatibilityPasting (1.5s)
✔ [4883/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasTripleOverlapLongConeCells (3.1s)
✔ [4884/8991] Built Iut.Foundations.SourceCategoryEqualityPostcompositionIdentity (1.4s)
✔ [4885/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverPullbackMorphismDetection (3.2s)
✔ [4886/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMap (5.8s)
✔ [4887/8991] Built Iut.Foundations.SourceCategoryTheoryColimMapFunctoriality (1.5s)
✔ [4888/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverStrictEpiUnderlyingScheme (2.8s)
✔ [4889/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentNormalizedNaturality (34s)
✔ [4890/8991] Built Iut.Foundations.SourceSignSwapActionCoproductQuotient (3.6s)
✔ [4891/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorProjectionEffectiveEpi (2.0s)
✔ [4892/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorEquivariantMapIso (4.5s)
✔ [4893/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientTrivialAtlasIdentityPoint (2.8s)
✔ [4894/8991] Built Iut.Foundations.SourceCategoryMiddleIdentityConjugation (2.8s)
✔ [4895/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftCompatibilityRightContext (1.5s)
✔ [4896/8991] Built Iut.Foundations.SourceCategoryThreeLegPasting (1.5s)
✔ [4897/8991] Built Iut.Foundations.SourceCategoryFunctorOfObjMap (1.4s)
✔ [4898/8991] Built Iut.Foundations.SourceCategoryThreeProjectionPastingCore (1.6s)
✔ [4899/8991] Built Iut.Foundations.SourceCategoryFactorizedMiddlePasting (1.4s)
✔ [4900/8991] Built Iut.Foundations.SourceCategoryThreeLegQuotientPasting (1.5s)
✔ [4901/8991] Built Iut.Foundations.SourceCategoryFiveLegPasting (1.5s)
✔ [4902/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexHomExt (3.4s)
✔ [4903/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftToTestPasting (1.4s)
✔ [4904/8991] Built Iut.Foundations.SourceEqualityProofPackage (329ms)
✔ [4905/8991] Built Iut.Foundations.SourceCategoryReplaceRightmostFactor (1.4s)
✔ [4906/8991] Built Iut.Foundations.SourceCategoryReplaceTwoRightFactors (1.4s)
✔ [4907/8991] Built Iut.Foundations.SourceCategoryPrefixFactorPasting (1.4s)
✔ [4908/8991] Built Iut.Foundations.SourceCategoryTwoCompatibilityPasting (1.4s)
✔ [4909/8991] Built Iut.Foundations.SourceCategoryCongrThreeFactors (1.4s)
✔ [4910/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataDependentCongrArg (1.4s)
✔ [4911/8991] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePasting (1.8s)
✔ [4912/8991] Built Iut.Foundations.SourceCategoryTwoMorphismHEqPastingData (1.4s)
✔ [4913/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseFst (3.0s)
✔ [4914/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionTotalNaturality (4.6s)
✔ [4915/8991] Built Iut.Foundations.SourceEtalePseudofunctorYonedaRecoveryModificationNaturality (5.1s)
✔ [4916/8991] Built Iut.Foundations.SourceCategoryHEqEndpointProjections (1.4s)
✔ [4917/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparisonConverse (2.7s)
✔ [4918/8991] Built Iut.Foundations.SourceFinitaryExtensiveComplementComparison (1.8s)
✔ [4919/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeIso (3.4s)
✔ [4920/8991] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimits (2.8s)
✔ [4921/8991] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4922/8991] Built Iut.Foundations.SourceContinuousActionRestrictionSurjectivity (4.3s)
✔ [4923/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCongrProjection (1.6s)
✔ [4924/8991] Built Iut.Foundations.SourceFiniteAlgebraSeparableClosureFactorization (2.8s)
✔ [4925/8991] Built Iut.Foundations.SourceProfiniteKernelLift (2.9s)
✔ [4926/8991] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapData (322ms)
✔ [4927/8991] Built Iut.Foundations.SourcePullbackSelectedSectionAction (1.6s)
✔ [4928/8991] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeComponentHEq (1.5s)
✔ [4929/8991] Built Iut.Foundations.SourceCategoryTheoryDetachedNaturalityPastingMaps (1.5s)
✔ [4930/8991] Built Iut.Foundations.SourceProfiniteClosedSubgroupOpenExtension (2.0s)
✔ [4931/8991] Built Iut.Foundations.SourcePretransitiveContinuousActionCoset (3.4s)
✔ [4932/8991] Built Iut.Foundations.SourcePointedAnabelioidFiberEquivariance (2.8s)
✔ [4933/8991] Built Iut.Foundations.SourceSpecRingHomSemiconjugacy (2.3s)
✔ [4934/8991] Built Iut.Foundations.SourceCategoryTheoryIsoRightFactorInvOfHomEq (1.3s)
✔ [4935/8991] Built Iut.Foundations.SourceFintypeCatFunctorMapCompApply (1.6s)
✔ [4936/8991] Built Iut.Foundations.SourceCategoryPackedTwoProjectionPasting (1.4s)
✔ [4937/8991] Built Iut.Foundations.SourceCategoryHEqPrecomposition (1.4s)
✔ [4938/8991] Built Iut.Foundations.SourceCategoryTheoryEquivalenceInverseObjectIsoCounit (1.4s)
✔ [4939/8991] Built Iut.Foundations.SourceCategoryTwoMorphismEquationDataOfCompositeEq (1.3s)
✔ [4940/8991] Built Iut.Foundations.SourceHEqTransExplicit (1.5s)
✔ [4941/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonData (1.4s)
✔ [4942/8991] Built Iut.Foundations.SourceFunctionPointwiseFactorizationData (355ms)
✔ [4943/8991] Built Iut.Foundations.SourceFintypeFunctorFactorizationApply (1.7s)
✔ [4944/8991] Built Iut.Foundations.SourceFunctionHEqCastMapData (379ms)
✔ [4945/8991] Built Iut.Foundations.SourceFunctionPointwiseEqualityData (373ms)
✔ [4946/8991] Built Iut.Foundations.SourceFunctionHEqCongr (327ms)
✔ [4947/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorage (1.4s)
✔ [4948/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataOfTwoHEq (1.4s)
✔ [4949/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionData (1.5s)
✔ [4950/8991] Built Iut.Foundations.SourceSelectedFiberComponentDomination (1.7s)
✔ [4951/8991] Built Iut.Foundations.SourceContinuousActionRestrictionComponentStability (3.2s)
✔ [4952/8991] Built Iut.Foundations.SourceHEqApply (340ms)
✔ [4953/8991] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionNaturality (4.7s)
✔ [4954/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftSchemeMap (2.0s)
✔ [4955/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointHEqWhisker (1.4s)
✔ [4956/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentObjectPullbackProjections (2.0s)
✔ [4957/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivialAtlasFirstSheetExt (3.7s)
✔ [4958/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSource (2.9s)
✔ [4959/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentOverlapComparisonLeft (3.0s)
✔ [4960/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseLeftProjection (3.0s)
✔ [4961/8991] Built Iut.Foundations.SourceCategoryInvolutiveActionTransport (1.5s)
✔ [4962/8991] Built Iut.Foundations.SourceRegularInvolutivePullbackFiberSwap (1.8s)
✔ [4963/8991] Built Iut.Foundations.SourceEtaleStackFiniteEtaleComposition (5.5s)
✔ [4964/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkContext (1.4s)
✔ [4965/8991] Built Iut.Foundations.SourceCategoryDetachedHEqData (370ms)
✔ [4966/8991] Built Iut.Foundations.SourceCategoryComparisonProjectionContext (1.3s)
✔ [4967/8991] Built Iut.Foundations.SourceCategoryDetachedEqDataProjections (333ms)
✔ [4968/8991] Built Iut.Foundations.SourceProfinitePostcompositionKernelIso (4.5s)
✔ [4969/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerExactSequence (3.2s)
✔ [4970/8991] Built Iut.Foundations.SourceProfiniteOpenSubgroupKernelIso (3.7s)
✔ [4971/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoNaturality (3.2s)
✔ [4972/8991] Built Iut.Foundations.SourceOrbicurveSignInvariantCategory (3.2s)
✔ [4973/8991] Built Iut.Foundations.SourcePseudofunctorStrongTransCompNaturalityInvApp (1.7s)
✔ [4974/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePasting (1.4s)
✔ [4975/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNestedFactorization (2.9s)
✔ [4976/8992] Built Iut.Foundations.SourceFiberFunctorComparison (2.5s)
✔ [4977/8992] Built Iut.Foundations.SourceSchemeEtaleStackPresentationReverseFiniteEtaleCover (3.0s)
✔ [4978/8992] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullbackEquivalence (3.9s)
✔ [4979/8992] Built Iut.Foundations.SourcePreGaloisFiberFunctorEquivalenceTransport (1.6s)
✔ [4980/8992] Built Iut.Foundations.SourcePseudofunctorRestrictionPullHom (2.1s)
✔ [4981/8992] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsSliceEquivalence (4.3s)
✔ [4982/8992] Built Iut.Foundations.SourceEtaleFundamentalGroupCoverActionEquivalence (2.7s)
✔ [4983/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightDataRight (2.0s)
✔ [4985/8992] Built Iut.Foundations.SourceCategoryFourLegSquareReassociation (1.4s)
✔ [4986/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullLeft (1.9s)
✔ [4987/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullRight (2.3s)
✔ [4988/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIsoSource (2.0s)
✔ [4989/8992] Built Iut.Foundations.SourceCategoryFunctorMapSubsingletonComposition (1.5s)
✔ [4990/8992] Built Iut.Foundations.SourceCategoryEndpointTransportPasting (1.5s)
✔ [4991/8992] Built Iut.Foundations.SourceCategoryMappedTwoThreePasting (1.4s)
✔ [4992/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasPointFiberIsoNaturalityFirstSheet (5.5s)
✔ [4993/8992] Built Iut.Foundations.SourceCategoryMappedNaturalityPasting (1.4s)
✔ [4994/8992] Built Iut.Foundations.SourceCategoryPullNaturalityThroughIso (1.4s)
✔ [4995/8992] Built Iut.Foundations.SourceCategoryThreeFactorIsoRecoveryData (1.5s)
✔ [4996/8992] Built Iut.Foundations.SourceCategoryThreeMapHEq (1.4s)
✔ [4997/8992] Built Iut.Foundations.SourceCategoryRecoverFactorThroughMappedIso (1.4s)
✔ [4998/8992] Built Iut.Foundations.SourceEtalePseudofunctorYonedaIdentityBaseChange (3.3s)
✔ [4999/8992] Built Iut.Foundations.SourceInitialTheta11a1DivisionRootFiberToThirtyTorsion (4.4s)
⚠ [5000/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints (3.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:53:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
⚠ [5001/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData (3.0s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [5002/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalProjection (3.8s)
✔ [5003/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleIdentity (3.3s)
✔ [5004/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTriplePastedConeIso (3.0s)
✔ [5005/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleLongEdgeGeometricTargetAfterSourceAssociator (3.6s)
✔ [5006/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMappedRight (3.2s)
✔ [5007/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveSecondOverlapValueFactorDataMapped (2.9s)
✔ [5008/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveFirstOverlapValueFactorDataMapped (2.9s)
✔ [5009/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightWhiskerRightSymmInv (2.9s)
✔ [5010/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightCongrIsoSymmInv (2.8s)
⚠ [5011/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr (2.9s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr.lean:7:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [5012/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapLocalMapCechData (2.8s)
✔ [5013/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.6s)
✔ [5014/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.0s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1792-runtime-lean_checker-2488807-1789160279224754432-1 on attempt 1

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1792-runtime-blueprint_build-2488807-1789167479988494347-2	888832	1331200	21474836480	0	0	0	0	0	0	5492736	108515328	21474836480	0	0	0	0	0	0