Verification run

Run 635

promachina/iut-lean branch master triggered via poller

failed commit 2b8e256cba8a toolchain lean-v4-30-0 prover lean took 13h 27m · finished 2w ago

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset) failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: <command argv unavailable>)

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

$ git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-861-source
exit_code=Some(0) duration_ms=3327
stderr:
Cloning into '/var/lib/apodeixis/repos/job-861-source'...


$ git checkout 2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6
exit_code=Some(0) duration_ms=134
stderr:
Note: switching to '2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6'.

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 2b8e256 Add milestone completion audit

Resolved source revision: 2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6 provenance={"branch":"master","checked_out_revision":"2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 shared Lean git mirror alias(es)
Lean semantic module cache: computed 31 module hash fact(s) from source and olean files; skipping Lean module-facts probe
Lean semantic module cache: 23/31 module hit(s), 8 miss(es)
Lean semantic module cache: stable superset runner maps 8 missing module(s) to 7 weighted target group(s) capped at target weight 32, but will attempt them in one Lean invocation
Lean semantic module cache: trying stable superset runner for 8 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: stable superset runner target set maps to 7 weighted batch(es), but will run in one Lean invocation so the superset import is paid once
Lean semantic module cache: stable superset runner failed with timeout after checkpointing 3 completed module(s); falling back for 5 remaining module(s)
Lean semantic module cache: stable superset runner timed out for extract-stable-superset; retrying 5 remaining module(s) across 5 stable target retry batch(es): [1, 1, 1, 1, 1]
Lean semantic module cache: checkpointed 1 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 1 missing module(s) in one Lean invocation
Lean semantic module cache: checkpointed 1 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 1 missing module(s) in one Lean invocation
Lean semantic module cache: checkpointed 1 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 1 missing module(s) in one Lean invocation
Lean semantic module cache: stable superset runner failed with timeout; falling back
Lean semantic module cache: checkpointed 1 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 1 missing module(s) in one Lean invocation
Lean semantic module cache: stable superset runner fell back to exact-module batches
Lean semantic module cache: capping exact extraction batch extract-batch-00000 at 3600s; total exact budget remaining is 43200s
Lean semantic module cache: extraction batch extract-batch-00000 failed for module Iut/Stage1/IUTStage1Experiments.lean; continuing with remaining modules
Lean semantic module cache: extraction batch extract-batch-00000 did not fully complete; continuing with remaining batches
Lean semantic module cache: extracted 0 module fragment(s) before one or more module failures; leaving full semantic response unwritten

$ lake exe cache get
exit_code=Some(0) duration_ms=60062
stdout:
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)

stderr:
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%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 13 KB/s], Decompressed: 36
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 26 KB/s], Decompressed: 59
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 191 KB/s], Decompressed: 78
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 314 KB/s], Decompressed: 123
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 119 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 298 KB/s], Decompressed: 196
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 409 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 149 KB/s], Decompressed: 254
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 24 KB/s], Decompressed: 306
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 49 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 183 KB/s], Decompressed: 388
Downloaded: 434 file(s) [attempted 434/8459 = 5%, 245 KB/s], Decompressed: 429
Downloaded: 467 file(s) [attempted 467/8459 = 5%, 153 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 761 KB/s], Decompressed: 497
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 28 KB/s], Decompressed: 545
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 805 KB/s], Decompressed: 583
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 74 KB/s], Decompressed: 621
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 89 KB/s], Decompressed: 662
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 82 KB/s], Decompressed: 703
Downloaded: 744 file(s) [attempted 744/8459 = 8%, 171 KB/s], Decompressed: 737
Downloaded: 785 file(s) [attempted 785/8459 = 9%, 100 KB/s], Decompressed: 778
Downloaded: 823 file(s) [attempted 823/8459 = 9%, 165 KB/s], Decompressed: 819
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 384 KB/s], Decompressed: 860
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 302 KB/s], Decompressed: 908
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 317 KB/s], Decompressed: 943
Downloaded: 985 file(s) [attempted 985/8459 = 11%, 107 KB/s], Decompressed: 980
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 155 KB/s], Decompressed: 1021
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 213 KB/s], Decompressed: 1066
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 350 KB/s], Decompressed: 1107
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 350 KB/s], Decompressed: 1134
Downloaded: 1181 file(s) [attempted 1181/8459 = 13%, 346 KB/s], Decompressed: 1175
Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 240 KB/s], Decompressed: 1220
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 28 KB/s], Decompressed: 1258
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 791 KB/s], Decompressed: 1302
Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 1117 KB/s], Decompressed: 1333
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 1121 KB/s], Decompressed: 1370
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 373 KB/s], Decompressed: 1401
Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 102 KB/s], Decompressed: 1449
Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 189 KB/s], Decompressed: 1490
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 25 KB/s], Decompressed: 1518
Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 992 KB/s], Decompressed: 1566
Downloaded: 1607 file(s) [attempted 1607/8459 = 18%, 156 KB/s], Decompressed: 1603
Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 411 KB/s], Decompressed: 1641
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 345 KB/s], Decompressed: 1678
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 282 KB/s], Decompressed: 1716
Downloaded: 1764 file(s) [attempted 1764/8459 = 20%, 129 KB/s], Decompressed: 1757
Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 185 KB/s], Decompressed: 1802
Downloaded: 1841 file(s) [attempted 1841/8459 = 21%, 105 KB/s], Decompressed: 1836
Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 499 KB/s], Decompressed: 1870
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 371 KB/s], Decompressed: 1915
Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 200 KB/s], Decompressed: 1952
Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 124 KB/s], Decompressed: 1986
Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 456 KB/s], Decompressed: 2028
Downloaded: 2075 file(s) [attempted 2075/8459 = 24%, 251 KB/s], Decompressed: 2072
Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 346 KB/s], Decompressed: 2106
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 483 KB/s], Decompressed: 2154
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 132 KB/s], Decompressed: 2188
Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 129 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 138 KB/s], Decompressed: 2271
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 108 KB/s], Decompressed: 2308
Downloaded: 2355 file(s) [attempted 2355/8459 = 27%, 322 KB/s], Decompressed: 2342
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 256 KB/s], Decompressed: 2383
Downloaded: 2428 file(s) [attempted 2428/8459 = 28%, 378 KB/s], Decompressed: 2425
Downloaded: 2465 file(s) [attempted 2465/8459 = 29%, 54 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 85 KB/s], Decompressed: 2496
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 120 KB/s], Decompressed: 2544
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 106 KB/s], Decompressed: 2575
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 162 KB/s], Decompressed: 2613
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 186 KB/s], Decompressed: 2654
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 249 KB/s], Decompressed: 2692
Downloaded: 2734 file(s) [attempted 2734/8459 = 32%, 299 KB/s], Decompressed: 2726
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 245 KB/s], Decompressed: 2767
Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 98 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 262 KB/s], Decompressed: 2846
Downloaded: 2893 file(s) [attempted 2893/8459 = 34%, 522 KB/s], Decompressed: 2890
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 643 KB/s], Decompressed: 2931
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 806 KB/s], Decompressed: 2966
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 40 KB/s], Decompressed: 3000
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 156 KB/s], Decompressed: 3037
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 301 KB/s], Decompressed: 3085
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 100 KB/s], Decompressed: 3126
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 660 KB/s], Decompressed: 3160
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 230 KB/s], Decompressed: 3198
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 1378 KB/s], Decompressed: 3246
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 225 KB/s], Decompressed: 3287
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 198 KB/s], Decompressed: 3325
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 888 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 618 KB/s], Decompressed: 3403
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 251 KB/s], Decompressed: 3441
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 231 KB/s], Decompressed: 3482
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 63 KB/s], Decompressed: 3520
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 467 KB/s], Decompressed: 3564
Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 402 KB/s], Decompressed: 3605
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 314 KB/s], Decompressed: 3639
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 52 KB/s], Decompressed: 3681
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 278 KB/s], Decompressed: 3725
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 1338 KB/s], Decompressed: 3766
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 216 KB/s], Decompressed: 3790
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 546 KB/s], Decompressed: 3838
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 423 KB/s], Decompressed: 3879
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 149 KB/s], Decompressed: 3917
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 30 KB/s], Decompressed: 3961
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 32 KB/s], Decompressed: 3995
Downloaded: 4043 file(s) [attempted 4043/8459 = 47%, 591 KB/s], Decompressed: 4040
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 246 KB/s], Decompressed: 4078
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 339 KB/s], Decompressed: 4112
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 238 KB/s], Decompressed: 4149
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 208 KB/s], Decompressed: 4187
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 235 KB/s], Decompressed: 4235
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 536 KB/s], Decompressed: 4273
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 60 KB/s], Decompressed: 4307
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 926 KB/s], Decompressed: 4348
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 221 KB/s], Decompressed: 4386
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 121 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 753 KB/s], Decompressed: 4461
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 376 KB/s], Decompressed: 4505
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 924 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 148 KB/s], Decompressed: 4577
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 1037 KB/s], Decompressed: 4622
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 107 KB/s], Decompressed: 4664
Downloaded: 4702 file(s) [attempted 4702/8459 = 55%, 196 KB/s], Decompressed: 4687
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 226 KB/s], Decompressed: 4731
Downloaded: 4780 file(s) [attempted 4780/8459 = 56%, 280 KB/s], Decompressed: 4776
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 40 KB/s], Decompressed: 4820
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 191 KB/s], Decompressed: 4854
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 493 KB/s], Decompressed: 4892
Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 163 KB/s], Decompressed: 4930
Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 56 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 401 KB/s], Decompressed: 5019
Downloaded: 5060 file(s) [attempted 5060/8459 = 59%, 45 KB/s], Decompressed: 5046
Downloaded: 5094 file(s) [attempted 5094/8459 = 60%, 832 KB/s], Decompressed: 5091
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 591 KB/s], Decompressed: 5121
Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 1311 KB/s], Decompressed: 5169
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 121 KB/s], Decompressed: 5214
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 23 KB/s], Decompressed: 5251
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 56 KB/s], Decompressed: 5293
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 187 KB/s], Decompressed: 5330
Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 332 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 218 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 70 KB/s], Decompressed: 5457
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 958 KB/s], Decompressed: 5494
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 277 KB/s], Decompressed: 5539
Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 155 KB/s], Decompressed: 5577
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 188 KB/s], Decompressed: 5614
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 223 KB/s], Decompressed: 5659
Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 460 KB/s], Decompressed: 5700
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 37 KB/s], Decompressed: 5731
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 78 KB/s], Decompressed: 5779
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 308 KB/s], Decompressed: 5816
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 74 KB/s], Decompressed: 5857
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 325 KB/s], Decompressed: 5898
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 286 KB/s], Decompressed: 5939
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 248 KB/s], Decompressed: 5980
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 262 KB/s], Decompressed: 6021
Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 932 KB/s], Decompressed: 6056
Downloaded: 6098 file(s) [attempted 6098/8459 = 72%, 56 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 253 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 138 KB/s], Decompressed: 6179
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 295 KB/s], Decompressed: 6210
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 87 KB/s], Decompressed: 6247
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 236 KB/s], Decompressed: 6288
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 348 KB/s], Decompressed: 6326
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 671 KB/s], Decompressed: 6371
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 284 KB/s], Decompressed: 6408
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 260 KB/s], Decompressed: 6449
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 73 KB/s], Decompressed: 6494
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 600 KB/s], Decompressed: 6535
Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 1833 KB/s], Decompressed: 6583
Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 55 KB/s], Decompressed: 6624
Downloaded: 6663 file(s) [attempted 6663/8459 = 78%, 739 KB/s], Decompressed: 6658
Downloaded: 6701 file(s) [attempted 6701/8459 = 79%, 103 KB/s], Decompressed: 6696
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 286 KB/s], Decompressed: 6737
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 88 KB/s], Decompressed: 6781
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 123 KB/s], Decompressed: 6815
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 75 KB/s], Decompressed: 6860
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 316 KB/s], Decompressed: 6894
Downloaded: 6941 file(s) [attempted 6941/8459 = 82%, 406 KB/s], Decompressed: 6934
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 605 KB/s], Decompressed: 6973
Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 108 KB/s], Decompressed: 7014
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 292 KB/s], Decompressed: 7055
Downloaded: 7095 file(s) [attempted 7095/8459 = 83%, 632 KB/s], Decompressed: 7089
Downloaded: 7131 file(s) [attempted 7131/8459 = 84%, 79 KB/s], Decompressed: 7128
Downloaded: 7168 file(s) [attempted 7168/8459 = 84%, 992 KB/s], Decompressed: 7165
Downloaded: 7209 file(s) [attempted 7209/8459 = 85%, 696 KB/s], Decompressed: 7206
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 833 KB/s], Decompressed: 7236
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 427 KB/s], Decompressed: 7284
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 221 KB/s], Decompressed: 7312
Downloaded: 7361 file(s) [attempted 7361/8459 = 87%, 152 KB/s], Decompressed: 7356
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 279 KB/s], Decompressed: 7397
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 108 KB/s], Decompressed: 7435
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 578 KB/s], Decompressed: 7466
Downloaded: 7514 file(s) [attempted 7514/8459 = 88%, 459 KB/s], Decompressed: 7510
Downloaded: 7555 file(s) [attempted 7555/8459 = 89%, 110 KB/s], Decompressed: 7551
Downloaded: 7596 file(s) [attempted 7596/8459 = 89%, 299 KB/s], Decompressed: 7592
Downloaded: 7634 file(s) [attempted 7634/8459 = 90%, 174 KB/s], Decompressed: 7630
Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 63 KB/s], Decompressed: 7668
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 121 KB/s], Decompressed: 7709
Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 164 KB/s], Decompressed: 7746
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 890 KB/s], Decompressed: 7791
Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 1430 KB/s], Decompressed: 7832
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 639 KB/s], Decompressed: 7866
Downloaded: 7913 file(s) [attempted 7913/8459 = 93%, 831 KB/s], Decompressed: 7904
Downloaded: 7947 file(s) [attempted 7947/8459 = 93%, 173 KB/s], Decompressed: 7941
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 595 KB/s], Decompressed: 7986
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 279 KB/s], Decompressed: 8027
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 34 KB/s], Decompressed: 8061
Downloaded: 8106 file(s) [attempted 8106/8459 = 95%, 69 KB/s], Decompressed: 8102
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 70 KB/s], Decompressed: 8140
Downloaded: 8189 file(s) [attempted 8189/8459 = 96%, 253 KB/s], Decompressed: 8184
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 484 KB/s], Decompressed: 8219
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 76 KB/s], Decompressed: 8256
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 123 KB/s], Decompressed: 8294
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 687 KB/s], Decompressed: 8338
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 53 KB/s], Decompressed: 8379
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 650 KB/s], Decompressed: 8414
Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 505 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 505 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=918490
stdout:
⚠ [3410/3425] Replayed Iut.Stage1.IUTStage1SourceCore
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17140:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17141:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17145: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:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17155:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17180:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17181:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17184:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17185:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17186:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
⚠ [3412/3425] Replayed Iut.Stage1.IUTStage1IUTIVAlgebra
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (86s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4517:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4522:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4654:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4686:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4691:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4734:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4788:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4823:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4828:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4960:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4994:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4999:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5137:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5171:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5176:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5319:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5351:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5356:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5469:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7524:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15276:100: This line exceeds the 100 character limit, please shorten it!

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [3418/3425] Built Iut.Stage1.IUTStage1StepXI (88s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (278s)
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) [0x71f19ebc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x71f19ebbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x71f19ebbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x71f19eaf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x71f19eaf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x71f19ebcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x71f19ea32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x71f19ea32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x71f19ea33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x71f19ea341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x71f19ebc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x71f19e815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71f19ebc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71f19ebc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x71f19eb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x71f19e815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x71f199c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x71f199a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x71f199569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x71f199569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x71f19644524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x71f196445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x619eac0458da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (42s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (309s)
warning: Iut/Stage1/IUTStage1Experiments.lean:157346:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:157714:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:158455:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:158659:100: This line exceeds the 100 character limit, please shorten it!

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

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x72b4b57c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x72b4b57bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x72b4b57bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x72b4b56eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x72b4b56ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x72b4b57caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x72b4b5632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x72b4b5632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x72b4b5633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x72b4b56341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x72b4b57c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x72b4b5415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72b4b579b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x72b4b5415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x72b4b0822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72b4b060cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x72b4b0169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x72b4b0169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72b4b5c5324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72b4b5c53305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cc64ba698da]
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) [0x72b4b57c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x72b4b57bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x72b4b57bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x72b4b56f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x72b4b56f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x72b4b57caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x72b4b5632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x72b4b5632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x72b4b5633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x72b4b56341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x72b4b57c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x72b4b5415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72b4b579b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x72b4b5415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x72b4b0822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72b4b060cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x72b4b0169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x72b4b0169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72b4b5c5324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72b4b5c53305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cc64ba698da]
✔ [3423/3425] Built Iut.Basic (74s)
✔ [3424/3425] Built Iut (2.6s)
Build completed successfully (3425 jobs).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=3130
stderr:
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`


blueprint_build failed; continuing (non-fatal phase).

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
exit_code=None duration_ms=14400007
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3547}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1636,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":10388,"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 966ba2529555816167d921673666be6b01bab0cf0ff3d47bf8bdf486b0350898
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-861-runtime-semantic_extract-2546638-1782911731169359399-3

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=None duration_ms=14400009
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":5788,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 966ba2529555816167d921673666be6b01bab0cf0ff3d47bf8bdf486b0350898
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":30,"runner_cache_hit":true}
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-861-runtime-semantic_extract-2546638-1782932718684438666-7

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=None duration_ms=3600009
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1133,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":111478,"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 2978386f23bc9d652a81eeb2edbd4070cbeb9482e6c42dcc2d5db957cff92665
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 3600s
podman cleanup removed verifier container apx-verifier-job-861-runtime-semantic_extract-2546638-1782955335993885699-9
Stored Lean workspace build cache

Command runs

lake_cache exit 0 duration 1m 0s · created 7/2/2026, 2:23:01 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%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 13 KB/s], Decompressed: 36
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 26 KB/s], Decompressed: 59
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 191 KB/s], Decompressed: 78
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 314 KB/s], Decompressed: 123
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 119 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 298 KB/s], Decompressed: 196
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 409 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 149 KB/s], Decompressed: 254
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 24 KB/s], Decompressed: 306
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 49 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 183 KB/s], Decompressed: 388
Downloaded: 434 file(s) [attempted 434/8459 = 5%, 245 KB/s], Decompressed: 429
Downloaded: 467 file(s) [attempted 467/8459 = 5%, 153 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 761 KB/s], Decompressed: 497
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 28 KB/s], Decompressed: 545
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 805 KB/s], Decompressed: 583
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 74 KB/s], Decompressed: 621
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 89 KB/s], Decompressed: 662
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 82 KB/s], Decompressed: 703
Downloaded: 744 file(s) [attempted 744/8459 = 8%, 171 KB/s], Decompressed: 737
Downloaded: 785 file(s) [attempted 785/8459 = 9%, 100 KB/s], Decompressed: 778
Downloaded: 823 file(s) [attempted 823/8459 = 9%, 165 KB/s], Decompressed: 819
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 384 KB/s], Decompressed: 860
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 302 KB/s], Decompressed: 908
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 317 KB/s], Decompressed: 943
Downloaded: 985 file(s) [attempted 985/8459 = 11%, 107 KB/s], Decompressed: 980
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 155 KB/s], Decompressed: 1021
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 213 KB/s], Decompressed: 1066
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 350 KB/s], Decompressed: 1107
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 350 KB/s], Decompressed: 1134
Downloaded: 1181 file(s) [attempted 1181/8459 = 13%, 346 KB/s], Decompressed: 1175
Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 240 KB/s], Decompressed: 1220
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 28 KB/s], Decompressed: 1258
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 791 KB/s], Decompressed: 1302
Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 1117 KB/s], Decompressed: 1333
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 1121 KB/s], Decompressed: 1370
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 373 KB/s], Decompressed: 1401
Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 102 KB/s], Decompressed: 1449
Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 189 KB/s], Decompressed: 1490
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 25 KB/s], Decompressed: 1518
Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 992 KB/s], Decompressed: 1566
Downloaded: 1607 file(s) [attempted 1607/8459 = 18%, 156 KB/s], Decompressed: 1603
Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 411 KB/s], Decompressed: 1641
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 345 KB/s], Decompressed: 1678
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 282 KB/s], Decompressed: 1716
Downloaded: 1764 file(s) [attempted 1764/8459 = 20%, 129 KB/s], Decompressed: 1757
Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 185 KB/s], Decompressed: 1802
Downloaded: 1841 file(s) [attempted 1841/8459 = 21%, 105 KB/s], Decompressed: 1836
Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 499 KB/s], Decompressed: 1870
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 371 KB/s], Decompressed: 1915
Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 200 KB/s], Decompressed: 1952
Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 124 KB/s], Decompressed: 1986
Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 456 KB/s], Decompressed: 2028
Downloaded: 2075 file(s) [attempted 2075/8459 = 24%, 251 KB/s], Decompressed: 2072
Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 346 KB/s], Decompressed: 2106
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 483 KB/s], Decompressed: 2154
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 132 KB/s], Decompressed: 2188
Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 129 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 138 KB/s], Decompressed: 2271
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 108 KB/s], Decompressed: 2308
Downloaded: 2355 file(s) [attempted 2355/8459 = 27%, 322 KB/s], Decompressed: 2342
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 256 KB/s], Decompressed: 2383
Downloaded: 2428 file(s) [attempted 2428/8459 = 28%, 378 KB/s], Decompressed: 2425
Downloaded: 2465 file(s) [attempted 2465/8459 = 29%, 54 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 85 KB/s], Decompressed: 2496
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 120 KB/s], Decompressed: 2544
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 106 KB/s], Decompressed: 2575
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 162 KB/s], Decompressed: 2613
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 186 KB/s], Decompressed: 2654
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 249 KB/s], Decompressed: 2692
Downloaded: 2734 file(s) [attempted 2734/8459 = 32%, 299 KB/s], Decompressed: 2726
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 245 KB/s], Decompressed: 2767
Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 98 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 262 KB/s], Decompressed: 2846
Downloaded: 2893 file(s) [attempted 2893/8459 = 34%, 522 KB/s], Decompressed: 2890
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 643 KB/s], Decompressed: 2931
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 806 KB/s], Decompressed: 2966
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 40 KB/s], Decompressed: 3000
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 156 KB/s], Decompressed: 3037
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 301 KB/s], Decompressed: 3085
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 100 KB/s], Decompressed: 3126
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 660 KB/s], Decompressed: 3160
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 230 KB/s], Decompressed: 3198
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 1378 KB/s], Decompressed: 3246
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 225 KB/s], Decompressed: 3287
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 198 KB/s], Decompressed: 3325
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 888 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 618 KB/s], Decompressed: 3403
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 251 KB/s], Decompressed: 3441
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 231 KB/s], Decompressed: 3482
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 63 KB/s], Decompressed: 3520
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 467 KB/s], Decompressed: 3564
Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 402 KB/s], Decompressed: 3605
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 314 KB/s], Decompressed: 3639
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 52 KB/s], Decompressed: 3681
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 278 KB/s], Decompressed: 3725
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 1338 KB/s], Decompressed: 3766
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 216 KB/s], Decompressed: 3790
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 546 KB/s], Decompressed: 3838
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 423 KB/s], Decompressed: 3879
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 149 KB/s], Decompressed: 3917
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 30 KB/s], Decompressed: 3961
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 32 KB/s], Decompressed: 3995
Downloaded: 4043 file(s) [attempted 4043/8459 = 47%, 591 KB/s], Decompressed: 4040
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 246 KB/s], Decompressed: 4078
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 339 KB/s], Decompressed: 4112
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 238 KB/s], Decompressed: 4149
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 208 KB/s], Decompressed: 4187
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 235 KB/s], Decompressed: 4235
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 536 KB/s], Decompressed: 4273
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 60 KB/s], Decompressed: 4307
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 926 KB/s], Decompressed: 4348
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 221 KB/s], Decompressed: 4386
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 121 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 753 KB/s], Decompressed: 4461
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 376 KB/s], Decompressed: 4505
Downloaded: 4543 file(s) [attempted 4543/8459 = 53%, 924 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 148 KB/s], Decompressed: 4577
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 1037 KB/s], Decompressed: 4622
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 107 KB/s], Decompressed: 4664
Downloaded: 4702 file(s) [attempted 4702/8459 = 55%, 196 KB/s], Decompressed: 4687
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 226 KB/s], Decompressed: 4731
Downloaded: 4780 file(s) [attempted 4780/8459 = 56%, 280 KB/s], Decompressed: 4776
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 40 KB/s], Decompressed: 4820
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 191 KB/s], Decompressed: 4854
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 493 KB/s], Decompressed: 4892
Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 163 KB/s], Decompressed: 4930
Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 56 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 401 KB/s], Decompressed: 5019
Downloaded: 5060 file(s) [attempted 5060/8459 = 59%, 45 KB/s], Decompressed: 5046
Downloaded: 5094 file(s) [attempted 5094/8459 = 60%, 832 KB/s], Decompressed: 5091
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 591 KB/s], Decompressed: 5121
Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 1311 KB/s], Decompressed: 5169
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 121 KB/s], Decompressed: 5214
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 23 KB/s], Decompressed: 5251
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 56 KB/s], Decompressed: 5293
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 187 KB/s], Decompressed: 5330
Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 332 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 218 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 70 KB/s], Decompressed: 5457
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 958 KB/s], Decompressed: 5494
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 277 KB/s], Decompressed: 5539
Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 155 KB/s], Decompressed: 5577
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 188 KB/s], Decompressed: 5614
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 223 KB/s], Decompressed: 5659
Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 460 KB/s], Decompressed: 5700
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 37 KB/s], Decompressed: 5731
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 78 KB/s], Decompressed: 5779
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 308 KB/s], Decompressed: 5816
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 74 KB/s], Decompressed: 5857
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 325 KB/s], Decompressed: 5898
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 286 KB/s], Decompressed: 5939
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 248 KB/s], Decompressed: 5980
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 262 KB/s], Decompressed: 6021
Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 932 KB/s], Decompressed: 6056
Downloaded: 6098 file(s) [attempted 6098/8459 = 72%, 56 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 253 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 138 KB/s], Decompressed: 6179
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 295 KB/s], Decompressed: 6210
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 87 KB/s], Decompressed: 6247
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 236 KB/s], Decompressed: 6288
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 348 KB/s], Decompressed: 6326
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 671 KB/s], Decompressed: 6371
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 284 KB/s], Decompressed: 6408
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 260 KB/s], Decompressed: 6449
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 73 KB/s], Decompressed: 6494
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 600 KB/s], Decompressed: 6535
Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 1833 KB/s], Decompressed: 6583
Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 55 KB/s], Decompressed: 6624
Downloaded: 6663 file(s) [attempted 6663/8459 = 78%, 739 KB/s], Decompressed: 6658
Downloaded: 6701 file(s) [attempted 6701/8459 = 79%, 103 KB/s], Decompressed: 6696
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 286 KB/s], Decompressed: 6737
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 88 KB/s], Decompressed: 6781
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 123 KB/s], Decompressed: 6815
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 75 KB/s], Decompressed: 6860
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 316 KB/s], Decompressed: 6894
Downloaded: 6941 file(s) [attempted 6941/8459 = 82%, 406 KB/s], Decompressed: 6934
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 605 KB/s], Decompressed: 6973
Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 108 KB/s], Decompressed: 7014
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 292 KB/s], Decompressed: 7055
Downloaded: 7095 file(s) [attempted 7095/8459 = 83%, 632 KB/s], Decompressed: 7089
Downloaded: 7131 file(s) [attempted 7131/8459 = 84%, 79 KB/s], Decompressed: 7128
Downloaded: 7168 file(s) [attempted 7168/8459 = 84%, 992 KB/s], Decompressed: 7165
Downloaded: 7209 file(s) [attempted 7209/8459 = 85%, 696 KB/s], Decompressed: 7206
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 833 KB/s], Decompressed: 7236
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 427 KB/s], Decompressed: 7284
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 221 KB/s], Decompressed: 7312
Downloaded: 7361 file(s) [attempted 7361/8459 = 87%, 152 KB/s], Decompressed: 7356
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 279 KB/s], Decompressed: 7397
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 108 KB/s], Decompressed: 7435
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 578 KB/s], Decompressed: 7466
Downloaded: 7514 file(s) [attempted 7514/8459 = 88%, 459 KB/s], Decompressed: 7510
Downloaded: 7555 file(s) [attempted 7555/8459 = 89%, 110 KB/s], Decompressed: 7551
Downloaded: 7596 file(s) [attempted 7596/8459 = 89%, 299 KB/s], Decompressed: 7592
Downloaded: 7634 file(s) [attempted 7634/8459 = 90%, 174 KB/s], Decompressed: 7630
Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 63 KB/s], Decompressed: 7668
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 121 KB/s], Decompressed: 7709
Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 164 KB/s], Decompressed: 7746
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 890 KB/s], Decompressed: 7791
Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 1430 KB/s], Decompressed: 7832
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 639 KB/s], Decompressed: 7866
Downloaded: 7913 file(s) [attempted 7913/8459 = 93%, 831 KB/s], Decompressed: 7904
Downloaded: 7947 file(s) [attempted 7947/8459 = 93%, 173 KB/s], Decompressed: 7941
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 595 KB/s], Decompressed: 7986
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 279 KB/s], Decompressed: 8027
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 34 KB/s], Decompressed: 8061
Downloaded: 8106 file(s) [attempted 8106/8459 = 95%, 69 KB/s], Decompressed: 8102
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 70 KB/s], Decompressed: 8140
Downloaded: 8189 file(s) [attempted 8189/8459 = 96%, 253 KB/s], Decompressed: 8184
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 484 KB/s], Decompressed: 8219
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 76 KB/s], Decompressed: 8256
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 123 KB/s], Decompressed: 8294
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 687 KB/s], Decompressed: 8338
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 53 KB/s], Decompressed: 8379
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 650 KB/s], Decompressed: 8414
Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 505 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 505 KB/s], Decompressed: 8455

lean_checker exit 0 duration 15m 18s · created 7/2/2026, 2:23:01 AM

lake build

⚠ [3410/3425] Replayed Iut.Stage1.IUTStage1SourceCore
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17140:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17141:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17145: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:17138: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:17138:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:17155:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17180:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17181:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17184:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17185:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:17178: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:17186:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
⚠ [3412/3425] Replayed Iut.Stage1.IUTStage1IUTIVAlgebra
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (86s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4517:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4522:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4654:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4686:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4691:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4734:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4788:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4823:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4828:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4960:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4994:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4999:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5137:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5171:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5176:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5319:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5351:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5356:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5469:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7524:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15276:100: This line exceeds the 100 character limit, please shorten it!

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

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [3418/3425] Built Iut.Stage1.IUTStage1StepXI (88s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (278s)
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) [0x71f19ebc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x71f19ebbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x71f19ebbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x71f19eaf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x71f19eaf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x71f19ebcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x71f19ea32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x71f19ea32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x71f19ea33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x71f19ea341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x71f19ebc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x71f19e815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71f19ebc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71f19ebc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x71f19eb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x71f19e815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x71f199c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x71f199a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x71f199569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x71f199569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x71f19644524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x71f196445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x619eac0458da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (42s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (309s)
warning: Iut/Stage1/IUTStage1Experiments.lean:157346:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:157714:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:158455:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Experiments.lean:158659:100: This line exceeds the 100 character limit, please shorten it!

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

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x72b4b57c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x72b4b57bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x72b4b57bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x72b4b56eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x72b4b56ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x72b4b57caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x72b4b5632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x72b4b5632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x72b4b5633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x72b4b56341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x72b4b57c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x72b4b5415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72b4b579b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x72b4b5415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x72b4b0822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72b4b060cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x72b4b0169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x72b4b0169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72b4b5c5324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72b4b5c53305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cc64ba698da]
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) [0x72b4b57c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x72b4b57bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x72b4b57bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x72b4b56f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x72b4b56f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x72b4b57caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x72b4b5632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x72b4b5632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x72b4b5633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x72b4b56341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x72b4b57c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x72b4b5415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x72b4b57c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72b4b579b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x72b4b5415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x72b4b0822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72b4b060cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x72b4b0169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x72b4b0169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72b4b5c5324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72b4b5c53305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cc64ba698da]
✔ [3423/3425] Built Iut.Basic (74s)
✔ [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 3s · created 7/2/2026, 2:23:01 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`

git_clone exit 0 duration 3s · created 7/2/2026, 2:23:01 AM

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

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

git_checkout exit 0 duration 134 ms · created 7/2/2026, 2:23:01 AM

git checkout 2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6

Note: switching to '2b8e256cba8ae4e82d1a2d8bd574dfbbb66803e6'.

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 2b8e256 Add milestone completion audit

semantic_extract exit - duration 4h 0m · created 7/2/2026, 2:23:01 AM

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

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3547}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1636,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":10388,"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 966ba2529555816167d921673666be6b01bab0cf0ff3d47bf8bdf486b0350898
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-861-runtime-semantic_extract-2546638-1782911731169359399-3

semantic_extract exit - duration 4h 0m · created 7/2/2026, 2:23:01 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":5788,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 966ba2529555816167d921673666be6b01bab0cf0ff3d47bf8bdf486b0350898
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":30,"runner_cache_hit":true}
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-861-runtime-semantic_extract-2546638-1782932718684438666-7

semantic_extract exit - duration 1h 0m · created 7/2/2026, 2:23:01 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1133,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":111478,"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 2978386f23bc9d652a81eeb2edbd4070cbeb9482e6c42dcc2d5db957cff92665
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 3600s
podman cleanup removed verifier container apx-verifier-job-861-runtime-semantic_extract-2546638-1782955335993885699-9