Verification run

Run 336

promachina/iut-lean branch master triggered via poller

failed commit e1fd2289614e toolchain lean-v4-30-0 prover lean took 6h 15m · finished 5w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)

Open project

Package 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_clone exit 0 duration 2s · created 6/10/2026, 12:17:16 AM

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

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

git_checkout exit 0 duration 143 ms · created 6/10/2026, 12:17:16 AM

git checkout e1fd2289614ecacd3e7f1fa9b3eb21d7d500befd

Note: switching to 'e1fd2289614ecacd3e7f1fa9b3eb21d7d500befd'.

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 e1fd228 Transport submodule residue quotient to Haar endpoint

lake_cache exit 0 duration 36s · created 6/10/2026, 12:17:16 AM

lake exe cache get

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

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8459 = 0%, 8 KB/s], Decompressed: 16
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 22 KB/s], Decompressed: 35
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 56 KB/s], Decompressed: 61
Downloaded: 91 file(s) [attempted 91/8459 = 1%, 184 KB/s], Decompressed: 86
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 282 KB/s], Decompressed: 121
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 752 KB/s], Decompressed: 151
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 44 KB/s], Decompressed: 189
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 618 KB/s], Decompressed: 230
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 55 KB/s], Decompressed: 264
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 328 KB/s], Decompressed: 306
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 685 KB/s], Decompressed: 347
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 55 KB/s], Decompressed: 388
Downloaded: 431 file(s) [attempted 431/8459 = 5%, 564 KB/s], Decompressed: 425
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 1124 KB/s], Decompressed: 463
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 825 KB/s], Decompressed: 501
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 65 KB/s], Decompressed: 542
Downloaded: 588 file(s) [attempted 588/8459 = 6%, 47 KB/s], Decompressed: 583
Downloaded: 631 file(s) [attempted 631/8459 = 7%, 181 KB/s], Decompressed: 627
Downloaded: 667 file(s) [attempted 667/8459 = 7%, 64 KB/s], Decompressed: 658
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 65 KB/s], Decompressed: 699
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 89 KB/s], Decompressed: 744
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 97 KB/s], Decompressed: 785
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 205 KB/s], Decompressed: 833
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 290 KB/s], Decompressed: 881
Downloaded: 927 file(s) [attempted 927/8459 = 10%, 177 KB/s], Decompressed: 919
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 362 KB/s], Decompressed: 960
Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 363 KB/s], Decompressed: 1001
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 699 KB/s], Decompressed: 1042
Downloaded: 1084 file(s) [attempted 1084/8459 = 12%, 76 KB/s], Decompressed: 1080
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 152 KB/s], Decompressed: 1124
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 480 KB/s], Decompressed: 1162
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 989 KB/s], Decompressed: 1203
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 242 KB/s], Decompressed: 1240
Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 230 KB/s], Decompressed: 1288
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 161 KB/s], Decompressed: 1326
Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 148 KB/s], Decompressed: 1360
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 129 KB/s], Decompressed: 1405
Downloaded: 1451 file(s) [attempted 1451/8459 = 17%, 108 KB/s], Decompressed: 1442
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 272 KB/s], Decompressed: 1487
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 1186 KB/s], Decompressed: 1524
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 115 KB/s], Decompressed: 1566
Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 205 KB/s], Decompressed: 1603
Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 131 KB/s], Decompressed: 1644
Downloaded: 1691 file(s) [attempted 1691/8459 = 19%, 156 KB/s], Decompressed: 1682
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 289 KB/s], Decompressed: 1726
Downloaded: 1773 file(s) [attempted 1773/8459 = 20%, 172 KB/s], Decompressed: 1768
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 96 KB/s], Decompressed: 1809
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 150 KB/s], Decompressed: 1846
Downloaded: 1888 file(s) [attempted 1888/8459 = 22%, 303 KB/s], Decompressed: 1880
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 76 KB/s], Decompressed: 1925
Downloaded: 1973 file(s) [attempted 1973/8459 = 23%, 258 KB/s], Decompressed: 1969
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 129 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 192 KB/s], Decompressed: 2048
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 74 KB/s], Decompressed: 2086
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 987 KB/s], Decompressed: 2127
Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 104 KB/s], Decompressed: 2171
Downloaded: 2213 file(s) [attempted 2213/8459 = 26%, 414 KB/s], Decompressed: 2209
Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 726 KB/s], Decompressed: 2243
Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 313 KB/s], Decompressed: 2284
Downloaded: 2329 file(s) [attempted 2329/8459 = 27%, 38 KB/s], Decompressed: 2325
Downloaded: 2372 file(s) [attempted 2372/8459 = 28%, 1106 KB/s], Decompressed: 2366
Downloaded: 2408 file(s) [attempted 2408/8459 = 28%, 274 KB/s], Decompressed: 2404
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 256 KB/s], Decompressed: 2442
Downloaded: 2492 file(s) [attempted 2492/8459 = 29%, 132 KB/s], Decompressed: 2486
Downloaded: 2532 file(s) [attempted 2532/8459 = 29%, 254 KB/s], Decompressed: 2527
Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 703 KB/s], Decompressed: 2565
Downloaded: 2611 file(s) [attempted 2611/8459 = 30%, 386 KB/s], Decompressed: 2602
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 268 KB/s], Decompressed: 2644
Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 794 KB/s], Decompressed: 2691
Downloaded: 2731 file(s) [attempted 2731/8459 = 32%, 630 KB/s], Decompressed: 2726
Downloaded: 2771 file(s) [attempted 2771/8459 = 32%, 62 KB/s], Decompressed: 2763
Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 160 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 124 KB/s], Decompressed: 2849
Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 176 KB/s], Decompressed: 2890
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 679 KB/s], Decompressed: 2931
Downloaded: 2972 file(s) [attempted 2972/8459 = 35%, 1101 KB/s], Decompressed: 2969
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 212 KB/s], Decompressed: 3013
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 1160 KB/s], Decompressed: 3054
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 182 KB/s], Decompressed: 3095
Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 594 KB/s], Decompressed: 3136
Downloaded: 3186 file(s) [attempted 3186/8459 = 37%, 60 KB/s], Decompressed: 3177
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 51 KB/s], Decompressed: 3222
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 1080 KB/s], Decompressed: 3256
Downloaded: 3303 file(s) [attempted 3303/8459 = 39%, 323 KB/s], Decompressed: 3294
Downloaded: 3342 file(s) [attempted 3342/8459 = 39%, 493 KB/s], Decompressed: 3338
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 76 KB/s], Decompressed: 3379
Downloaded: 3428 file(s) [attempted 3428/8459 = 40%, 696 KB/s], Decompressed: 3420
Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 589 KB/s], Decompressed: 3461
Downloaded: 3506 file(s) [attempted 3506/8459 = 41%, 80 KB/s], Decompressed: 3503
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 464 KB/s], Decompressed: 3544
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 172 KB/s], Decompressed: 3585
Downloaded: 3628 file(s) [attempted 3628/8459 = 42%, 622 KB/s], Decompressed: 3622
Downloaded: 3665 file(s) [attempted 3665/8459 = 43%, 248 KB/s], Decompressed: 3660
Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 58 KB/s], Decompressed: 3701
Downloaded: 3748 file(s) [attempted 3748/8459 = 44%, 216 KB/s], Decompressed: 3742
Downloaded: 3788 file(s) [attempted 3788/8459 = 44%, 473 KB/s], Decompressed: 3783
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 402 KB/s], Decompressed: 3821
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 52 KB/s], Decompressed: 3862
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 65 KB/s], Decompressed: 3903
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 341 KB/s], Decompressed: 3947
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 173 KB/s], Decompressed: 3985
Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 106 KB/s], Decompressed: 4023
Downloaded: 4064 file(s) [attempted 4064/8459 = 48%, 967 KB/s], Decompressed: 4060
Downloaded: 4106 file(s) [attempted 4106/8459 = 48%, 40 KB/s], Decompressed: 4101
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 794 KB/s], Decompressed: 4140
Downloaded: 4181 file(s) [attempted 4181/8459 = 49%, 109 KB/s], Decompressed: 4178
Downloaded: 4222 file(s) [attempted 4222/8459 = 49%, 423 KB/s], Decompressed: 4218
Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 329 KB/s], Decompressed: 4255
Downloaded: 4301 file(s) [attempted 4301/8459 = 50%, 217 KB/s], Decompressed: 4297
Downloaded: 4344 file(s) [attempted 4344/8459 = 51%, 136 KB/s], Decompressed: 4338
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 1024 KB/s], Decompressed: 4375
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 449 KB/s], Decompressed: 4420
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 110 KB/s], Decompressed: 4461
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 203 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 142 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 649 KB/s], Decompressed: 4577
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 150 KB/s], Decompressed: 4625
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 535 KB/s], Decompressed: 4659
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 162 KB/s], Decompressed: 4704
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 110 KB/s], Decompressed: 4741
Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 63 KB/s], Decompressed: 4783
Downloaded: 4830 file(s) [attempted 4830/8459 = 57%, 397 KB/s], Decompressed: 4824
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 188 KB/s], Decompressed: 4865
Downloaded: 4911 file(s) [attempted 4911/8459 = 58%, 281 KB/s], Decompressed: 4902
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 621 KB/s], Decompressed: 4948
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 91 KB/s], Decompressed: 4988
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 57 KB/s], Decompressed: 5032
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 362 KB/s], Decompressed: 5078
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 50 KB/s], Decompressed: 5118
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 413 KB/s], Decompressed: 5159
Downloaded: 5207 file(s) [attempted 5207/8459 = 61%, 49 KB/s], Decompressed: 5203
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 44 KB/s], Decompressed: 5241
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 290 KB/s], Decompressed: 5282
Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 66 KB/s], Decompressed: 5320
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 880 KB/s], Decompressed: 5361
Downloaded: 5410 file(s) [attempted 5410/8459 = 63%, 172 KB/s], Decompressed: 5405
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 465 KB/s], Decompressed: 5443
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 296 KB/s], Decompressed: 5481
Downloaded: 5520 file(s) [attempted 5520/8459 = 65%, 178 KB/s], Decompressed: 5512
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 99 KB/s], Decompressed: 5559
Downloaded: 5609 file(s) [attempted 5609/8459 = 66%, 455 KB/s], Decompressed: 5600
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 552 KB/s], Decompressed: 5638
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 651 KB/s], Decompressed: 5679
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 157 KB/s], Decompressed: 5720
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 470 KB/s], Decompressed: 5761
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 68 KB/s], Decompressed: 5809
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 96 KB/s], Decompressed: 5850
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 53 KB/s], Decompressed: 5885
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 1199 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 615 KB/s], Decompressed: 5967
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 105 KB/s], Decompressed: 6015
Downloaded: 6062 file(s) [attempted 6062/8459 = 71%, 25 KB/s], Decompressed: 6056
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 62 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 239 KB/s], Decompressed: 6138
Downloaded: 6183 file(s) [attempted 6183/8459 = 73%, 175 KB/s], Decompressed: 6175
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 95 KB/s], Decompressed: 6221
Downloaded: 6265 file(s) [attempted 6265/8459 = 74%, 121 KB/s], Decompressed: 6261
Downloaded: 6302 file(s) [attempted 6302/8459 = 74%, 1083 KB/s], Decompressed: 6295
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 272 KB/s], Decompressed: 6336
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 73 KB/s], Decompressed: 6384
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 158 KB/s], Decompressed: 6429
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 133 KB/s], Decompressed: 6466
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 86 KB/s], Decompressed: 6504
Downloaded: 6547 file(s) [attempted 6547/8459 = 77%, 474 KB/s], Decompressed: 6542
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 395 KB/s], Decompressed: 6590
Downloaded: 6638 file(s) [attempted 6638/8459 = 78%, 34 KB/s], Decompressed: 6634
Downloaded: 6678 file(s) [attempted 6678/8459 = 78%, 530 KB/s], Decompressed: 6675
Downloaded: 6716 file(s) [attempted 6716/8459 = 79%, 594 KB/s], Decompressed: 6709
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 171 KB/s], Decompressed: 6750
Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 201 KB/s], Decompressed: 6791
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 239 KB/s], Decompressed: 6836
Downloaded: 6885 file(s) [attempted 6885/8459 = 81%, 182 KB/s], Decompressed: 6880
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 255 KB/s], Decompressed: 6918
Downloaded: 6959 file(s) [attempted 6959/8459 = 82%, 972 KB/s], Decompressed: 6952
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 131 KB/s], Decompressed: 6993
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 393 KB/s], Decompressed: 7038
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 312 KB/s], Decompressed: 7082
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 30 KB/s], Decompressed: 7123
Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 92 KB/s], Decompressed: 7161
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 135 KB/s], Decompressed: 7202
Downloaded: 7248 file(s) [attempted 7248/8459 = 85%, 70 KB/s], Decompressed: 7243
Downloaded: 7285 file(s) [attempted 7285/8459 = 86%, 35 KB/s], Decompressed: 7281
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 161 KB/s], Decompressed: 7325
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 58 KB/s], Decompressed: 7360
Downloaded: 7406 file(s) [attempted 7406/8459 = 87%, 42 KB/s], Decompressed: 7397
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 115 KB/s], Decompressed: 7445
Downloaded: 7494 file(s) [attempted 7494/8459 = 88%, 331 KB/s], Decompressed: 7490
Downloaded: 7532 file(s) [attempted 7532/8459 = 89%, 650 KB/s], Decompressed: 7527
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 135 KB/s], Decompressed: 7565
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 221 KB/s], Decompressed: 7603
Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 210 KB/s], Decompressed: 7647
Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 355 KB/s], Decompressed: 7691
Downloaded: 7735 file(s) [attempted 7735/8459 = 91%, 258 KB/s], Decompressed: 7729
Downloaded: 7772 file(s) [attempted 7772/8459 = 91%, 165 KB/s], Decompressed: 7767
Downloaded: 7809 file(s) [attempted 7809/8459 = 92%, 48 KB/s], Decompressed: 7804
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 77 KB/s], Decompressed: 7849
Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 1288 KB/s], Decompressed: 7891
Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 107 KB/s], Decompressed: 7931
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 211 KB/s], Decompressed: 7969
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 342 KB/s], Decompressed: 8010
Downloaded: 8049 file(s) [attempted 8049/8459 = 95%, 137 KB/s], Decompressed: 8041
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 111 KB/s], Decompressed: 8088
Downloaded: 8131 file(s) [attempted 8131/8459 = 96%, 914 KB/s], Decompressed: 8126
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 1105 KB/s], Decompressed: 8171
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8205
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 207 KB/s], Decompressed: 8242
Downloaded: 8292 file(s) [attempted 8292/8459 = 98%, 464 KB/s], Decompressed: 8284
Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 531 KB/s], Decompressed: 8328
Downloaded: 8370 file(s) [attempted 8370/8459 = 98%, 690 KB/s], Decompressed: 8366
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 982 KB/s], Decompressed: 8403
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 214 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 214 KB/s], Decompressed: 8455

lean_checker exit 0 duration 6m 45s · created 6/10/2026, 12:17:16 AM

lake build

⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (73s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:17095: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:17095:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17097:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17095: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:17095:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17098:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17095: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:17095:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17102: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:17095: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:17095:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17112:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17135: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:17137:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17135: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:17138:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17135: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:17141:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17135: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:17142:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17135: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:17143:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
✔ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.5s)
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.4s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.1s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (5.4s)
✔ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (4.4s)
✔ [3418/3425] Built Iut.Stage1.IUTStage1StepXI (18s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (204s)
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) [0x74aa3f3c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x74aa3f3bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x74aa3f3bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x74aa3f2f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x74aa3f2f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x74aa3f3caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x74aa3f232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x74aa3f232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x74aa3f233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x74aa3f2341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x74aa3f3c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x74aa3f015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74aa3f3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74aa3f3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x74aa3f39b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x74aa3f015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x74aa3a422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x74aa3a20cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x74aa39d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x74aa39d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x74aa36c4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x74aa36c45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x60604a40a8da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (9.6s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (46s)
✔ [3423/3425] Built Iut.Basic (2.7s)
✔ [3424/3425] Built Iut (2.6s)
Build completed successfully (3425 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

blueprint_build exit 1 duration 2s · created 6/10/2026, 12:17:16 AM

lake build :blueprint

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`

semantic_module_facts exit 0 duration 2h 6m · created 6/10/2026, 12:17:16 AM

./.apodeixis/tools/lean-semantic-extract.sh --module-facts

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: restored compiled static runner cache b8ade8a5a75badb2412ef674e9cf813e5e33dd881f43d8103f9aabc58695563a
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit - duration 4h 0m · created 6/10/2026, 12:17:16 AM

./.apodeixis/tools/lean-semantic-extract.sh

lean semantic helper: restored compiled static runner cache cce27869c0d4aaab5a9a11452cfb29f4952473614ca88d877d92ab8b59b7ba1f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-403-runtime-semantic_extract-1166115-1781036223384237695-9