Verification run
Run 1210
succeededcommit
96868cb82707toolchain lean-v4-30-0prover leantook 3h 15m · finished 6w agoPackage inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
(no log excerpt)
Command runs
git_cloneexit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1548-source
Cloning into '/var/lib/apodeixis/repos/job-1548-source'...
git_checkoutexit 0
git checkout 96868cb8270774e8d87ce8cf5e43ea7932bc97e8
Note: switching to '96868cb8270774e8d87ce8cf5e43ea7932bc97e8'. 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 96868cb Merge pull request #50 from promachina/agent/45-countable-temperoids
lake_cacheexit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
✔ [8/25] Built Cache.Lean (604ms) ✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.3s) ✔ [11/25] Built Batteries.Data.String.Basic:c.o (107ms) ✔ [12/25] Built Batteries.Data.String.Matcher:c.o (158ms) ✔ [13/25] Built Cache.Lean:c.o (134ms) ✔ [15/25] Built Cache.Init (412ms) ✔ [16/25] Built Cache.IO (2.5s) ✔ [17/25] Built Cache.Init:c.o (79ms) ✔ [18/25] Built Cache.IO:c.o (1.3s) ✔ [19/25] Built Cache.Hashing (1.0s) ✔ [20/25] Built Cache.Hashing:c.o (342ms) ✔ [21/25] Built Cache.Requests (2.2s) ✔ [22/25] Built Cache.Requests:c.o (1.8s) ✔ [23/25] Built Cache.Main (1.0s) ✔ [24/25] Built Cache.Main:c.o (513ms) ✔ [25/25] Built cache:exe (4.7s) Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 9 Downloaded: 35 file(s) [attempted 35/8459 = 0%, 30 KB/s], Decompressed: 26 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 31 KB/s], Decompressed: 52 Downloaded: 88 file(s) [attempted 88/8459 = 1%, 54 KB/s], Decompressed: 75 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 383 KB/s], Decompressed: 88 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 80 KB/s], Decompressed: 127 Downloaded: 192 file(s) [attempted 192/8459 = 2%, 43 KB/s], Decompressed: 127 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 361 KB/s], Decompressed: 155 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 889 KB/s], Decompressed: 199 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 86 KB/s], Decompressed: 240 Downloaded: 343 file(s) [attempted 343/8459 = 4%, 244 KB/s], Decompressed: 240 Downloaded: 377 file(s) [attempted 377/8459 = 4%, 82 KB/s], Decompressed: 295 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 97 KB/s], Decompressed: 357 Downloaded: 459 file(s) [attempted 459/8459 = 5%, 57 KB/s], Decompressed: 357 Downloaded: 504 file(s) [attempted 504/8459 = 5%, 244 KB/s], Decompressed: 415 Downloaded: 538 file(s) [attempted 538/8459 = 6%, 334 KB/s], Decompressed: 415 Downloaded: 579 file(s) [attempted 579/8459 = 6%, 34 KB/s], Decompressed: 483 Downloaded: 617 file(s) [attempted 617/8459 = 7%, 179 KB/s], Decompressed: 483 Downloaded: 655 file(s) [attempted 655/8459 = 7%, 180 KB/s], Decompressed: 548 Downloaded: 696 file(s) [attempted 696/8459 = 8%, 205 KB/s], Decompressed: 620 Downloaded: 737 file(s) [attempted 737/8459 = 8%, 284 KB/s], Decompressed: 620 Downloaded: 781 file(s) [attempted 781/8459 = 9%, 300 KB/s], Decompressed: 696 Downloaded: 822 file(s) [attempted 822/8459 = 9%, 1929 KB/s], Decompressed: 696 Downloaded: 860 file(s) [attempted 860/8459 = 10%, 570 KB/s], Decompressed: 771 Downloaded: 901 file(s) [attempted 901/8459 = 10%, 586 KB/s], Decompressed: 771 Downloaded: 942 file(s) [attempted 942/8459 = 11%, 177 KB/s], Decompressed: 836 Downloaded: 987 file(s) [attempted 987/8459 = 11%, 399 KB/s], Decompressed: 836 Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 315 KB/s], Decompressed: 836 Downloaded: 1072 file(s) [attempted 1072/8459 = 12%, 377 KB/s], Decompressed: 932 Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 267 KB/s], Decompressed: 932 Downloaded: 1161 file(s) [attempted 1161/8459 = 13%, 595 KB/s], Decompressed: 932 Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 318 KB/s], Decompressed: 1048 Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 479 KB/s], Decompressed: 1048 Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 895 KB/s], Decompressed: 1048 Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 309 KB/s], Decompressed: 1172 Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 866 KB/s], Decompressed: 1172 Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 391 KB/s], Decompressed: 1172 Downloaded: 1452 file(s) [attempted 1452/8459 = 17%, 523 KB/s], Decompressed: 1305 Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 274 KB/s], Decompressed: 1305 Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 1234 KB/s], Decompressed: 1305 Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 83 KB/s], Decompressed: 1432 Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 94 KB/s], Decompressed: 1432 Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 136 KB/s], Decompressed: 1432 Downloaded: 1695 file(s) [attempted 1695/8459 = 20%, 153 KB/s], Decompressed: 1548 Downloaded: 1740 file(s) [attempted 1740/8459 = 20%, 326 KB/s], Decompressed: 1548 Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 1111 KB/s], Decompressed: 1548 Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 224 KB/s], Decompressed: 1685 Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 142 KB/s], Decompressed: 1685 Downloaded: 1907 file(s) [attempted 1907/8459 = 22%, 43 KB/s], Decompressed: 1685 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 834 KB/s], Decompressed: 1685 Downloaded: 1993 file(s) [attempted 1993/8459 = 23%, 70 KB/s], Decompressed: 1815 Downloaded: 2027 file(s) [attempted 2027/8459 = 23%, 975 KB/s], Decompressed: 1815 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 37 KB/s], Decompressed: 1815 Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 247 KB/s], Decompressed: 1952 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 128 KB/s], Decompressed: 1952 Downloaded: 2198 file(s) [attempted 2198/8459 = 25%, 201 KB/s], Decompressed: 1952 Downloaded: 2239 file(s) [attempted 2239/8459 = 26%, 699 KB/s], Decompressed: 1952 Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 214 KB/s], Decompressed: 2103 Downloaded: 2311 file(s) [attempted 2311/8459 = 27%, 38 KB/s], Decompressed: 2103 Downloaded: 2352 file(s) [attempted 2352/8459 = 27%, 1009 KB/s], Decompressed: 2103 Downloaded: 2400 file(s) [attempted 2400/8459 = 28%, 543 KB/s], Decompressed: 2253 Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 265 KB/s], Decompressed: 2253 Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 363 KB/s], Decompressed: 2253 Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 229 KB/s], Decompressed: 2253 Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 161 KB/s], Decompressed: 2390 Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 553 KB/s], Decompressed: 2390 Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 52 KB/s], Decompressed: 2534 Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 61 KB/s], Decompressed: 2534 Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 76 KB/s], Decompressed: 2534 Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 949 KB/s], Decompressed: 2647 Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 669 KB/s], Decompressed: 2647 Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 1472 KB/s], Decompressed: 2746 Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 303 KB/s], Decompressed: 2746 Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 692 KB/s], Decompressed: 2746 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 25 KB/s], Decompressed: 2849 Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 314 KB/s], Decompressed: 2849 Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 195 KB/s], Decompressed: 2849 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 65 KB/s], Decompressed: 2982 Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 1105 KB/s], Decompressed: 2982 Downloaded: 3187 file(s) [attempted 3187/8459 = 37%, 60 KB/s], Decompressed: 2982 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 172 KB/s], Decompressed: 3095 Downloaded: 3276 file(s) [attempted 3276/8459 = 38%, 99 KB/s], Decompressed: 3095 Downloaded: 3317 file(s) [attempted 3317/8459 = 39%, 28 KB/s], Decompressed: 3196 Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 123 KB/s], Decompressed: 3196 Downloaded: 3406 file(s) [attempted 3406/8459 = 40%, 646 KB/s], Decompressed: 3290 Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 413 KB/s], Decompressed: 3290 Downloaded: 3489 file(s) [attempted 3489/8459 = 41%, 491 KB/s], Decompressed: 3379 Downloaded: 3526 file(s) [attempted 3526/8459 = 41%, 264 KB/s], Decompressed: 3379 Downloaded: 3567 file(s) [attempted 3567/8459 = 42%, 481 KB/s], Decompressed: 3468 Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 38 KB/s], Decompressed: 3468 Downloaded: 3656 file(s) [attempted 3656/8459 = 43%, 300 KB/s], Decompressed: 3557 Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 40 KB/s], Decompressed: 3557 Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 481 KB/s], Decompressed: 3653 Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 202 KB/s], Decompressed: 3653 Downloaded: 3834 file(s) [attempted 3834/8459 = 45%, 468 KB/s], Decompressed: 3653 Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 1277 KB/s], Decompressed: 3752 Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 119 KB/s], Decompressed: 3752 Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 201 KB/s], Decompressed: 3855 Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 287 KB/s], Decompressed: 3855 Downloaded: 4046 file(s) [attempted 4046/8459 = 47%, 640 KB/s], Decompressed: 3951 Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 257 KB/s], Decompressed: 3951 Downloaded: 4122 file(s) [attempted 4122/8459 = 48%, 153 KB/s], Decompressed: 3951 Downloaded: 4159 file(s) [attempted 4159/8459 = 49%, 70 KB/s], Decompressed: 4046 Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 633 KB/s], Decompressed: 4046 Downloaded: 4248 file(s) [attempted 4248/8459 = 50%, 495 KB/s], Decompressed: 4149 Downloaded: 4289 file(s) [attempted 4289/8459 = 50%, 403 KB/s], Decompressed: 4149 Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 207 KB/s], Decompressed: 4149 Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 423 KB/s], Decompressed: 4248 Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 313 KB/s], Decompressed: 4248 Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 192 KB/s], Decompressed: 4344 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 209 KB/s], Decompressed: 4344 Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 111 KB/s], Decompressed: 4440 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 151 KB/s], Decompressed: 4440 Downloaded: 4628 file(s) [attempted 4628/8459 = 54%, 153 KB/s], Decompressed: 4536 Downloaded: 4669 file(s) [attempted 4669/8459 = 55%, 106 KB/s], Decompressed: 4536 Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 318 KB/s], Decompressed: 4615 Downloaded: 4758 file(s) [attempted 4758/8459 = 56%, 93 KB/s], Decompressed: 4615 Downloaded: 4799 file(s) [attempted 4799/8459 = 56%, 160 KB/s], Decompressed: 4702 Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 51 KB/s], Decompressed: 4702 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 130 KB/s], Decompressed: 4775 Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 348 KB/s], Decompressed: 4775 Downloaded: 4960 file(s) [attempted 4960/8459 = 58%, 40 KB/s], Decompressed: 4851 Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 137 KB/s], Decompressed: 4851 Downloaded: 5053 file(s) [attempted 5053/8459 = 59%, 202 KB/s], Decompressed: 4940 Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 392 KB/s], Decompressed: 4940 Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 64 KB/s], Decompressed: 4940 Downloaded: 5179 file(s) [attempted 5179/8459 = 61%, 266 KB/s], Decompressed: 5032 Downloaded: 5220 file(s) [attempted 5220/8459 = 61%, 80 KB/s], Decompressed: 5032 Downloaded: 5263 file(s) [attempted 5263/8459 = 62%, 128 KB/s], Decompressed: 5032 Downloaded: 5302 file(s) [attempted 5302/8459 = 62%, 403 KB/s], Decompressed: 5155 Downloaded: 5347 file(s) [attempted 5347/8459 = 63%, 716 KB/s], Decompressed: 5155 Downloaded: 5391 file(s) [attempted 5391/8459 = 63%, 77 KB/s], Decompressed: 5279 Downloaded: 5433 file(s) [attempted 5433/8459 = 64%, 161 KB/s], Decompressed: 5279 Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 288 KB/s], Decompressed: 5279 Downloaded: 5515 file(s) [attempted 5515/8459 = 65%, 449 KB/s], Decompressed: 5388 Downloaded: 5556 file(s) [attempted 5556/8459 = 65%, 180 KB/s], Decompressed: 5388 Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 89 KB/s], Decompressed: 5388 Downloaded: 5636 file(s) [attempted 5636/8459 = 66%, 170 KB/s], Decompressed: 5498 Downloaded: 5675 file(s) [attempted 5675/8459 = 67%, 72 KB/s], Decompressed: 5498 Downloaded: 5723 file(s) [attempted 5723/8459 = 67%, 222 KB/s], Decompressed: 5498 Downloaded: 5771 file(s) [attempted 5771/8459 = 68%, 470 KB/s], Decompressed: 5610 Downloaded: 5810 file(s) [attempted 5810/8459 = 68%, 821 KB/s], Decompressed: 5610 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 875 KB/s], Decompressed: 5727 Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 446 KB/s], Decompressed: 5727 Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 139 KB/s], Decompressed: 5727 Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 290 KB/s], Decompressed: 5850 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 269 KB/s], Decompressed: 5850 Downloaded: 6072 file(s) [attempted 6072/8459 = 71%, 361 KB/s], Decompressed: 5850 Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 1187 KB/s], Decompressed: 5973 Downloaded: 6151 file(s) [attempted 6151/8459 = 72%, 394 KB/s], Decompressed: 5973 Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 484 KB/s], Decompressed: 5973 Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 148 KB/s], Decompressed: 6095 Downloaded: 6274 file(s) [attempted 6274/8459 = 74%, 106 KB/s], Decompressed: 6095 Downloaded: 6319 file(s) [attempted 6319/8459 = 74%, 1049 KB/s], Decompressed: 6095 Downloaded: 6363 file(s) [attempted 6363/8459 = 75%, 231 KB/s], Decompressed: 6223 Downloaded: 6398 file(s) [attempted 6398/8459 = 75%, 35 KB/s], Decompressed: 6223 Downloaded: 6435 file(s) [attempted 6435/8459 = 76%, 134 KB/s], Decompressed: 6223 Downloaded: 6478 file(s) [attempted 6478/8459 = 76%, 93 KB/s], Decompressed: 6353 Downloaded: 6517 file(s) [attempted 6517/8459 = 77%, 1685 KB/s], Decompressed: 6353 Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 735 KB/s], Decompressed: 6353 Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 99 KB/s], Decompressed: 6476 Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 101 KB/s], Decompressed: 6476 Downloaded: 6678 file(s) [attempted 6678/8459 = 78%, 101 KB/s], Decompressed: 6476 Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 176 KB/s], Decompressed: 6582 Downloaded: 6767 file(s) [attempted 6767/8459 = 79%, 458 KB/s], Decompressed: 6582 Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 1052 KB/s], Decompressed: 6688 Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 471 KB/s], Decompressed: 6688 Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 894 KB/s], Decompressed: 6688 Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 283 KB/s], Decompressed: 6798 Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 562 KB/s], Decompressed: 6798 Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 117 KB/s], Decompressed: 6798 Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 89 KB/s], Decompressed: 6798 Downloaded: 7109 file(s) [attempted 7109/8459 = 84%, 760 KB/s], Decompressed: 6921 Downloaded: 7154 file(s) [attempted 7154/8459 = 84%, 110 KB/s], Decompressed: 6921 Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 58 KB/s], Decompressed: 6921 Downloaded: 7229 file(s) [attempted 7229/8459 = 85%, 323 KB/s], Decompressed: 6921 Downloaded: 7270 file(s) [attempted 7270/8459 = 85%, 807 KB/s], Decompressed: 7092 Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 192 KB/s], Decompressed: 7092 Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 258 KB/s], Decompressed: 7092 Downloaded: 7400 file(s) [attempted 7400/8459 = 87%, 976 KB/s], Decompressed: 7092 Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 87 KB/s], Decompressed: 7263 Downloaded: 7488 file(s) [attempted 7488/8459 = 88%, 404 KB/s], Decompressed: 7263 Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 544 KB/s], Decompressed: 7263 Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 1356 KB/s], Decompressed: 7263 Downloaded: 7612 file(s) [attempted 7612/8459 = 89%, 226 KB/s], Decompressed: 7425 Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 221 KB/s], Decompressed: 7425 Downloaded: 7691 file(s) [attempted 7691/8459 = 90%, 998 KB/s], Decompressed: 7425 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 28 KB/s], Decompressed: 7425 Downloaded: 7780 file(s) [attempted 7780/8459 = 91%, 325 KB/s], Decompressed: 7589 Downloaded: 7821 file(s) [attempted 7821/8459 = 92%, 146 KB/s], Decompressed: 7589 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 53 KB/s], Decompressed: 7589 Downloaded: 7903 file(s) [attempted 7903/8459 = 93%, 80 KB/s], Decompressed: 7589 Downloaded: 7944 file(s) [attempted 7944/8459 = 93%, 1053 KB/s], Decompressed: 7589 Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 1728 KB/s], Decompressed: 7770 Downloaded: 8027 file(s) [attempted 8027/8459 = 94%, 1992 KB/s], Decompressed: 7770 Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 835 KB/s], Decompressed: 7770 Downloaded: 8105 file(s) [attempted 8105/8459 = 95%, 894 KB/s], Decompressed: 7770 Downloaded: 8146 file(s) [attempted 8146/8459 = 96%, 637 KB/s], Decompressed: 7965 Downloaded: 8187 file(s) [attempted 8187/8459 = 96%, 78 KB/s], Decompressed: 7965 Downloaded: 8228 file(s) [attempted 8228/8459 = 97%, 595 KB/s], Decompressed: 7965 Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 559 KB/s], Decompressed: 7965 Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 168 KB/s], Decompressed: 7965 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 423 KB/s], Decompressed: 8140 Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 99 KB/s], Decompressed: 8140 Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 319 KB/s], Decompressed: 8140 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 319 KB/s], Decompressed: 8140 apx-runtime-resource-v1 apx-verifier-job-1548-runtime-lake_cache-959654-1785590159595142248-0 3215360 3743744 21474836480 0 0 0 0 0 0 4270850048 5256437760 21474836480 0 0 0 0 0 0
lean_checkerexit 0
lake build
✔ [1/4] Built Iut.Foundations.Species (476ms)
✔ [753/760] Built Iut.Foundations.RealLineCopy (26s)
✔ [754/760] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [755/760] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [756/760] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [757/760] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [758/760] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [759/761] Built Iut.Foundations.QualitativeData (2.3s)
✔ [3504/3507] Built Iut.Foundations.EtaleThetaQuotient (34s)
✔ [3506/3516] Built Iut.Foundations.Orbicurve (31s)
✔ [3953/3956] Built Iut.Foundations.InitialThetaData (27s)
✔ [3962/3968] Built Iut.Foundations.OrbicurvePullback (3.9s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (4.4s)
✔ [3967/3973] Built Iut.Foundations.SourceInitialThetaData (37s)
✔ [4109/4118] Built Iut.Foundations.SourceSemiGraph (2.1s)
✔ [4110/4119] Built Iut.Foundations.SourceSemiGraphAction (2.4s)
✔ [4112/4119] Built Iut.Foundations.SourceSemiGraphOfSubgroups (2.4s)
✔ [4116/4119] Built Iut.Foundations.SourceProfiniteCosetSystem (3.0s)
✔ [4117/4119] Built Iut.Foundations.SourceProfiniteSemiGraphSystem (76s)
✔ [4118/4119] Built Iut.Foundations.SourceInitialThetaDefinition (9.5s)
✔ [4152/4156] Built Iut.Foundations.KummerFaithfulness (2.1s)
✔ [4153/4157] Built Iut.Foundations.SourceTemperedSemigraph (5.3s)
✔ [4154/4158] Built Iut.Foundations.SourceMonoThetaEnvironment (7.8s)
✔ [4156/4168] Built Iut.Foundations.ContinuousH1 (6.5s)
✔ [4164/4172] Built Iut.Foundations.Procession (2.5s)
✔ [4168/4172] Built Iut.Foundations.SourceMLFKummerFaithfulness (2.0s)
✔ [4169/4172] Built Iut.Foundations.Frobenioid (6.1s)
✔ [4170/4172] Built Iut.Foundations.SourceThetaHodgeTheater (19s)
✔ [4171/4179] Built Iut.Foundations.SourceProcession (7.4s)
✔ [4187/4206] Built Iut.Foundations.SourceModelFrobenioid (5.4s)
✔ [4190/4207] Built Iut.Foundations.SourceAutHolomorphic (2.8s)
⚠ [4193/4210] 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`
✔ [4196/4212] Built Iut.Foundations.SourceTopologicalActionPairCategory (3.3s)
✔ [4197/4212] Built Iut.Foundations.SourceConjugateSynchronization (3.9s)
✔ [4198/4212] Built Iut.Foundations.SourceThetaSplitting (6.4s)
✔ [4199/4212] Built Iut.Foundations.SourceSplitKummerFrobenioid (7.6s)
✔ [4203/4212] Built Iut.Foundations.SourceHodgeArakelovEvaluation (3.9s)
✔ [4204/4212] Built Iut.Foundations.SourceArchimedeanKummerSystem (5.6s)
✔ [4206/4219] Built Iut.Foundations.SourceTimesMuPrimeStrip (9.8s)
✔ [4208/4219] Built Iut.Foundations.SourceTimesMuPrimeStripIsomorphism (15s)
✔ [4209/4220] Built Iut.Foundations.SourceArchimedeanSemiGerm (2.9s)
✔ [4211/4220] Built Iut.Foundations.SourceFThetaBridge (3.9s)
✔ [4212/4220] Built Iut.Foundations.SourceTopologicalPseudoMonoid (4.7s)
✔ [4213/4221] Built Iut.Foundations.SourceTimesMuPrimeStripFullPolyIsomorphism (8.3s)
✔ [4216/4222] Built Iut.Foundations.SourceTimesMuReconstructionAlgorithm (7.0s)
✔ [4221/4227] Built Iut.Foundations.SourceAutHolomorphicRigidity (2.7s)
⚠ [4255/4261] 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 `⊢`!
✔ [4256/4261] Built Iut.Foundations.SourceFiniteLocalMLFComparison (10s)
✔ [4257/4264] Built Iut.Foundations.SourceDefinition52LocalReconstruction (27s)
✔ [4258/4270] Built Iut.Foundations.SourceDefinition52LocalContinuity (14s)
✔ [4260/4270] Built Iut.Foundations.SourceDefinition52LocalJointContinuity (4.0s)
✔ [4263/4270] Built Iut.Foundations.SourceAnabelioid (4.3s)
✔ [4264/4272] Built Iut.Foundations.SourceDefinition52IndSystem (9.7s)
✔ [4271/4278] Built Iut.Foundations.SourceDefinition52Sequential (7.0s)
✔ [4273/4289] Built Iut.Foundations.SourcePrimeStripConstructions (4.0s)
✔ [4280/4289] Built Iut.Foundations.SourceAnabelioidEquivalence (2.9s)
✔ [4282/4289] Built Iut.Foundations.SourceContinuousAnabelioid (4.7s)
✔ [4283/4289] Built Iut.Foundations.SourceFiberFunctorComparison (2.5s)
✔ [4284/4310] Built Iut.Foundations.SourceAnabelioidSlice (18s)
✔ [4286/4337] Built Iut.Foundations.SourceAnabelioidComponents (7.8s)
✔ [4288/4337] Built Iut.Foundations.SourceKernelOrbit (4.5s)
✔ [4289/4337] Built Iut.Foundations.SourceSemiGraphOfAnabelioids (3.0s)
✔ [4290/4337] Built Iut.Foundations.ThetaHodgeTheater (6.0s)
✔ [4291/4337] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [4292/4337] Built Iut.SourceTrace.M1M3PaperLedger (9.3s)
✔ [4293/4337] Built Iut.Stage1.PilotComparison (1.6s)
✔ [4294/4337] Built Iut.Foundations.SourceConnectedAnabelioidSlice (3.9s)
✔ [4296/4337] Built Iut.Foundations.SourceVerticalLogLink (5.7s)
✔ [4297/4337] Built Iut.Foundations.SourceTheorem311Horizontal (11s)
✔ [4299/4337] Built Iut.Stage1.IUTStage1HodgeTheaterSource (3.1s)
✔ [4300/4337] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [4301/4337] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4303/4337] Built Iut.Foundations.SourceTheorem311Assembly (7.4s)
✔ [4304/4337] Built Iut.Stage1.CorollarySchema (2.8s)
✔ [4305/4337] Built Iut.Foundations.SourceAnabelioidGrothendieck (3.7s)
✔ [4307/4337] Built Iut.Stage1.SourceObligations (2.0s)
✔ [4308/4337] Built Iut.Foundations.SourceConnectedCoveringCategory (3.3s)
✔ [4309/4337] Built Iut.Stage1.IUTSourceScaffold (2.5s)
✔ [4310/4337] Built Iut.Foundations.SourceTemperoid (4.0s)
✔ [4311/4337] Built Iut.Foundations.SourceConnectedCoveringQuotient (6.5s)
✔ [4312/4337] Built Iut.Stage1.IUTStage1Data (3.3s)
✔ [4313/4337] Built Iut.Foundations.SourceTemperoidQuotient (6.2s)
✔ [4314/4337] Built Iut.Foundations.SourceFiniteLocalCoveringCategory (3.5s)
⚠ [4315/4337] Built Iut.Stage1.IUTStage1SourceCore (78s)
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 `⊢`!
✔ [4316/4337] Built Iut.Stage1.IUTStage1Remark312Absorption (2.7s)
⚠ [4317/4337] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
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`
✔ [4318/4337] Built Iut.Stage1.IUTStage1FiniteLabels (4.4s)
⚠ [4319/4337] Built Iut.Stage1.IUTStage1StepX (5.5s)
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`
✔ [4320/4337] Built Iut.Stage1.IUTStage1Gaussian (8.0s)
✔ [4321/4337] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
✔ [4322/4337] Built Iut.Stage1.IUTStage1HodgeArakelovPilots (6.4s)
⚠ [4323/4337] Built Iut.Stage1.IUTStage1Theorem311 (24s)
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`
✔ [4324/4337] Built Iut.Stage1.IUTStage1ConstructedTheorem311 (8.9s)
ℹ [4325/4337] Built Iut.Stage1.IUTStage1StepXI.Core (715s)
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) [0x7a7c651c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7a7c651bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7a7c651bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7a7c650eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7a7c650ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7a7c651caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7a7c65032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7a7c65032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7a7c65033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7a7c650341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7a7c651c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7a7c64e15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a7c651c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a7c651c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7a7c6519b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7a7c64e15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7a7c60222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7a7c6000cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7a7c5fb69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7a7c5fb69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7a7c5ca4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7a7c5ca45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x630de69c08da]
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) [0x7a7c651c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7a7c651bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7a7c651bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7a7c650f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7a7c650f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7a7c651caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7a7c65032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7a7c65032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7a7c65033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7a7c650341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7a7c651c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7a7c64e15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a7c651c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a7c651c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7a7c6519b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7a7c64e15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7a7c60222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7a7c6000cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7a7c5fb69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7a7c5fb69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7a7c5ca4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7a7c5ca45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x630de69c08da]
✔ [4326/4337] Built Iut.Stage1.IUTStage1StepXI (83s)
ℹ [4327/4337] Built Iut.Stage1.IUTStage1FrobenioidShift (225s)
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) [0x7a9c8cfc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7a9c8cfbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7a9c8cfbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7a9c8cef3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7a9c8cef4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7a9c8cfcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7a9c8ce32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7a9c8ce32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7a9c8ce33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7a9c8ce341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7a9c8cfc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7a9c8cc15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a9c8cfc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7a9c8cfc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7a9c8cf9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7a9c8cc15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7a9c88022638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7a9c87e0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7a9c87969a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7a9c87969f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7a9c8484524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7a9c84845305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x620240daf8da]
✔ [4328/4337] Built Iut.Stage1.IUTStage1EndpointAudit (3.6s)
✔ [4329/4337] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [4330/4337] Built Iut.Stage1.IUTStage1Experiments.Diagnostics (46s)
✔ [4331/4337] Built Iut.Stage1.IUTStage1Experiments.ClosedEndpoints (4.4s)
⚠ [4332/4337] Built Iut.Stage1.IUTStage1Experiments.AdditiveHaar (165s)
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) [0x7ca0c35c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7ca0c35bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7ca0c35bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7ca0c34eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7ca0c34ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7ca0c35caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7ca0c3432923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7ca0c3432b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7ca0c3433827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7ca0c34341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7ca0c35c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7ca0c3215adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ca0c35c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ca0c35c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7ca0c359b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7ca0c3215c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7ca0be622638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7ca0be40cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7ca0bdf69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7ca0bdf69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7ca0bae4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7ca0bae45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x59c5e8d428da]
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) [0x7ca0c35c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7ca0c35bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7ca0c35bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7ca0c34f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7ca0c34f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7ca0c35caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7ca0c3432923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7ca0c3432b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7ca0c3433827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7ca0c34341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7ca0c35c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7ca0c3215adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ca0c35c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7ca0c35c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7ca0c359b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7ca0c3215c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7ca0be622638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7ca0be40cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7ca0bdf69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7ca0bdf69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7ca0bae4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7ca0bae45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x59c5e8d428da]
✔ [4333/4337] Built Iut.Stage1.IUTStage1StepXI.AdditiveHaarBridge (10s)
ℹ [4334/4337] Built Iut.Stage1.IUTStage1StepXIDependencyAudit (30s)
info: Iut/Stage1/IUTStage1StepXIDependencyAudit.lean:3961:0: 'Iut.Stage1.IUTStage1SourcePackage.IUTStage1Theorem311HullDetSourceConstructor.IUTStage1Theorem311OneSidedMultiradialConstructionSource.IUTStage1ConcreteTheorem311PrimitiveSourcePacket.ofSourceSpineDataOneSidedComponentSHECodomainSelectedLabelQPilotBridgeAlignmentOutputFlagCalibrationSource_packetConstructionAudit' depends on axioms: [propext,
Classical.choice,
Quot.sound]
✔ [4335/4337] Built Iut.Basic (3.7s)
✔ [4336/4337] Built Iut (3.2s)
Build completed successfully (4337 jobs).
apx-runtime-resource-v1 apx-verifier-job-1548-runtime-lean_checker-959654-1785590241365488734-1 1134592 1384448 21474836480 0 0 0 0 0 0 5472796672 10044440576 21474836480 0 0 0 0 0 0
blueprint_buildexit 1
lake build :blueprint
error: unknown package facet `blueprint` apx-runtime-resource-v1 apx-verifier-job-1548-runtime-blueprint_build-959654-1785592570335440030-2 1052672 1265664 21474836480 0 0 0 0 0 0 109645824 213016576 21474836480 0 0 0 0 0 0
semantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)
.apodeixis/lean-runner/ApodeixisSemanticInternal/RepositorySemanticCore.lean:956:5: warning: unused variable `modulePath` Note: This linter can be disabled with `set_option linter.unusedVariables false`
apx-semantic-phase {"phase":"core_compile","duration_ms":8518}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":149,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8024e416d7e83df815d7d152f1957f9d0b9f83b87a0741b5eca0396d12f02a4f
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":55,"runner_cache_hit":true}
apx-semantic-phase {"cgroup_memory_current_bytes":554606592,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":554610688,"current_rss_bytes":4005236736,"duration_ms":0,"environment_module_count":5652,"peak_rss_bytes":4005236736,"phase":"lean_environment_ready","target_module_count":5}
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"duration_ms":0,"measurement_complete":true,"missing_module_count":0,"phase":"lean_olean_footprint","resolution_source":"env_header_findOLean","resolved_module_count":5650,"resolved_olean_bytes":1243094552,"target_module_count":5,"unique_olean_file_count":5650,"unmeasured_olean_file_count":0}
apx-semantic-phase {"duration_ms":32276,"module_count":5,"ok":true,"phase":"lean_module_facts","target_module_count":5}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":600834048,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4013002752,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceConnectedCoveringCategory","module_path":"Iut/Foundations/SourceConnectedCoveringCategory.lean","payload_bytes":0,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":16,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":480,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":594661376,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":895,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":2670,"current_rss_bytes":4009472000,"declaration_count":16,"diagnostic_count":5,"duration_ms":0,"last_completed_declaration":"Iut.sourceConnectedContinuousAction","last_completed_ordinal":16,"module_name":"Iut.Foundations.SourceConnectedCoveringCategory","module_path":"Iut/Foundations/SourceConnectedCoveringCategory.lean","payload_bytes":1915917,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":16,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":1377,"total_declaration_count":16,"type_rendering_ms":1291}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":1918436,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":1918436,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":594644992,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"current_rss_bytes":4009472000,"declaration_count":16,"declaration_writer":"direct_fields","diagnostic_count":5,"duration_ms":2705,"module_index":0,"module_name":"Iut.Foundations.SourceConnectedCoveringCategory","module_path":"Iut/Foundations/SourceConnectedCoveringCategory.lean","module_payload_kind":"fragment","payload_bytes":1918436,"peak_rss_bytes":4016103424,"phase":"lean_module_fragment_stream","processed_declaration_count":16}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":594907136,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4009537536,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceConnectedCoveringQuotient","module_path":"Iut/Foundations/SourceConnectedCoveringQuotient.lean","payload_bytes":0,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":50,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":968,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":603168768,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":6242,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":14468,"current_rss_bytes":4009463808,"declaration_count":32,"diagnostic_count":12,"duration_ms":0,"last_completed_declaration":"Iut.SourceActionKernelQuotient.fiberMap_smul","last_completed_ordinal":32,"module_name":"Iut.Foundations.SourceConnectedCoveringQuotient","module_path":"Iut/Foundations/SourceConnectedCoveringQuotient.lean","payload_bytes":10236833,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":32,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":3,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":7217,"total_declaration_count":50,"type_rendering_ms":7249}
apx-semantic-phase {"binder_summary_ms":1346,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":606760960,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":8621,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":19963,"current_rss_bytes":4009455616,"declaration_count":50,"diagnostic_count":19,"duration_ms":0,"last_completed_declaration":"Iut.SourceActionKernelQuotient.smul_mk","last_completed_ordinal":50,"module_name":"Iut.Foundations.SourceConnectedCoveringQuotient","module_path":"Iut/Foundations/SourceConnectedCoveringQuotient.lean","payload_bytes":14064751,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":50,"reference_collection_ms":0,"shape_profile_count":1,"shape_profiling_ms":7,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":9978,"total_declaration_count":50,"type_rendering_ms":9983}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":1,"module_payload_kind":"fragment","payload_bytes":14073792,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":1,"module_payload_kind":"fragment","payload_bytes":14073792,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":606474240,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"current_rss_bytes":4009410560,"declaration_count":50,"declaration_writer":"direct_fields","diagnostic_count":19,"duration_ms":20056,"module_index":1,"module_name":"Iut.Foundations.SourceConnectedCoveringQuotient","module_path":"Iut/Foundations/SourceConnectedCoveringQuotient.lean","module_payload_kind":"fragment","payload_bytes":14073792,"peak_rss_bytes":4016103424,"phase":"lean_module_fragment_stream","processed_declaration_count":50}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":606474240,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4009472000,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceKernelOrbit","module_path":"Iut/Foundations/SourceKernelOrbit.lean","payload_bytes":0,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":14,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":194,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":606543872,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":126,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":534,"current_rss_bytes":4009431040,"declaration_count":14,"diagnostic_count":5,"duration_ms":0,"last_completed_declaration":"Iut.SourceKernelOrbit.targetContinuous","last_completed_ordinal":14,"module_name":"Iut.Foundations.SourceKernelOrbit","module_path":"Iut/Foundations/SourceKernelOrbit.lean","payload_bytes":207559,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":14,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":320,"total_declaration_count":14,"type_rendering_ms":214}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":2,"module_payload_kind":"fragment","payload_bytes":209858,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":2,"module_payload_kind":"fragment","payload_bytes":209858,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":606535680,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"current_rss_bytes":4009431040,"declaration_count":14,"declaration_writer":"direct_fields","diagnostic_count":5,"duration_ms":560,"module_index":2,"module_name":"Iut.Foundations.SourceKernelOrbit","module_path":"Iut/Foundations/SourceKernelOrbit.lean","module_payload_kind":"fragment","payload_bytes":209858,"peak_rss_bytes":4016103424,"phase":"lean_module_fragment_stream","processed_declaration_count":14}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":606797824,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4009472000,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceTemperoid","module_path":"Iut/Foundations/SourceTemperoid.lean","payload_bytes":0,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":52,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":212,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":609886208,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610496512,"conclusion_summary_ms":1609,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":3844,"current_rss_bytes":4009488384,"declaration_count":32,"diagnostic_count":11,"duration_ms":0,"last_completed_declaration":"Iut.SourceCountableTypeCatDiscrete.instHasForget₂SourceCountableTypeCatFunObjCountableTopCatContinuousMapCarrier._proof_4","last_completed_ordinal":32,"module_name":"Iut.Foundations.SourceTemperoid","module_path":"Iut/Foundations/SourceTemperoid.lean","payload_bytes":2790784,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":32,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":1,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":1822,"total_declaration_count":52,"type_rendering_ms":2022}
apx-semantic-phase {"binder_summary_ms":238,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":610762752,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610824192,"conclusion_summary_ms":2207,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":5100,"current_rss_bytes":4009570304,"declaration_count":52,"diagnostic_count":19,"duration_ms":0,"last_completed_declaration":"Iut.sourceConnectedTemperoidAction","last_completed_ordinal":52,"module_name":"Iut.Foundations.SourceTemperoid","module_path":"Iut/Foundations/SourceTemperoid.lean","payload_bytes":3689561,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":52,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":1,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":2449,"total_declaration_count":52,"type_rendering_ms":2651}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":3,"module_payload_kind":"fragment","payload_bytes":3699182,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":3,"module_payload_kind":"fragment","payload_bytes":3699182,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":610746368,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":610824192,"current_rss_bytes":4009574400,"declaration_count":52,"declaration_writer":"direct_fields","diagnostic_count":19,"duration_ms":5177,"module_index":3,"module_name":"Iut.Foundations.SourceTemperoid","module_path":"Iut/Foundations/SourceTemperoid.lean","module_payload_kind":"fragment","payload_bytes":3699182,"peak_rss_bytes":4016103424,"phase":"lean_module_fragment_stream","processed_declaration_count":52}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611069952,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":611270656,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4009902080,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":0,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":134,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":50,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611151872,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":611270656,"conclusion_summary_ms":307,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":382,"current_rss_bytes":4009906176,"declaration_count":32,"diagnostic_count":25,"duration_ms":0,"last_completed_declaration":"Iut.SourceTrace.PaperClause.gap","last_completed_ordinal":32,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":37327,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":32,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":2,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":361,"total_declaration_count":134,"type_rendering_ms":21}
apx-semantic-phase {"binder_summary_ms":96,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611471360,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":611504128,"conclusion_summary_ms":441,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":619,"current_rss_bytes":4009934848,"declaration_count":64,"diagnostic_count":47,"duration_ms":0,"last_completed_declaration":"Iut.SourceTrace.PaperSourceDocument.sha256","last_completed_ordinal":64,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":86268,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":64,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":3,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":543,"total_declaration_count":134,"type_rendering_ms":76}
apx-semantic-phase {"binder_summary_ms":356,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611180544,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":611516416,"conclusion_summary_ms":797,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":1265,"current_rss_bytes":4009934848,"declaration_count":96,"diagnostic_count":69,"duration_ms":0,"last_completed_declaration":"Iut.SourceTrace.PaperVolume.iutIII.sizeOf_spec","last_completed_ordinal":96,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":122667,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":96,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":4,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":1162,"total_declaration_count":134,"type_rendering_ms":103}
apx-semantic-phase {"binder_summary_ms":609,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611942400,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":612093952,"conclusion_summary_ms":1092,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":1860,"current_rss_bytes":4010827776,"declaration_count":128,"diagnostic_count":84,"duration_ms":0,"last_completed_declaration":"Iut.SourceTrace.m1m3SourceDocuments_count","last_completed_ordinal":128,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":404866,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":128,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":7,"source_excerpt_ms":5,"statement_alias_ms":0,"statement_summary_ms":1716,"total_declaration_count":134,"type_rendering_ms":139}
apx-semantic-phase {"binder_summary_ms":612,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":611975168,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":612093952,"conclusion_summary_ms":1111,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":1897,"current_rss_bytes":4010827776,"declaration_count":134,"diagnostic_count":84,"duration_ms":0,"last_completed_declaration":"_private.Iut.SourceTrace.M1M3PaperLedger.0.Iut.SourceTrace.clause","last_completed_ordinal":134,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","payload_bytes":414676,"peak_rss_bytes":4016103424,"phase":"lean_declaration_progress","processed_declaration_count":134,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":7,"source_excerpt_ms":5,"statement_alias_ms":0,"statement_summary_ms":1741,"total_declaration_count":134,"type_rendering_ms":151}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":4,"module_payload_kind":"fragment","payload_bytes":451583,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":4,"module_payload_kind":"fragment","payload_bytes":451583,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":611934208,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":612093952,"current_rss_bytes":4010868736,"declaration_count":134,"declaration_writer":"direct_fields","diagnostic_count":84,"duration_ms":2201,"module_index":4,"module_name":"Iut.SourceTrace.M1M3PaperLedger","module_path":"Iut/SourceTrace/M1M3PaperLedger.lean","module_payload_kind":"fragment","payload_bytes":451583,"peak_rss_bytes":4016103424,"phase":"lean_module_fragment_stream","processed_declaration_count":134}
apx-semantic-phase {"current_rss_bytes":4010868736,"current_rss_kib":3916864,"duration_ms":0,"measurement_available":true,"measurement_scope":"target_lean_process","measurement_source":"proc_self_status_vmhwm","peak_rss_bytes":4016103424,"peak_rss_kib":3921976,"phase":"lean_process_resources"}
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":66625,"ok":true}
apx-semantic-phase {"phase":"semantic_command_cgroup_memory","duration_ms":0,"measurement_available":true,"measurement_scope":"visible_cgroup","cgroup_version":2,"cgroup_memory_current_bytes":93597696,"cgroup_memory_peak_bytes":614805504,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_max_unlimited":false}
apx-runtime-resource-v1 apx-verifier-job-1548-runtime-semantic_extract-959654-1785597247548264421-3 1019904 1531904 21474836480 0 0 0 0 0 0 93216768 614805504 21474836480 0 0 0 0 0 0
podman cleanup verified verifier container apx-verifier-job-1548-runtime-semantic_extract-959654-1785597247548264421-3 is absent after command completionsemantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":102,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8024e416d7e83df815d7d152f1957f9d0b9f83b87a0741b5eca0396d12f02a4f
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":18,"runner_cache_hit":true}
apx-semantic-phase {"cgroup_memory_current_bytes":539000832,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":539000832,"current_rss_bytes":4355641344,"duration_ms":0,"environment_module_count":6114,"peak_rss_bytes":4355641344,"phase":"lean_environment_ready","target_module_count":2}
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"duration_ms":0,"measurement_complete":true,"missing_module_count":0,"phase":"lean_olean_footprint","resolution_source":"env_header_findOLean","resolved_module_count":6112,"resolved_olean_bytes":1383921160,"target_module_count":2,"unique_olean_file_count":6112,"unmeasured_olean_file_count":0}
apx-semantic-phase {"duration_ms":21884,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":558641152,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":568950784,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4363423744,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceFiniteLocalCoveringCategory","module_path":"Iut/Foundations/SourceFiniteLocalCoveringCategory.lean","payload_bytes":0,"peak_rss_bytes":4366053376,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":26,"type_rendering_ms":0}
apx-semantic-phase {"cgroup_memory_current_bytes":573407232,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575397888,"complete":false,"current_rss_bytes":4360716288,"declaration_name":"Iut.SourceThetaFiniteLocalCoreData.xCoverActionEquivalence","duration_ms":1378,"emitted_bytes":983040,"field":"statement_summary.conclusion_summary.type_text","limit_bytes":1048562,"module_name":"Iut.Foundations.SourceFiniteLocalCoveringCategory","module_path":"Iut/Foundations/SourceFiniteLocalCoveringCategory.lean","peak_rss_bytes":4366053376,"phase":"lean_declaration_field_progress"}
apx-semantic-phase {"binder_summary_ms":376,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":573202432,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575397888,"conclusion_summary_ms":9232,"conclusion_summary_omitted_count":1,"cumulative_extraction_ms":31521,"current_rss_bytes":4360675328,"declaration_count":26,"diagnostic_count":6,"duration_ms":0,"last_completed_declaration":"Iut.SourceThetaFiniteLocalCoreData.xLocalExactSequence._proof_3","last_completed_ordinal":26,"module_name":"Iut.Foundations.SourceFiniteLocalCoveringCategory","module_path":"Iut/Foundations/SourceFiniteLocalCoveringCategory.lean","payload_bytes":23847967,"peak_rss_bytes":4366053376,"phase":"lean_declaration_progress","processed_declaration_count":26,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":1,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":9609,"total_declaration_count":26,"type_rendering_ms":21910}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":23851080,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":23851080,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":573190144,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575397888,"current_rss_bytes":4360683520,"declaration_count":26,"declaration_writer":"direct_fields","diagnostic_count":6,"duration_ms":31583,"module_index":0,"module_name":"Iut.Foundations.SourceFiniteLocalCoveringCategory","module_path":"Iut/Foundations/SourceFiniteLocalCoveringCategory.lean","module_payload_kind":"fragment","payload_bytes":23851080,"peak_rss_bytes":4366053376,"phase":"lean_module_fragment_stream","processed_declaration_count":26}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":573190144,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575397888,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4360781824,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Foundations.SourceTemperoidQuotient","module_path":"Iut/Foundations/SourceTemperoidQuotient.lean","payload_bytes":0,"peak_rss_bytes":4366053376,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":49,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":393,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":553541632,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575848448,"conclusion_summary_ms":2653,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":6507,"current_rss_bytes":4360699904,"declaration_count":32,"diagnostic_count":11,"duration_ms":0,"last_completed_declaration":"Iut.SourceTemperoidKernelQuotient.fiberMap_smul","last_completed_ordinal":32,"module_name":"Iut.Foundations.SourceTemperoidQuotient","module_path":"Iut/Foundations/SourceTemperoidQuotient.lean","payload_bytes":4790040,"peak_rss_bytes":4366053376,"phase":"lean_declaration_progress","processed_declaration_count":32,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":3047,"total_declaration_count":49,"type_rendering_ms":3458}
apx-semantic-phase {"binder_summary_ms":485,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":555696128,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575848448,"conclusion_summary_ms":3806,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":9187,"current_rss_bytes":4360732672,"declaration_count":49,"diagnostic_count":17,"duration_ms":0,"last_completed_declaration":"Iut.SourceTemperoidKernelQuotient.smul_mk","last_completed_ordinal":49,"module_name":"Iut.Foundations.SourceTemperoidQuotient","module_path":"Iut/Foundations/SourceTemperoidQuotient.lean","payload_bytes":6814120,"peak_rss_bytes":4366053376,"phase":"lean_declaration_progress","processed_declaration_count":49,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":2,"statement_alias_ms":0,"statement_summary_ms":4293,"total_declaration_count":49,"type_rendering_ms":4892}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":1,"module_payload_kind":"fragment","payload_bytes":6822157,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":1,"module_payload_kind":"fragment","payload_bytes":6822157,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":555593728,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":575848448,"current_rss_bytes":4360740864,"declaration_count":49,"declaration_writer":"direct_fields","diagnostic_count":17,"duration_ms":9298,"module_index":1,"module_name":"Iut.Foundations.SourceTemperoidQuotient","module_path":"Iut/Foundations/SourceTemperoidQuotient.lean","module_payload_kind":"fragment","payload_bytes":6822157,"peak_rss_bytes":4366053376,"phase":"lean_module_fragment_stream","processed_declaration_count":49}
apx-semantic-phase {"current_rss_bytes":4360740864,"current_rss_kib":4258536,"duration_ms":0,"measurement_available":true,"measurement_scope":"target_lean_process","measurement_source":"proc_self_status_vmhwm","peak_rss_bytes":4366053376,"peak_rss_kib":4263724,"phase":"lean_process_resources"}
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":66490,"ok":true}
apx-semantic-phase {"phase":"semantic_command_cgroup_memory","duration_ms":0,"measurement_available":true,"measurement_scope":"visible_cgroup","cgroup_version":2,"cgroup_memory_current_bytes":16969728,"cgroup_memory_peak_bytes":575848448,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_max_unlimited":false}
apx-runtime-resource-v1 apx-verifier-job-1548-runtime-semantic_extract-959654-1785597325639599082-4 892928 1404928 21474836480 0 0 0 0 0 0 16666624 575848448 21474836480 0 0 0 0 0 0
podman cleanup verified verifier container apx-verifier-job-1548-runtime-semantic_extract-959654-1785597325639599082-4 is absent after command completionsemantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":97,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8024e416d7e83df815d7d152f1957f9d0b9f83b87a0741b5eca0396d12f02a4f
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":true}
apx-semantic-phase {"cgroup_memory_current_bytes":578314240,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":578314240,"current_rss_bytes":4973244416,"duration_ms":0,"environment_module_count":6464,"peak_rss_bytes":4973244416,"phase":"lean_environment_ready","target_module_count":1}
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"duration_ms":0,"measurement_complete":true,"missing_module_count":0,"phase":"lean_olean_footprint","resolution_source":"env_header_findOLean","resolved_module_count":6462,"resolved_olean_bytes":2009688152,"target_module_count":1,"unique_olean_file_count":6462,"unmeasured_olean_file_count":0}
apx-semantic-phase {"duration_ms":19423,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":621481984,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":632307712,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4979130368,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","payload_bytes":0,"peak_rss_bytes":4981686272,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":1,"type_rendering_ms":0}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":621740032,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":632307712,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4979982336,"declaration_count":1,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":"Iut.projectName","last_completed_ordinal":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","payload_bytes":1003,"peak_rss_bytes":4981686272,"phase":"lean_declaration_progress","processed_declaration_count":1,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":1,"type_rendering_ms":0}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":1057,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":1057,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":621735936,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":632307712,"current_rss_bytes":4979986432,"declaration_count":1,"declaration_writer":"direct_fields","diagnostic_count":0,"duration_ms":8,"module_index":0,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","module_payload_kind":"fragment","payload_bytes":1057,"peak_rss_bytes":4981686272,"phase":"lean_module_fragment_stream","processed_declaration_count":1}
apx-semantic-phase {"current_rss_bytes":4979986432,"current_rss_kib":4863268,"duration_ms":0,"measurement_available":true,"measurement_scope":"target_lean_process","measurement_source":"proc_self_status_vmhwm","peak_rss_bytes":4981686272,"peak_rss_kib":4864928,"phase":"lean_process_resources"}
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":23570,"ok":true}
apx-semantic-phase {"phase":"semantic_command_cgroup_memory","duration_ms":0,"measurement_available":true,"measurement_scope":"visible_cgroup","cgroup_version":2,"cgroup_memory_current_bytes":34439168,"cgroup_memory_peak_bytes":632307712,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_max_unlimited":false}
apx-runtime-resource-v1 apx-verifier-job-1548-runtime-semantic_extract-959654-1785597393576414997-5 1093632 1343488 21474836480 0 0 0 0 0 0 34070528 632307712 21474836480 0 0 0 0 0 0
podman cleanup verified verifier container apx-verifier-job-1548-runtime-semantic_extract-959654-1785597393576414997-5 is absent after command completionsemantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
apx-semantic-phase {"phase":"core_compile","duration_ms":27}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":122,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8024e416d7e83df815d7d152f1957f9d0b9f83b87a0741b5eca0396d12f02a4f
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":36,"runner_cache_hit":true}
apx-semantic-phase {"cgroup_memory_current_bytes":577511424,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":577974272,"current_rss_bytes":4973932544,"duration_ms":0,"environment_module_count":6465,"peak_rss_bytes":4973932544,"phase":"lean_environment_ready","target_module_count":1}
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"duration_ms":0,"measurement_complete":true,"missing_module_count":0,"phase":"lean_olean_footprint","resolution_source":"env_header_findOLean","resolved_module_count":6463,"resolved_olean_bytes":2009689520,"target_module_count":1,"unique_olean_file_count":6463,"unmeasured_olean_file_count":0}
apx-semantic-phase {"duration_ms":18848,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"binder_summary_ms":0,"binder_summary_omitted_count":0,"cgroup_memory_current_bytes":588894208,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":601812992,"conclusion_summary_ms":0,"conclusion_summary_omitted_count":0,"cumulative_extraction_ms":0,"current_rss_bytes":4981841920,"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"last_completed_declaration":null,"last_completed_ordinal":0,"module_name":"Iut","module_path":"Iut.lean","payload_bytes":0,"peak_rss_bytes":4985180160,"phase":"lean_declaration_progress","processed_declaration_count":0,"reference_collection_ms":0,"shape_profile_count":0,"shape_profiling_ms":0,"source_excerpt_ms":0,"statement_alias_ms":0,"statement_summary_ms":0,"total_declaration_count":0,"type_rendering_ms":0}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":422,"phase":"lean_module_json_serialize","streamed":true}
apx-semantic-phase {"declaration_writer":"direct_fields","duration_ms":0,"module_index":0,"module_payload_kind":"fragment","payload_bytes":422,"phase":"lean_module_json_write","streamed":true}
apx-semantic-phase {"cgroup_memory_current_bytes":588894208,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_peak_bytes":601812992,"current_rss_bytes":4982034432,"declaration_count":0,"declaration_writer":"direct_fields","diagnostic_count":0,"duration_ms":1,"module_index":0,"module_name":"Iut","module_path":"Iut.lean","module_payload_kind":"fragment","payload_bytes":422,"peak_rss_bytes":4985180160,"phase":"lean_module_fragment_stream","processed_declaration_count":0}
apx-semantic-phase {"current_rss_bytes":4982034432,"current_rss_kib":4865268,"duration_ms":0,"measurement_available":true,"measurement_scope":"target_lean_process","measurement_source":"proc_self_status_vmhwm","peak_rss_bytes":4985180160,"peak_rss_kib":4868340,"phase":"lean_process_resources"}
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":22984,"ok":true}
apx-semantic-phase {"phase":"semantic_command_cgroup_memory","duration_ms":0,"measurement_available":true,"measurement_scope":"visible_cgroup","cgroup_version":2,"cgroup_memory_current_bytes":1626112,"cgroup_memory_peak_bytes":601812992,"cgroup_memory_max_bytes":21474836480,"cgroup_memory_max_unlimited":false}
apx-runtime-resource-v1 apx-verifier-job-1548-runtime-semantic_extract-959654-1785597418163435774-6 892928 1400832 21474836480 0 0 0 0 0 0 1290240 601812992 21474836480 0 0 0 0 0 0
podman cleanup verified verifier container apx-verifier-job-1548-runtime-semantic_extract-959654-1785597418163435774-6 is absent after command completion