Run 25

semantic_extract (extract-batch-00085)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00086)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00087)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00088)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00089)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00090)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00091)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00092)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00093)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00094)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00095)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00096)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00097)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00098)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8551 file(s) from leanprover-community/mathlib4 cache
Decompressed 8525 file(s)
Already decompressed 8525 file(s)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '1ccad003f48319848becd773bde09f17729eec3e'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '5dd219c775e402f818b42cd3997b5cf21017babf'
✔ [7/24] Built Cache.Lean (4.1s)
✔ [9/24] Built Batteries.Data.Array.Match:c.o (1.4s)
✔ [10/24] Built Batteries.Data.String.Basic:c.o (114ms)
✔ [11/24] Built Batteries.Data.String.Matcher:c.o (219ms)
✔ [12/24] Built Cache.Lean:c.o (130ms)
✔ [14/24] Built Cache.Init (390ms)
✔ [15/24] Built Cache.IO (1.8s)
✔ [16/24] Built Cache.Init:c.o (97ms)
✔ [17/24] Built Cache.IO:c.o (1.2s)
✔ [18/24] Built Cache.Hashing (984ms)
✔ [19/24] Built Cache.Hashing:c.o (342ms)
✔ [20/24] Built Cache.Requests (2.0s)
✔ [21/24] Built Cache.Requests:c.o (1.8s)
✔ [22/24] Built Cache.Main (1.5s)
✔ [23/24] Built Cache.Main:c.o (504ms)
✔ [24/24] Built cache:exe (6.6s)

Downloaded: 1 file(s) [attempted 1/8551 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8551 = 0%, 4 KB/s], Decompressed: 15
Downloaded: 41 file(s) [attempted 41/8551 = 0%, 14 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8551 = 0%, 25 KB/s], Decompressed: 53
Downloaded: 92 file(s) [attempted 93/8551 = 1%, 231 KB/s], Decompressed: 76
Downloaded: 126 file(s) [attempted 127/8551 = 1%, 160 KB/s], Decompressed: 99
Downloaded: 157 file(s) [attempted 158/8551 = 1%, 77 KB/s], Decompressed: 116
Downloaded: 191 file(s) [attempted 192/8551 = 2%, 557 KB/s], Decompressed: 140
Downloaded: 226 file(s) [attempted 227/8551 = 2%, 843 KB/s], Decompressed: 168
Downloaded: 263 file(s) [attempted 264/8551 = 3%, 252 KB/s], Decompressed: 202
Downloaded: 301 file(s) [attempted 302/8551 = 3%, 301 KB/s], Decompressed: 243
Downloaded: 342 file(s) [attempted 343/8551 = 4%, 37 KB/s], Decompressed: 243
Downloaded: 376 file(s) [attempted 377/8551 = 4%, 99 KB/s], Decompressed: 243
Downloaded: 414 file(s) [attempted 415/8551 = 4%, 224 KB/s], Decompressed: 301
Downloaded: 459 file(s) [attempted 460/8551 = 5%, 1327 KB/s], Decompressed: 301
Downloaded: 496 file(s) [attempted 497/8551 = 5%, 441 KB/s], Decompressed: 383
Downloaded: 537 file(s) [attempted 538/8551 = 6%, 1424 KB/s], Decompressed: 383
Downloaded: 568 file(s) [attempted 569/8551 = 6%, 234 KB/s], Decompressed: 383
Downloaded: 613 file(s) [attempted 614/8551 = 7%, 591 KB/s], Decompressed: 472
Downloaded: 657 file(s) [attempted 658/8551 = 7%, 129 KB/s], Decompressed: 472
Downloaded: 698 file(s) [attempted 699/8551 = 8%, 895 KB/s], Decompressed: 472
Downloaded: 736 file(s) [attempted 737/8551 = 8%, 69 KB/s], Decompressed: 472
Downloaded: 774 file(s) [attempted 775/8551 = 9%, 475 KB/s], Decompressed: 603
Downloaded: 815 file(s) [attempted 816/8551 = 9%, 129 KB/s], Decompressed: 603
Downloaded: 856 file(s) [attempted 857/8551 = 10%, 114 KB/s], Decompressed: 603
Downloaded: 896 file(s) [attempted 898/8551 = 10%, 84 KB/s], Decompressed: 603
Downloaded: 937 file(s) [attempted 939/8551 = 10%, 831 KB/s], Decompressed: 764
Downloaded: 971 file(s) [attempted 973/8551 = 11%, 170 KB/s], Decompressed: 764
Downloaded: 1019 file(s) [attempted 1021/8551 = 11%, 174 KB/s], Decompressed: 764
Downloaded: 1064 file(s) [attempted 1066/8551 = 12%, 343 KB/s], Decompressed: 764
Downloaded: 1102 file(s) [attempted 1104/8551 = 12%, 147 KB/s], Decompressed: 764
Downloaded: 1143 file(s) [attempted 1145/8551 = 13%, 1924 KB/s], Decompressed: 920
Downloaded: 1184 file(s) [attempted 1186/8551 = 13%, 851 KB/s], Decompressed: 920
Downloaded: 1218 file(s) [attempted 1220/8551 = 14%, 104 KB/s], Decompressed: 920
Downloaded: 1262 file(s) [attempted 1264/8551 = 14%, 569 KB/s], Decompressed: 920
Downloaded: 1302 file(s) [attempted 1305/8551 = 15%, 107 KB/s], Decompressed: 920
Downloaded: 1344 file(s) [attempted 1347/8551 = 15%, 145 KB/s], Decompressed: 1105
Downloaded: 1385 file(s) [attempted 1388/8551 = 16%, 739 KB/s], Decompressed: 1105
Downloaded: 1422 file(s) [attempted 1425/8551 = 16%, 232 KB/s], Decompressed: 1105
Downloaded: 1463 file(s) [attempted 1466/8551 = 17%, 172 KB/s], Decompressed: 1105
Downloaded: 1508 file(s) [attempted 1511/8551 = 17%, 196 KB/s], Decompressed: 1105
Downloaded: 1547 file(s) [attempted 1552/8551 = 18%, 339 KB/s], Decompressed: 1105
Downloaded: 1588 file(s) [attempted 1593/8551 = 18%, 260 KB/s], Decompressed: 1105
Downloaded: 1629 file(s) [attempted 1634/8551 = 19%, 201 KB/s], Decompressed: 1333
Downloaded: 1670 file(s) [attempted 1675/8551 = 19%, 58 KB/s], Decompressed: 1333
Downloaded: 1708 file(s) [attempted 1713/8551 = 20%, 227 KB/s], Decompressed: 1333
Downloaded: 1749 file(s) [attempted 1754/8551 = 20%, 252 KB/s], Decompressed: 1333
Downloaded: 1790 file(s) [attempted 1795/8551 = 20%, 258 KB/s], Decompressed: 1333
Downloaded: 1834 file(s) [attempted 1839/8551 = 21%, 155 KB/s], Decompressed: 1333
Downloaded: 1875 file(s) [attempted 1880/8551 = 21%, 1224 KB/s], Decompressed: 1333
Downloaded: 1916 file(s) [attempted 1921/8551 = 22%, 75 KB/s], Decompressed: 1333
Downloaded: 1954 file(s) [attempted 1959/8551 = 22%, 65 KB/s], Decompressed: 1333
Downloaded: 1995 file(s) [attempted 2000/8551 = 23%, 37 KB/s], Decompressed: 1626
Downloaded: 2036 file(s) [attempted 2041/8551 = 23%, 410 KB/s], Decompressed: 1626
Downloaded: 2077 file(s) [attempted 2082/8551 = 24%, 104 KB/s], Decompressed: 1626
Downloaded: 2118 file(s) [attempted 2123/8551 = 24%, 1051 KB/s], Decompressed: 1626
Downloaded: 2160 file(s) [attempted 2165/8551 = 25%, 507 KB/s], Decompressed: 1626
Downloaded: 2201 file(s) [attempted 2206/8551 = 25%, 521 KB/s], Decompressed: 1626
Downloaded: 2242 file(s) [attempted 2247/8551 = 26%, 40 KB/s], Decompressed: 1626
Downloaded: 2283 file(s) [attempted 2288/8551 = 26%, 60 KB/s], Decompressed: 1626
Downloaded: 2317 file(s) [attempted 2322/8551 = 27%, 2080 KB/s], Decompressed: 1626
Downloaded: 2361 file(s) [attempted 2366/8551 = 27%, 163 KB/s], Decompressed: 1626
Downloaded: 2402 file(s) [attempted 2407/8551 = 28%, 728 KB/s], Decompressed: 1626
Downloaded: 2444 file(s) [attempted 2449/8551 = 28%, 394 KB/s], Decompressed: 1975
Downloaded: 2485 file(s) [attempted 2490/8551 = 29%, 241 KB/s], Decompressed: 1975
Downloaded: 2522 file(s) [attempted 2527/8551 = 29%, 357 KB/s], Decompressed: 1975
Downloaded: 2563 file(s) [attempted 2568/8551 = 30%, 180 KB/s], Decompressed: 1975
Downloaded: 2608 file(s) [attempted 2613/8551 = 30%, 440 KB/s], Decompressed: 1975
Downloaded: 2649 file(s) [attempted 2654/8551 = 31%, 868 KB/s], Decompressed: 1975
Downloaded: 2687 file(s) [attempted 2692/8551 = 31%, 266 KB/s], Decompressed: 1975
Downloaded: 2724 file(s) [attempted 2729/8551 = 31%, 1038 KB/s], Decompressed: 1975
Downloaded: 2762 file(s) [attempted 2767/8551 = 32%, 136 KB/s], Decompressed: 1975
Downloaded: 2806 file(s) [attempted 2811/8551 = 32%, 658 KB/s], Decompressed: 1975
Downloaded: 2851 file(s) [attempted 2856/8551 = 33%, 39 KB/s], Decompressed: 1975
Downloaded: 2888 file(s) [attempted 2893/8551 = 33%, 447 KB/s], Decompressed: 1975
Downloaded: 2926 file(s) [attempted 2931/8551 = 34%, 118 KB/s], Decompressed: 1975
Downloaded: 2967 file(s) [attempted 2972/8551 = 34%, 333 KB/s], Decompressed: 2416
Downloaded: 3007 file(s) [attempted 3013/8551 = 35%, 440 KB/s], Decompressed: 2416
Downloaded: 3051 file(s) [attempted 3058/8551 = 35%, 156 KB/s], Decompressed: 2416
Downloaded: 3088 file(s) [attempted 3095/8551 = 36%, 192 KB/s], Decompressed: 2416
Downloaded: 3129 file(s) [attempted 3136/8551 = 36%, 64 KB/s], Decompressed: 2416
Downloaded: 3174 file(s) [attempted 3181/8551 = 37%, 80 KB/s], Decompressed: 2416
Downloaded: 3215 file(s) [attempted 3222/8551 = 37%, 194 KB/s], Decompressed: 2416
Downloaded: 3256 file(s) [attempted 3263/8551 = 38%, 218 KB/s], Decompressed: 2416
Downloaded: 3292 file(s) [attempted 3299/8551 = 38%, 68 KB/s], Decompressed: 2416
Downloaded: 3331 file(s) [attempted 3338/8551 = 39%, 652 KB/s], Decompressed: 2416
Downloaded: 3375 file(s) [attempted 3383/8551 = 39%, 53 KB/s], Decompressed: 2416
Downloaded: 3419 file(s) [attempted 3427/8551 = 40%, 817 KB/s], Decompressed: 2416
Downloaded: 3460 file(s) [attempted 3468/8551 = 40%, 68 KB/s], Decompressed: 2416
Downloaded: 3491 file(s) [attempted 3499/8551 = 40%, 494 KB/s], Decompressed: 2416
Downloaded: 3533 file(s) [attempted 3541/8551 = 41%, 295 KB/s], Decompressed: 2416
Downloaded: 3573 file(s) [attempted 3581/8551 = 41%, 232 KB/s], Decompressed: 2416
Downloaded: 3617 file(s) [attempted 3626/8551 = 42%, 252 KB/s], Decompressed: 2967
Downloaded: 3658 file(s) [attempted 3667/8551 = 42%, 296 KB/s], Decompressed: 2967
Downloaded: 3692 file(s) [attempted 3701/8551 = 43%, 100 KB/s], Decompressed: 2967
Downloaded: 3733 file(s) [attempted 3742/8551 = 43%, 440 KB/s], Decompressed: 2967
Downloaded: 3774 file(s) [attempted 3783/8551 = 44%, 100 KB/s], Decompressed: 2967
Downloaded: 3812 file(s) [attempted 3821/8551 = 44%, 185 KB/s], Decompressed: 2967
Downloaded: 3850 file(s) [attempted 3859/8551 = 45%, 472 KB/s], Decompressed: 2967
Downloaded: 3887 file(s) [attempted 3896/8551 = 45%, 432 KB/s], Decompressed: 2967
Downloaded: 3935 file(s) [attempted 3944/8551 = 46%, 376 KB/s], Decompressed: 2967
Downloaded: 3980 file(s) [attempted 3989/8551 = 46%, 353 KB/s], Decompressed: 2967
Downloaded: 4024 file(s) [attempted 4033/8551 = 47%, 194 KB/s], Decompressed: 2967
Downloaded: 4055 file(s) [attempted 4064/8551 = 47%, 599 KB/s], Decompressed: 2967
Downloaded: 4088 file(s) [attempted 4098/8551 = 47%, 1 KB/s], Decompressed: 2967
Downloaded: 4133 file(s) [attempted 4143/8551 = 48%, 340 KB/s], Decompressed: 2967
Downloaded: 4177 file(s) [attempted 4187/8551 = 48%, 48 KB/s], Decompressed: 2967
Downloaded: 4217 file(s) [attempted 4228/8551 = 49%, 326 KB/s], Decompressed: 2967
Downloaded: 4251 file(s) [attempted 4262/8551 = 49%, 406 KB/s], Decompressed: 2967
Downloaded: 4282 file(s) [attempted 4293/8551 = 50%, 148 KB/s], Decompressed: 2967
Downloaded: 4330 file(s) [attempted 4341/8551 = 50%, 675 KB/s], Decompressed: 2967
Downloaded: 4378 file(s) [attempted 4389/8551 = 51%, 165 KB/s], Decompressed: 2967
Downloaded: 4426 file(s) [attempted 4437/8551 = 51%, 25 KB/s], Decompressed: 2967
Downloaded: 4464 file(s) [attempted 4475/8551 = 52%, 101 KB/s], Decompressed: 3617
Downloaded: 4501 file(s) [attempted 4512/8551 = 52%, 87 KB/s], Decompressed: 3617
Downloaded: 4532 file(s) [attempted 4543/8551 = 53%, 575 KB/s], Decompressed: 3617
Downloaded: 4580 file(s) [attempted 4591/8551 = 53%, 22 KB/s], Decompressed: 3617
Downloaded: 4625 file(s) [attempted 4636/8551 = 54%, 487 KB/s], Decompressed: 3617
Downloaded: 4670 file(s) [attempted 4681/8551 = 54%, 69 KB/s], Decompressed: 3617
Downloaded: 4709 file(s) [attempted 4721/8551 = 55%, 236 KB/s], Decompressed: 3617
Downloaded: 4750 file(s) [attempted 4762/8551 = 55%, 1363 KB/s], Decompressed: 3617
Downloaded: 4781 file(s) [attempted 4793/8551 = 56%, 240 KB/s], Decompressed: 3617
Downloaded: 4825 file(s) [attempted 4837/8551 = 56%, 101 KB/s], Decompressed: 3617
Downloaded: 4870 file(s) [attempted 4882/8551 = 57%, 96 KB/s], Decompressed: 3617
Downloaded: 4914 file(s) [attempted 4926/8551 = 57%, 34 KB/s], Decompressed: 3617
Downloaded: 4956 file(s) [attempted 4968/8551 = 58%, 92 KB/s], Decompressed: 3617
Downloaded: 4985 file(s) [attempted 4998/8551 = 58%, 416 KB/s], Decompressed: 3617
Downloaded: 5026 file(s) [attempted 5039/8551 = 58%, 299 KB/s], Decompressed: 3617
Downloaded: 5067 file(s) [attempted 5080/8551 = 59%, 240 KB/s], Decompressed: 3617
Downloaded: 5112 file(s) [attempted 5125/8551 = 59%, 2463 KB/s], Decompressed: 3617
Downloaded: 5156 file(s) [attempted 5169/8551 = 60%, 504 KB/s], Decompressed: 3617
Downloaded: 5191 file(s) [attempted 5204/8551 = 60%, 451 KB/s], Decompressed: 3617
Downloaded: 5232 file(s) [attempted 5245/8551 = 61%, 102 KB/s], Decompressed: 3617
Downloaded: 5269 file(s) [attempted 5282/8551 = 61%, 301 KB/s], Decompressed: 3617
Downloaded: 5314 file(s) [attempted 5327/8551 = 62%, 43 KB/s], Decompressed: 3617
Downloaded: 5358 file(s) [attempted 5371/8551 = 62%, 401 KB/s], Decompressed: 3617
Downloaded: 5403 file(s) [attempted 5416/8551 = 63%, 237 KB/s], Decompressed: 4429
Downloaded: 5437 file(s) [attempted 5450/8551 = 63%, 449 KB/s], Decompressed: 4429
Downloaded: 5474 file(s) [attempted 5487/8551 = 64%, 236 KB/s], Decompressed: 4429
Downloaded: 5516 file(s) [attempted 5529/8551 = 64%, 562 KB/s], Decompressed: 4429
Downloaded: 5557 file(s) [attempted 5570/8551 = 65%, 349 KB/s], Decompressed: 4429
Downloaded: 5601 file(s) [attempted 5614/8551 = 65%, 223 KB/s], Decompressed: 4429
Downloaded: 5632 file(s) [attempted 5645/8551 = 66%, 1009 KB/s], Decompressed: 4429
Downloaded: 5673 file(s) [attempted 5686/8551 = 66%, 283 KB/s], Decompressed: 4429
Downloaded: 5721 file(s) [attempted 5734/8551 = 67%, 69 KB/s], Decompressed: 4429
Downloaded: 5769 file(s) [attempted 5782/8551 = 67%, 1288 KB/s], Decompressed: 4429
Downloaded: 5812 file(s) [attempted 5827/8551 = 68%, 791 KB/s], Decompressed: 4429
Downloaded: 5848 file(s) [attempted 5864/8551 = 68%, 38 KB/s], Decompressed: 4429
Downloaded: 5879 file(s) [attempted 5895/8551 = 68%, 664 KB/s], Decompressed: 4429
Downloaded: 5920 file(s) [attempted 5936/8551 = 69%, 148 KB/s], Decompressed: 4429
Downloaded: 5968 file(s) [attempted 5984/8551 = 69%, 608 KB/s], Decompressed: 4429
Downloaded: 6015 file(s) [attempted 6032/8551 = 70%, 93 KB/s], Decompressed: 4429
Downloaded: 6056 file(s) [attempted 6073/8551 = 71%, 542 KB/s], Decompressed: 4429
Downloaded: 6090 file(s) [attempted 6107/8551 = 71%, 103 KB/s], Decompressed: 4429
Downloaded: 6128 file(s) [attempted 6145/8551 = 71%, 141 KB/s], Decompressed: 4429
Downloaded: 6169 file(s) [attempted 6186/8551 = 72%, 416 KB/s], Decompressed: 4429
Downloaded: 6213 file(s) [attempted 6230/8551 = 72%, 72 KB/s], Decompressed: 4429
Downloaded: 6254 file(s) [attempted 6271/8551 = 73%, 632 KB/s], Decompressed: 4429
Downloaded: 6289 file(s) [attempted 6306/8551 = 73%, 551 KB/s], Decompressed: 4429
Downloaded: 6323 file(s) [attempted 6340/8551 = 74%, 172 KB/s], Decompressed: 4429
Downloaded: 6364 file(s) [attempted 6381/8551 = 74%, 158 KB/s], Decompressed: 4429
Downloaded: 6404 file(s) [attempted 6422/8551 = 75%, 283 KB/s], Decompressed: 5372
Downloaded: 6449 file(s) [attempted 6467/8551 = 75%, 126 KB/s], Decompressed: 5372
Downloaded: 6485 file(s) [attempted 6504/8551 = 76%, 156 KB/s], Decompressed: 5372
Downloaded: 6526 file(s) [attempted 6545/8551 = 76%, 261 KB/s], Decompressed: 5372
Downloaded: 6556 file(s) [attempted 6576/8551 = 76%, 162 KB/s], Decompressed: 5372
Downloaded: 6601 file(s) [attempted 6621/8551 = 77%, 320 KB/s], Decompressed: 5372
Downloaded: 6638 file(s) [attempted 6658/8551 = 77%, 336 KB/s], Decompressed: 5372
Downloaded: 6679 file(s) [attempted 6699/8551 = 78%, 110 KB/s], Decompressed: 5372
Downloaded: 6714 file(s) [attempted 6734/8551 = 78%, 187 KB/s], Decompressed: 5372
Downloaded: 6751 file(s) [attempted 6771/8551 = 79%, 141 KB/s], Decompressed: 5372
Downloaded: 6792 file(s) [attempted 6812/8551 = 79%, 325 KB/s], Decompressed: 5372
Downloaded: 6833 file(s) [attempted 6853/8551 = 80%, 87 KB/s], Decompressed: 5372
Downloaded: 6874 file(s) [attempted 6894/8551 = 80%, 620 KB/s], Decompressed: 5372
Downloaded: 6911 file(s) [attempted 6931/8551 = 81%, 103 KB/s], Decompressed: 5372
Downloaded: 6949 file(s) [attempted 6970/8551 = 81%, 191 KB/s], Decompressed: 5372
Downloaded: 6992 file(s) [attempted 7014/8551 = 82%, 1213 KB/s], Decompressed: 5372
Downloaded: 7033 file(s) [attempted 7055/8551 = 82%, 642 KB/s], Decompressed: 5372
Downloaded: 7070 file(s) [attempted 7093/8551 = 82%, 112 KB/s], Decompressed: 5372
Downloaded: 7108 file(s) [attempted 7131/8551 = 83%, 866 KB/s], Decompressed: 5372
Downloaded: 7152 file(s) [attempted 7175/8551 = 83%, 630 KB/s], Decompressed: 5372
Downloaded: 7193 file(s) [attempted 7216/8551 = 84%, 118 KB/s], Decompressed: 5372
Downloaded: 7234 file(s) [attempted 7257/8551 = 84%, 39 KB/s], Decompressed: 5372
Downloaded: 7272 file(s) [attempted 7295/8551 = 85%, 172 KB/s], Decompressed: 5372
Downloaded: 7306 file(s) [attempted 7329/8551 = 85%, 285 KB/s], Decompressed: 5372
Downloaded: 7347 file(s) [attempted 7370/8551 = 86%, 421 KB/s], Decompressed: 5372
Downloaded: 7388 file(s) [attempted 7411/8551 = 86%, 74 KB/s], Decompressed: 5372
Downloaded: 7429 file(s) [attempted 7452/8551 = 87%, 287 KB/s], Decompressed: 5372
Downloaded: 7466 file(s) [attempted 7490/8551 = 87%, 41 KB/s], Decompressed: 5372
Downloaded: 7504 file(s) [attempted 7528/8551 = 88%, 590 KB/s], Decompressed: 6381
Downloaded: 7541 file(s) [attempted 7565/8551 = 88%, 1412 KB/s], Decompressed: 6381
Downloaded: 7582 file(s) [attempted 7606/8551 = 88%, 235 KB/s], Decompressed: 6381
Downloaded: 7623 file(s) [attempted 7647/8551 = 89%, 165 KB/s], Decompressed: 6381
Downloaded: 7661 file(s) [attempted 7685/8551 = 89%, 454 KB/s], Decompressed: 6381
Downloaded: 7705 file(s) [attempted 7729/8551 = 90%, 303 KB/s], Decompressed: 6381
Downloaded: 7750 file(s) [attempted 7774/8551 = 90%, 225 KB/s], Decompressed: 6381
Downloaded: 7788 file(s) [attempted 7812/8551 = 91%, 78 KB/s], Decompressed: 6381
Downloaded: 7824 file(s) [attempted 7849/8551 = 91%, 362 KB/s], Decompressed: 6381
Downloaded: 7865 file(s) [attempted 7890/8551 = 92%, 613 KB/s], Decompressed: 6381
Downloaded: 7906 file(s) [attempted 7931/8551 = 92%, 1069 KB/s], Decompressed: 6381
Downloaded: 7951 file(s) [attempted 7976/8551 = 93%, 230 KB/s], Decompressed: 6381
Downloaded: 7985 file(s) [attempted 8010/8551 = 93%, 100 KB/s], Decompressed: 6381
Downloaded: 8026 file(s) [attempted 8051/8551 = 94%, 185 KB/s], Decompressed: 6381
Downloaded: 8071 file(s) [attempted 8096/8551 = 94%, 52 KB/s], Decompressed: 6381
Downloaded: 8108 file(s) [attempted 8133/8551 = 95%, 441 KB/s], Decompressed: 6381
Downloaded: 8149 file(s) [attempted 8174/8551 = 95%, 307 KB/s], Decompressed: 6381
Downloaded: 8190 file(s) [attempted 8215/8551 = 96%, 161 KB/s], Decompressed: 6381
Downloaded: 8228 file(s) [attempted 8253/8551 = 96%, 116 KB/s], Decompressed: 6381
Downloaded: 8269 file(s) [attempted 8294/8551 = 96%, 29 KB/s], Decompressed: 6381
Downloaded: 8307 file(s) [attempted 8332/8551 = 97%, 240 KB/s], Decompressed: 6381
Downloaded: 8344 file(s) [attempted 8369/8551 = 97%, 559 KB/s], Decompressed: 6381
Downloaded: 8388 file(s) [attempted 8414/8551 = 98%, 182 KB/s], Decompressed: 6381
Downloaded: 8426 file(s) [attempted 8452/8551 = 98%, 320 KB/s], Decompressed: 6381
Downloaded: 8470 file(s) [attempted 8496/8551 = 99%, 57 KB/s], Decompressed: 6381
Downloaded: 8508 file(s) [attempted 8534/8551 = 99%, 75 KB/s], Decompressed: 6381
Downloaded: 8525 file(s) [attempted 8551/8551 = 100%, 476 KB/s], Decompressed: 6381
Downloaded: 8525 file(s) [attempted 8551/8551 = 100%, 476 KB/s], Decompressed: 6381
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.

  * If you push your commits to a PR to the mathlib4 repository
    (use a draft PR if it is not ready for review),
    then CI will build the oleans and they will be available later.
  * If you have already opened a PR, this may mean
    the CI build has failed part-way through building.

lake build

✔ [1954/1963] Built FLT.Assumptions.Mazur (17s)
✔ [2944/2951] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (3.1s)
✔ [2947/2952] Built FLT.Mathlib.Algebra.Algebra.Tower (1.7s)
✔ [2951/2965] Built FLT.Assumptions.Odlyzko (6.6s)
✔ [3221/3226] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.3s)
✔ [3224/3228] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (6.2s)
✔ [3225/3241] Built FLT.Hacks.RightActionInstances (3.7s)
✔ [3306/3323] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.5s)
✔ [3307/3323] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (2.9s)
✔ [3308/3323] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (1.6s)
✔ [3309/3323] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.2s)
✔ [3310/3323] Built FLT.Mathlib.Order.Filter.Cofinite (1.1s)
✔ [3312/3323] Built FLT.Mathlib.Topology.Bases (1.1s)
✔ [3314/3323] Built FLT.Mathlib.MeasureTheory.Group.Action (2.4s)
✔ [3315/3323] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.6s)
✔ [3316/3323] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.5s)
✔ [3317/3323] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (5.3s)
✔ [3319/3324] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.7s)
✔ [3320/3324] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.8s)
✔ [3321/3324] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (5.5s)
✔ [3322/3324] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (4.6s)
✔ [3328/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.2s)
✔ [3331/3337] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (10s)
✔ [3334/3345] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.6s)
✔ [3336/3345] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.9s)
✔ [3337/3345] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.2s)
✔ [3338/3345] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.2s)
✔ [3339/3345] Built FLT.HaarMeasure.HaarChar.AddEquiv (6.6s)
✔ [3342/3351] Built FLT.HaarMeasure.HaarChar.Ring (3.2s)
✔ [3345/3351] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.0s)
✔ [3346/3352] Built FLT.Mathlib.LinearAlgebra.Countable (1.5s)
✔ [3350/3358] Built FLT.DedekindDomain.AdicValuation (8.9s)
✔ [3357/3362] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (2.5s)
✔ [3367/3378] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.1s)
✔ [3371/3378] Built FLT.DedekindDomain.IntegralClosure (5.0s)
✔ [3372/3378] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.8s)
✔ [3375/3380] Built FLT.NumberField.HeightOneSpectrum (1.7s)
✔ [3376/3382] Built FLT.NumberField.Completion.Finite (2.5s)
✔ [3378/3396] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.1s)
✔ [3383/3396] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.7s)
✔ [3384/3396] Built FLT.Mathlib.Algebra.Algebra.Hom (2.0s)
✔ [3385/3396] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.0s)
✔ [3387/3406] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.8s)
✔ [3388/3406] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.4s)
✔ [3389/3406] Built FLT.Mathlib.Algebra.Algebra.Pi (1.4s)
✔ [3391/3406] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.1s)
✔ [3393/3406] Built FLT.Mathlib.Algebra.IsDirectLimit (1.9s)
✔ [3394/3406] Built FLT.Mathlib.Topology.Algebra.MulAction (1.1s)
✔ [3395/3406] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.7s)
✔ [3398/3410] Built FLT.Mathlib.LinearAlgebra.Pi (1.4s)
✔ [3399/3410] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.6s)
✔ [3401/3410] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.2s)
✔ [3403/3410] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.2s)
✔ [3405/3410] Built FLT.DedekindDomain.Completion.BaseChange (28s)
✔ [3406/3412] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.2s)
✔ [3407/3425] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (1.0s)
✔ [3410/3426] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (80s)
✔ [3412/3426] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.8s)
✔ [3413/3426] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.8s)
✔ [3414/3426] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.4s)
✔ [3415/3426] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.2s)
✔ [3416/3426] Built FLT.NumberField.InfinitePlace.Extension (2.6s)
✔ [3417/3426] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.5s)
✔ [3419/3429] Built FLT.Mathlib.Topology.Constructions (1.0s)
✔ [3422/3429] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.5s)
✔ [3424/3436] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.9s)
✔ [3425/3438] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.9s)
✔ [3427/3438] Built FLT.NumberField.Padics.RestrictedProduct (2.8s)
✔ [3428/3438] Built FLT.Mathlib.Data.Real.Archimedean (1.1s)
✔ [3429/3438] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.4s)
✔ [3430/3438] Built FLT.NumberField.Completion.Infinite (16s)
✔ [3431/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.0s)
✔ [3434/3441] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.8s)
✔ [3435/3441] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (6.0s)
✔ [3436/3441] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3438/3441] Built FLT.NumberField.AdeleRing (23s)
✔ [3445/3463] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (2.1s)
✔ [3448/3466] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (3.3s)
✔ [3449/3466] Built FLT.HaarMeasure.MeasurableSpacePadics (1.0s)
✔ [3451/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.2s)
✔ [3452/3469] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.4s)
✔ [3453/3469] Built FLT.HaarMeasure.HaarChar.RealComplex (2.5s)
✔ [3456/3469] Built FLT.HaarMeasure.HaarChar.Padic (2.6s)
✔ [3457/3469] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.3s)
✔ [3460/3469] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.2s)
✔ [3461/3469] Built FLT.Mathlib.Algebra.Central.TensorProduct (2.1s)
✔ [3462/3469] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (6.8s)
✔ [3464/3469] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.2s)
✔ [3465/3470] Built FLT.Mathlib.LinearAlgebra.Determinant (3.9s)
✔ [3466/3471] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (2.8s)
✔ [3468/3474] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (31s)
✔ [3469/3474] Built FLT.HaarMeasure.HaarChar.AdeleRing (6.1s)
✔ [3479/3488] Built FLT.Mathlib.Topology.HomToDiscrete (1.7s)
✔ [3480/3488] Built FLT.Mathlib.Topology.Polish (2.1s)
✔ [3482/3488] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.3s)
✔ [3486/3505] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.6s)
✔ [3487/3505] Built FLT.Mathlib.Topology.Instances.Matrix (1.5s)
✔ [3488/3505] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.7s)
✔ [3489/3505] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (3.7s)
✔ [3490/3505] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.4s)
✔ [3493/3505] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.0s)
✔ [3494/3505] Built FLT.DivisionAlgebra.Finiteness (40s)
✔ [3495/3505] Built FLT.Data.QHat (5.8s)
✔ [3497/3505] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.5s)
✔ [3498/3505] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.4s)
✔ [3499/3511] Built FLT.Data.Hurwitz (3.8s)
✔ [3500/3512] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (1.9s)
✔ [3501/3512] Built FLT.Data.HurwitzRatHat (2.3s)
✔ [3503/3514] Built FLT.QuaternionAlgebra.NumberField (8.2s)
✔ [3506/3514] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (6.2s)
✔ [3509/3517] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (8.8s)
✔ [3512/3517] Built FLT.Patching.Utils.Lemmas (3.0s)
✔ [3515/3518] Built FLT.Patching.Utils.InverseLimit (1.3s)
✔ [3525/3535] Built FLT.Deformations.Lemmas (3.0s)
✔ [3526/3535] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.3s)
✔ [3529/3535] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.2s)
✔ [3530/3535] Built FLT.Deformations.IsResidueAlgebra (1.0s)
✔ [3531/3536] Built FLT.Patching.Utils.AdicTopology (3.3s)
✔ [3532/3536] Built FLT.Deformations.Subfunctor (946ms)
✔ [3533/3536] Built FLT.Deformations.IsProartinian (1.9s)
✔ [3535/3541] Built FLT.Deformations.Categories (3.2s)
✔ [3582/3586] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.2s)
✔ [3583/3589] Built FLT.Deformations.RepresentationTheory.Frobenius (2.9s)
✔ [3603/3610] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [3614/3622] Built FLT.Deformations.RepresentationTheory.Etale (8.9s)
✔ [3631/3639] Built FLT.Deformations.RepresentationTheory.GaloisRep (12s)
✔ [3634/3640] Built FLT.Mathlib.RepresentationTheory.Basic (2.2s)
✔ [3636/3640] Built FLT.Deformations.RepresentationTheory.Irreducible (1.5s)
✔ [3638/3640] Built FLT.Deformations.LiftFunctor (3.0s)
✔ [3639/3643] Built FLT.Deformations.Representable (2.9s)
✔ [3646/3651] Built FLT.EllipticCurve.Torsion (2.5s)
✔ [3652/3654] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (3.1s)
✔ [3816/3829] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.3s)
✔ [3817/3829] Built FLT.GaloisRepresentation.Automorphic (3.1s)
✔ [3819/3829] Built FLT.GaloisRepresentation.Cyclotomic (2.2s)
✔ [3821/3829] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.7s)
✔ [3822/3829] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.3s)
✔ [3823/3829] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.4s)
✔ [3824/3829] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.3s)
✔ [3825/3829] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.5s)
✔ [3826/3834] Built FLT.FreyCurve.FreyPackage (3.6s)
✔ [3827/3834] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.0s)
✔ [3829/3835] Built FLT.FreyCurve.Contradiction (2.1s)
✔ [3953/3971] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.3s)
✔ [3954/3971] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.6s)
✔ [3955/3971] Built FLT.Mathlib.Data.Fin.Basic (1.1s)
✔ [3956/3971] Built FLT.Mathlib.Data.Set.Prod (565ms)
✔ [3957/3971] Built FLT.Mathlib.GroupTheory.Index (1.1s)
✔ [3958/3971] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.5s)
✔ [3959/3971] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.4s)
✔ [3960/3971] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.5s)
✔ [3962/3971] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s)
✔ [3966/3974] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.3s)
✔ [3973/3981] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.0s)
✔ [3975/3985] Built FLT.GlobalLanglandsConjectures.GLzero (2.3s)
✔ [3979/3988] Built FLT.Patching.Utils.TopologicallyFG (1.6s)
✔ [3981/3988] Built FLT.NumberField.DiscriminantBounds (2.7s)
✔ [3983/3990] Built FLT.Patching.Utils.StructureFiniteness (3.6s)
✔ [3984/3990] Built FLT.Patching.Ultraproduct (8.3s)
✔ [3986/3990] Built FLT.Patching.Module (11s)
✔ [3987/3990] Built FLT.Patching.Algebra (9.7s)
✔ [3989/3993] Built FLT.Patching.Over (11s)
✔ [4006/4014] Built FLT.Patching.VanishingFilter (2.8s)
✔ [4008/4014] Built FLT.Patching.Utils.Depth (2.9s)
✔ [4009/4014] Built FLT.Patching.Utils.CompactHausdorffRings (2.2s)
✔ [4010/4014] Built FLT.Patching.System (10s)
✔ [4011/4014] Built FLT.Patching.REqualsT (4.0s)
✔ [4012/4014] Built FLT (2.4s)
✔ [4013/4014] Built FermatsLastTheorem (103s)
Build completed successfully (4014 jobs).

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract (extract-batch-00099)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00100)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00101)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-00000)

apx-semantic-phase	{"phase":"core_compile","duration_ms":30102}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":937,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":56563,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache d6146eaea26ed72ba775c97762cd00991cde0f0b3dbcd3b26d150e94e41cadc7
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-527-runtime-semantic_extract-814098-1781791774529742240-3

semantic_extract (extract-batch-00102)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00103)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00027)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00028)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00029)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00030)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00031)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00032)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00033)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00034)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00035)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00036)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00037)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00038)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00039)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00040)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00041)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00042)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00043)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00044)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00045)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00046)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00047)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00048)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00049)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00050)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00051)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00052)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00053)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00054)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-527-source

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

git checkout 8009e3496a5d1bd32ba938765deb1c1db208ef1e

Note: switching to '8009e3496a5d1bd32ba938765deb1c1db208ef1e'.

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 8009e34 chore: bump mathlib to 1ccad00, fix breaking changes (#1025)

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)

apx-semantic-phase	{"duration_ms":30,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":2,"diagnostic_count":0,"duration_ms":112,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":2,"dependency_count":2,"diagnostic_count":12,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":434139,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":2,"dependency_count":2,"diagnostic_count":12,"duration_ms":75,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":20996,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"ok":true,"payload_bytes":20996,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1396,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":103524,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache ae808ede3861ccf0a8433320c37f62727fec44384715e895d36a0da5c4a369ec
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":442424,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

apx-semantic-phase	{"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":1,"duration_ms":148,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":4,"diagnostic_count":8,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":402499,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":4,"diagnostic_count":8,"duration_ms":71,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":62975,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":62975,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":288,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":5010,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 1cd9fcc18341bdcecacd58285bd3aea7d3c12df823dac8b3e8fb706173cb42ed
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":410290,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":13,"diagnostic_count":6,"duration_ms":802,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":13,"dependency_count":28,"diagnostic_count":105,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":501412,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":13,"dependency_count":28,"diagnostic_count":105,"duration_ms":73,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":248948,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":248948,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":148,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":8314,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 8531df0ce1c9962b6c729bf161aeadbe283a9859e02cfd539be34007002f1c81
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":505990,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":1,"duration_ms":109,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":3,"diagnostic_count":16,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":145124,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":3,"diagnostic_count":16,"duration_ms":37,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":19301,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":19301,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":141,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":2446,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache daa4f381d4617708fee5c30289b13dac7805847dce87c93b73a59e7da33ee010
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":147694,"ok":true}

semantic_extract (extract-batch-00055)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00056)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00057)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00058)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00059)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00060)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":4,"diagnostic_count":1,"duration_ms":113,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":4,"dependency_count":6,"diagnostic_count":11,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":225630,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":4,"dependency_count":6,"diagnostic_count":11,"duration_ms":56,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":20458,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":20458,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":146,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":2529,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e89f0fa8ed2196ad6b7bedb4349a651eeb06327d6244dd44b01d4fca039eff98
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":228246,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":1,"duration_ms":109,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":2,"diagnostic_count":6,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":264086,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":3,"dependency_count":2,"diagnostic_count":6,"duration_ms":42,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":125724,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":125724,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":131,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":2855,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 33200a1f2e8128957fe012a1d037f939a15faa3a124fdfcd1cb1edf28894a28c
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":267079,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":251,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":6,"dependency_count":8,"diagnostic_count":28,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":473022,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":6,"dependency_count":8,"diagnostic_count":28,"duration_ms":78,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":164195,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":164195,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":190,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":10,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":9777,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache a5c2f6d1d38296eb70efafc482443ca96bbe24445054f5f6bd4772b05dd3a76a
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":476877,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)

apx-semantic-phase	{"duration_ms":26,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":29,"diagnostic_count":11,"duration_ms":1109,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":29,"dependency_count":61,"diagnostic_count":129,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":319593,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":29,"dependency_count":61,"diagnostic_count":129,"duration_ms":107,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":1405660,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"ok":true,"payload_bytes":1405660,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":112,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3158,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 02db8d063299bdf1c07b634fa3b9bc5d52c72c7da2cdc334c967ad0f0ba79ed4
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":324239,"ok":true}

semantic_extract (extract-batch-00061)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00062)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00063)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00064)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00065)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00066)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":114,"diagnostic_count":64,"duration_ms":3803,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":114,"dependency_count":353,"diagnostic_count":277,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":253781,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":114,"dependency_count":353,"diagnostic_count":277,"duration_ms":163,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":2342382,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"ok":true,"payload_bytes":2342382,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":156,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":2831,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e104eba0ad6ed58e19a0dacff49b125d8a4be82f8f085c6db83894e3c95540b1
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":260455,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":73,"diagnostic_count":39,"duration_ms":2143,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":73,"dependency_count":167,"diagnostic_count":45,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":250188,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":73,"dependency_count":167,"diagnostic_count":45,"duration_ms":60,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":1273513,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":1273513,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":150,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":2903,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 308091f827c844a84dd9178ff911c8019263783e1bc9246ec89eb8be71ed59f3
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":255147,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":64,"diagnostic_count":22,"duration_ms":4615,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":64,"dependency_count":195,"diagnostic_count":195,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":788353,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":64,"dependency_count":195,"diagnostic_count":195,"duration_ms":353,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":692589,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":30,"ok":true,"payload_bytes":692589,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":148,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":32949,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2a242a69e9c4d9d97762d09b36bd45e169d65a64e05a6b3efb376151de1149b3
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":798472,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)

apx-semantic-phase	{"duration_ms":18,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":2,"diagnostic_count":0,"duration_ms":143,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":191638,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":54,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":7020,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":5,"ok":true,"payload_bytes":7020,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1213,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":37,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":80455,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 09bca74ef0dc72cb82381433ba3362ade31f333b938369002cbad6e82fa6f882
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":197954,"ok":true}

semantic_extract (extract-batch-00067)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00068)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00069)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00070)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00071)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00072)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)

apx-semantic-phase	{"duration_ms":8,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":96,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":1,"diagnostic_count":4,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":233335,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":1,"diagnostic_count":4,"duration_ms":85,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":6262,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":6262,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":273,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":15008,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache b2883a5916bab698825822cc97e4b8c642641fe18a8462150208f240a06f3384
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":240337,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)

apx-semantic-phase	{"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":2,"diagnostic_count":0,"duration_ms":236,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":268481,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":92,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":13987,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"ok":true,"payload_bytes":13987,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":719,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":26,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":16675,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 3e68f62d038bdb2e0c9299eb159f5a1bac60b7d8dab8b9d2418eb93884a73988
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":277849,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)

apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":72,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":1,"diagnostic_count":3,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":153207,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":1,"diagnostic_count":3,"duration_ms":58,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":10119,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":10119,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":312,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4139,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e1286e509d1f717807526d2ca9fabcbc8ad0c2cef057747a4f4b13491db9120f
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":160973,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":2,"diagnostic_count":0,"duration_ms":174,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":270546,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":91,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":33504,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"ok":true,"payload_bytes":33504,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":470,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3657,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 82b6de9f22b18c7b2acce2b5bf1705d36864d9fef2a617bfa2ad59b8a818355e
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":274428,"ok":true}

semantic_extract (extract-batch-00073)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00074)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00075)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00076)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00077)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00078)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)

apx-semantic-phase	{"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":1,"duration_ms":296,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"dependency_count":2,"diagnostic_count":1,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":336170,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"dependency_count":2,"diagnostic_count":1,"duration_ms":69,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":50871,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"ok":true,"payload_bytes":50871,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":17}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":299,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":23288,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 549ca281e215137c971579d131a0ffdc07cdb270e5bb29394746bb1d789eefd6
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":356476,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)

apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":2,"diagnostic_count":0,"duration_ms":139,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":188909,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":54,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":6371,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":6371,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":688,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":7874,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 436b3b17e9527f8f09840715e267db5eea7ef75ab3c88113bba1533a89a99cde
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":203310,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":13,"diagnostic_count":6,"duration_ms":753,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":13,"dependency_count":31,"diagnostic_count":71,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":144835,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":13,"dependency_count":31,"diagnostic_count":71,"duration_ms":90,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":399479,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":399479,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":276,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4441,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 9ac14140501ac6c1520613353d32429899331393a4398403641a9e64e39cb118
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":155027,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00019)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":11,"diagnostic_count":9,"duration_ms":560,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":11,"dependency_count":24,"diagnostic_count":106,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":156041,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":11,"dependency_count":24,"diagnostic_count":106,"duration_ms":87,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":499238,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":499238,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":480,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":13,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":5082,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache ce6f3377cb6d1e833330cc2db6b276d700822a120cf8ebcf87aed9e05905f795
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":163829,"ok":true}

semantic_extract (extract-batch-00079)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00080)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00081)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00082)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00083)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00084)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00020)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":49,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":193157,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":64,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":7139,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":7139,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":15}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":276,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":7707,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 1d90972c61308fbff29c7bb74625395398626cca333505caa2485c5e14faafae
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":199802,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00021)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":5,"duration_ms":267,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":6,"dependency_count":6,"diagnostic_count":8,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":156714,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":6,"dependency_count":6,"diagnostic_count":8,"duration_ms":60,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":53978,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":53978,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":492,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4287,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 26ad3d1a9ecf31a28fa39b2a5fd4bbacc3520a282ad822d85edb112340500f8a
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":163819,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00022)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":5,"diagnostic_count":3,"duration_ms":286,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":5,"dependency_count":8,"diagnostic_count":23,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":131445,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":5,"dependency_count":8,"diagnostic_count":23,"duration_ms":64,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":295443,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":295443,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":262,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":6486,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 67004ec15ac1ac835ceaf8f5e77840d584d926665584553c9c29163dbb12392e
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":138331,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00023)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":4,"diagnostic_count":0,"duration_ms":230,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":4,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":135987,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":4,"dependency_count":0,"diagnostic_count":0,"duration_ms":45,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":26412,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":26412,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":455,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3975,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7c617ef5c8c1511a87528439fae9cc6ca4e947c53dcf4c19c828f132c003eb62
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":142074,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00024)

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":690,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":5417,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 0d09b80821be6bb45669c0f8b5daad68300d333a34362d8633a2688ef091483c
/usr/bin/podman timed out after 18s
podman cleanup removed verifier container apx-verifier-job-527-runtime-semantic_extract-814098-1781813362622559210-28

semantic_extract (extract-batch-00025)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00026)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00104)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00105)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00106)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00107)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00108)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00109)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00110)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00111)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00112)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00113)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00114)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00115)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00116)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00117)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00118)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00119)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00120)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00121)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00122)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00123)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00124)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00125)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00126)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00127)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00128)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00129)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started

semantic_extract (extract-batch-00130)

semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started