Verification run

Run 634

promachina/iut-lean branch master triggered via poller

failed commit 01b0e097b89b 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-856-source
exit_code=Some(0) duration_ms=3264
stderr:
Cloning into '/var/lib/apodeixis/repos/job-856-source'...


$ git checkout 01b0e097b89ba21aed97eb63739f5075958dee0e
exit_code=Some(0) duration_ms=153
stderr:
Note: switching to '01b0e097b89ba21aed97eb63739f5075958dee0e'.

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 01b0e09 Lower formula gap controlled source

Resolved source revision: 01b0e097b89ba21aed97eb63739f5075958dee0e

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=01b0e097b89ba21aed97eb63739f5075958dee0e provenance={"branch":"master","checked_out_revision":"01b0e097b89ba21aed97eb63739f5075958dee0e","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"01b0e097b89ba21aed97eb63739f5075958dee0e","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=58875
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%, 2 KB/s], Decompressed: 13
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 30
Downloaded: 67 file(s) [attempted 67/8459 = 0%, 28 KB/s], Decompressed: 64
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 241 KB/s], Decompressed: 79
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 35 KB/s], Decompressed: 120
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 94 KB/s], Decompressed: 148
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 509 KB/s], Decompressed: 182
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 758 KB/s], Decompressed: 220
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 213 KB/s], Decompressed: 254
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 84 KB/s], Decompressed: 295
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 570 KB/s], Decompressed: 343
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 214 KB/s], Decompressed: 384
Downloaded: 431 file(s) [attempted 431/8459 = 5%, 134 KB/s], Decompressed: 422
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 830 KB/s], Decompressed: 460
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 105 KB/s], Decompressed: 497
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 333 KB/s], Decompressed: 538
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 186 KB/s], Decompressed: 576
Downloaded: 624 file(s) [attempted 624/8459 = 7%, 157 KB/s], Decompressed: 610
Downloaded: 662 file(s) [attempted 662/8459 = 7%, 150 KB/s], Decompressed: 658
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 186 KB/s], Decompressed: 696
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 78 KB/s], Decompressed: 734
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 163 KB/s], Decompressed: 778
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 495 KB/s], Decompressed: 816
Downloaded: 854 file(s) [attempted 854/8459 = 10%, 36 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 177 KB/s], Decompressed: 895
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 69 KB/s], Decompressed: 932
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 516 KB/s], Decompressed: 980
Downloaded: 1019 file(s) [attempted 1019/8459 = 12%, 177 KB/s], Decompressed: 1011
Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 171 KB/s], Decompressed: 1049
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 546 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 69 KB/s], Decompressed: 1134
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 123 KB/s], Decompressed: 1165
Downloaded: 1210 file(s) [attempted 1210/8459 = 14%, 483 KB/s], Decompressed: 1203
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 203 KB/s], Decompressed: 1237
Downloaded: 1285 file(s) [attempted 1285/8459 = 15%, 138 KB/s], Decompressed: 1281
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 301 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 136 KB/s], Decompressed: 1360
Downloaded: 1404 file(s) [attempted 1404/8459 = 16%, 235 KB/s], Decompressed: 1398
Downloaded: 1439 file(s) [attempted 1439/8459 = 17%, 159 KB/s], Decompressed: 1435
Downloaded: 1480 file(s) [attempted 1480/8459 = 17%, 269 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 53 KB/s], Decompressed: 1518
Downloaded: 1564 file(s) [attempted 1564/8459 = 18%, 57 KB/s], Decompressed: 1548
Downloaded: 1600 file(s) [attempted 1600/8459 = 18%, 104 KB/s], Decompressed: 1593
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 229 KB/s], Decompressed: 1631
Downloaded: 1678 file(s) [attempted 1678/8459 = 19%, 470 KB/s], Decompressed: 1672
Downloaded: 1721 file(s) [attempted 1721/8459 = 20%, 275 KB/s], Decompressed: 1713
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 255 KB/s], Decompressed: 1757
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 894 KB/s], Decompressed: 1791
Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 100 KB/s], Decompressed: 1829
Downloaded: 1871 file(s) [attempted 1871/8459 = 22%, 667 KB/s], Decompressed: 1867
Downloaded: 1911 file(s) [attempted 1911/8459 = 22%, 485 KB/s], Decompressed: 1908
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 768 KB/s], Decompressed: 1945
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 73 KB/s], Decompressed: 1980
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 161 KB/s], Decompressed: 2021
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 205 KB/s], Decompressed: 2062
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 53 KB/s], Decompressed: 2099
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 293 KB/s], Decompressed: 2141
Downloaded: 2188 file(s) [attempted 2188/8459 = 25%, 35 KB/s], Decompressed: 2185
Downloaded: 2229 file(s) [attempted 2229/8459 = 26%, 162 KB/s], Decompressed: 2223
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 63 KB/s], Decompressed: 2260
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 705 KB/s], Decompressed: 2294
Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 669 KB/s], Decompressed: 2342
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 258 KB/s], Decompressed: 2383
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 1252 KB/s], Decompressed: 2414
Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 358 KB/s], Decompressed: 2449
Downloaded: 2500 file(s) [attempted 2500/8459 = 29%, 336 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 159 KB/s], Decompressed: 2534
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 63 KB/s], Decompressed: 2568
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 23 KB/s], Decompressed: 2609
Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 535 KB/s], Decompressed: 2650
Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 766 KB/s], Decompressed: 2691
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 284 KB/s], Decompressed: 2729
Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 284 KB/s], Decompressed: 2770
Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 96 KB/s], Decompressed: 2811
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 323 KB/s], Decompressed: 2835
Downloaded: 2895 file(s) [attempted 2895/8459 = 34%, 521 KB/s], Decompressed: 2887
Downloaded: 2929 file(s) [attempted 2929/8459 = 34%, 369 KB/s], Decompressed: 2924
Downloaded: 2973 file(s) [attempted 2973/8459 = 35%, 97 KB/s], Decompressed: 2965
Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 461 KB/s], Decompressed: 3010
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 411 KB/s], Decompressed: 3047
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 363 KB/s], Decompressed: 3078
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 333 KB/s], Decompressed: 3119
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 66 KB/s], Decompressed: 3160
Downloaded: 3210 file(s) [attempted 3210/8459 = 37%, 1226 KB/s], Decompressed: 3201
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 219 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 100 KB/s], Decompressed: 3280
Downloaded: 3327 file(s) [attempted 3327/8459 = 39%, 1392 KB/s], Decompressed: 3321
Downloaded: 3369 file(s) [attempted 3369/8459 = 39%, 306 KB/s], Decompressed: 3359
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 192 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 48 KB/s], Decompressed: 3444
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 243 KB/s], Decompressed: 3482
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 81 KB/s], Decompressed: 3523
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 23 KB/s], Decompressed: 3564
Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 630 KB/s], Decompressed: 3605
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 245 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 52 KB/s], Decompressed: 3681
Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 987 KB/s], Decompressed: 3722
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 92 KB/s], Decompressed: 3766
Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 361 KB/s], Decompressed: 3814
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 206 KB/s], Decompressed: 3848
Downloaded: 3890 file(s) [attempted 3890/8459 = 45%, 416 KB/s], Decompressed: 3886
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 351 KB/s], Decompressed: 3927
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 434 KB/s], Decompressed: 3965
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 297 KB/s], Decompressed: 4006
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 277 KB/s], Decompressed: 4047
Downloaded: 4087 file(s) [attempted 4087/8459 = 48%, 52 KB/s], Decompressed: 4081
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 341 KB/s], Decompressed: 4119
Downloaded: 4167 file(s) [attempted 4167/8459 = 49%, 634 KB/s], Decompressed: 4156
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 1383 KB/s], Decompressed: 4201
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 505 KB/s], Decompressed: 4238
Downloaded: 4283 file(s) [attempted 4283/8459 = 50%, 209 KB/s], Decompressed: 4276
Downloaded: 4322 file(s) [attempted 4322/8459 = 51%, 775 KB/s], Decompressed: 4314
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 227 KB/s], Decompressed: 4355
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 169 KB/s], Decompressed: 4386
Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 112 KB/s], Decompressed: 4423
Downloaded: 4466 file(s) [attempted 4466/8459 = 52%, 591 KB/s], Decompressed: 4457
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 128 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 111 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 157 KB/s], Decompressed: 4581
Downloaded: 4622 file(s) [attempted 4622/8459 = 54%, 154 KB/s], Decompressed: 4618
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 112 KB/s], Decompressed: 4663
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 150 KB/s], Decompressed: 4704
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 233 KB/s], Decompressed: 4742
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 590 KB/s], Decompressed: 4783
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 238 KB/s], Decompressed: 4813
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 779 KB/s], Decompressed: 4858
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 168 KB/s], Decompressed: 4902
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 599 KB/s], Decompressed: 4937
Downloaded: 4985 file(s) [attempted 4985/8459 = 58%, 50 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 149 KB/s], Decompressed: 5019
Downloaded: 5061 file(s) [attempted 5061/8459 = 59%, 203 KB/s], Decompressed: 5056
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 739 KB/s], Decompressed: 5101
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 867 KB/s], Decompressed: 5142
Downloaded: 5181 file(s) [attempted 5181/8459 = 61%, 332 KB/s], Decompressed: 5176
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 326 KB/s], Decompressed: 5214
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 23 KB/s], Decompressed: 5255
Downloaded: 5303 file(s) [attempted 5303/8459 = 62%, 30 KB/s], Decompressed: 5296
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 146 KB/s], Decompressed: 5330
Downloaded: 5377 file(s) [attempted 5377/8459 = 63%, 881 KB/s], Decompressed: 5368
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 774 KB/s], Decompressed: 5409
Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 57 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 296 KB/s], Decompressed: 5498
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 39 KB/s], Decompressed: 5536
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 165 KB/s], Decompressed: 5566
Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 91 KB/s], Decompressed: 5611
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 155 KB/s], Decompressed: 5655
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 108 KB/s], Decompressed: 5693
Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 281 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 301 KB/s], Decompressed: 5765
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 654 KB/s], Decompressed: 5809
Downloaded: 5851 file(s) [attempted 5851/8459 = 69%, 591 KB/s], Decompressed: 5847
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 302 KB/s], Decompressed: 5878
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1041 KB/s], Decompressed: 5922
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 523 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 90 KB/s], Decompressed: 6001
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 19 KB/s], Decompressed: 6039
Downloaded: 6087 file(s) [attempted 6087/8459 = 71%, 350 KB/s], Decompressed: 6083
Downloaded: 6128 file(s) [attempted 6128/8459 = 72%, 85 KB/s], Decompressed: 6124
Downloaded: 6166 file(s) [attempted 6166/8459 = 72%, 160 KB/s], Decompressed: 6158
Downloaded: 6203 file(s) [attempted 6203/8459 = 73%, 509 KB/s], Decompressed: 6196
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 50 KB/s], Decompressed: 6234
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 571 KB/s], Decompressed: 6275
Downloaded: 6323 file(s) [attempted 6323/8459 = 74%, 445 KB/s], Decompressed: 6319
Downloaded: 6357 file(s) [attempted 6357/8459 = 75%, 83 KB/s], Decompressed: 6347
Downloaded: 6398 file(s) [attempted 6398/8459 = 75%, 163 KB/s], Decompressed: 6391
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 61 KB/s], Decompressed: 6429
Downloaded: 6474 file(s) [attempted 6474/8459 = 76%, 21 KB/s], Decompressed: 6470
Downloaded: 6515 file(s) [attempted 6515/8459 = 77%, 1687 KB/s], Decompressed: 6511
Downloaded: 6549 file(s) [attempted 6549/8459 = 77%, 102 KB/s], Decompressed: 6536
Downloaded: 6591 file(s) [attempted 6591/8459 = 77%, 126 KB/s], Decompressed: 6586
Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 108 KB/s], Decompressed: 6624
Downloaded: 6668 file(s) [attempted 6668/8459 = 78%, 391 KB/s], Decompressed: 6661
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 475 KB/s], Decompressed: 6703
Downloaded: 6744 file(s) [attempted 6744/8459 = 79%, 704 KB/s], Decompressed: 6740
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 472 KB/s], Decompressed: 6781
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 135 KB/s], Decompressed: 6822
Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 139 KB/s], Decompressed: 6860
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 819 KB/s], Decompressed: 6901
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 440 KB/s], Decompressed: 6939
Downloaded: 6977 file(s) [attempted 6977/8459 = 82%, 627 KB/s], Decompressed: 6973
Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 62 KB/s], Decompressed: 7011
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 313 KB/s], Decompressed: 7062
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 50 KB/s], Decompressed: 7106
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 426 KB/s], Decompressed: 7137
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 123 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 297 KB/s], Decompressed: 7219
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 265 KB/s], Decompressed: 7264
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 184 KB/s], Decompressed: 7301
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 537 KB/s], Decompressed: 7339
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 602 KB/s], Decompressed: 7373
Downloaded: 7419 file(s) [attempted 7419/8459 = 87%, 112 KB/s], Decompressed: 7408
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 67 KB/s], Decompressed: 7449
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 26 KB/s], Decompressed: 7493
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 525 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 165 KB/s], Decompressed: 7568
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 158 KB/s], Decompressed: 7616
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 150 KB/s], Decompressed: 7654
Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 253 KB/s], Decompressed: 7695
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 3048 KB/s], Decompressed: 7733
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 1605 KB/s], Decompressed: 7763
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 241 KB/s], Decompressed: 7808
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 304 KB/s], Decompressed: 7849
Downloaded: 7894 file(s) [attempted 7894/8459 = 93%, 55 KB/s], Decompressed: 7890
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 652 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 1931 KB/s], Decompressed: 7965
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 56 KB/s], Decompressed: 8010
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 61 KB/s], Decompressed: 8048
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 105 KB/s], Decompressed: 8082
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 721 KB/s], Decompressed: 8126
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 106 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 398 KB/s], Decompressed: 8212
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 140 KB/s], Decompressed: 8253
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 333 KB/s], Decompressed: 8290
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 209 KB/s], Decompressed: 8325
Downloaded: 8370 file(s) [attempted 8370/8459 = 98%, 288 KB/s], Decompressed: 8366
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 448 KB/s], Decompressed: 8407
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 456 KB/s], Decompressed: 8445
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 456 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=867432
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 (82s)
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 (92s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (253s)
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) [0x7c723b1c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7c723b1bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7c723b1bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7c723b0f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7c723b0f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7c723b1caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7c723b032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7c723b032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7c723b033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7c723b0341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7c723b1c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7c723ae15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7c723b1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7c723b1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7c723b19b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7c723ae15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7c7236222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7c723600cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7c7235b69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7c7235b69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7c7232a4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7c7232a45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x64fc5721e8da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (31s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (296s)
warning: Iut/Stage1/IUTStage1Experiments.lean:155824: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:156192: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:156933: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:157137: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) [0x7469c97c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7469c97bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7469c97bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7469c96eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7469c96ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7469c97caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7469c9632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7469c9632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7469c9633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7469c96341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7469c97c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7469c9415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7469c979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7469c9415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7469c4822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7469c460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7469c4169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7469c4169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7469c104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7469c1045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff16018c8da]
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) [0x7469c97c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7469c97bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7469c97bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7469c96f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7469c96f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7469c97caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7469c9632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7469c9632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7469c9633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7469c96341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7469c97c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7469c9415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7469c979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7469c9415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7469c4822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7469c460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7469c4169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7469c4169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7469c104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7469c1045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff16018c8da]
✔ [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=3121
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=14400005
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":3600}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1706,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"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":10836,"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 807bbaac492c3a81adf44fd99e7005f2fbd011cba04d217b25553ed2f1455359
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-856-runtime-semantic_extract-2193316-1782851326644305551-3

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=None duration_ms=14400015
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2639,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 807bbaac492c3a81adf44fd99e7005f2fbd011cba04d217b25553ed2f1455359
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":41,"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-856-runtime-semantic_extract-2193316-1782872314687928131-7

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=None duration_ms=3600010
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1601,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"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":107861,"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 a8a139eaa5337a1eb0db8aa76cc9ddee23d43be73fcf90f3094e82631b0e1a85
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-856-runtime-semantic_extract-2193316-1782894981517553391-9
Stored Lean workspace build cache

Command runs

git_clone exit 0 duration 3s · created 7/1/2026, 9:36:55 AM

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

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

git_checkout exit 0 duration 153 ms · created 7/1/2026, 9:36:55 AM

git checkout 01b0e097b89ba21aed97eb63739f5075958dee0e

Note: switching to '01b0e097b89ba21aed97eb63739f5075958dee0e'.

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 01b0e09 Lower formula gap controlled source

lake_cache exit 0 duration 59s · created 7/1/2026, 9:36:55 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%, 2 KB/s], Decompressed: 13
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 30
Downloaded: 67 file(s) [attempted 67/8459 = 0%, 28 KB/s], Decompressed: 64
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 241 KB/s], Decompressed: 79
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 35 KB/s], Decompressed: 120
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 94 KB/s], Decompressed: 148
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 509 KB/s], Decompressed: 182
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 758 KB/s], Decompressed: 220
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 213 KB/s], Decompressed: 254
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 84 KB/s], Decompressed: 295
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 570 KB/s], Decompressed: 343
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 214 KB/s], Decompressed: 384
Downloaded: 431 file(s) [attempted 431/8459 = 5%, 134 KB/s], Decompressed: 422
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 830 KB/s], Decompressed: 460
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 105 KB/s], Decompressed: 497
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 333 KB/s], Decompressed: 538
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 186 KB/s], Decompressed: 576
Downloaded: 624 file(s) [attempted 624/8459 = 7%, 157 KB/s], Decompressed: 610
Downloaded: 662 file(s) [attempted 662/8459 = 7%, 150 KB/s], Decompressed: 658
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 186 KB/s], Decompressed: 696
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 78 KB/s], Decompressed: 734
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 163 KB/s], Decompressed: 778
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 495 KB/s], Decompressed: 816
Downloaded: 854 file(s) [attempted 854/8459 = 10%, 36 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 177 KB/s], Decompressed: 895
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 69 KB/s], Decompressed: 932
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 516 KB/s], Decompressed: 980
Downloaded: 1019 file(s) [attempted 1019/8459 = 12%, 177 KB/s], Decompressed: 1011
Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 171 KB/s], Decompressed: 1049
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 546 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 69 KB/s], Decompressed: 1134
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 123 KB/s], Decompressed: 1165
Downloaded: 1210 file(s) [attempted 1210/8459 = 14%, 483 KB/s], Decompressed: 1203
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 203 KB/s], Decompressed: 1237
Downloaded: 1285 file(s) [attempted 1285/8459 = 15%, 138 KB/s], Decompressed: 1281
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 301 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 136 KB/s], Decompressed: 1360
Downloaded: 1404 file(s) [attempted 1404/8459 = 16%, 235 KB/s], Decompressed: 1398
Downloaded: 1439 file(s) [attempted 1439/8459 = 17%, 159 KB/s], Decompressed: 1435
Downloaded: 1480 file(s) [attempted 1480/8459 = 17%, 269 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 53 KB/s], Decompressed: 1518
Downloaded: 1564 file(s) [attempted 1564/8459 = 18%, 57 KB/s], Decompressed: 1548
Downloaded: 1600 file(s) [attempted 1600/8459 = 18%, 104 KB/s], Decompressed: 1593
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 229 KB/s], Decompressed: 1631
Downloaded: 1678 file(s) [attempted 1678/8459 = 19%, 470 KB/s], Decompressed: 1672
Downloaded: 1721 file(s) [attempted 1721/8459 = 20%, 275 KB/s], Decompressed: 1713
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 255 KB/s], Decompressed: 1757
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 894 KB/s], Decompressed: 1791
Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 100 KB/s], Decompressed: 1829
Downloaded: 1871 file(s) [attempted 1871/8459 = 22%, 667 KB/s], Decompressed: 1867
Downloaded: 1911 file(s) [attempted 1911/8459 = 22%, 485 KB/s], Decompressed: 1908
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 768 KB/s], Decompressed: 1945
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 73 KB/s], Decompressed: 1980
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 161 KB/s], Decompressed: 2021
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 205 KB/s], Decompressed: 2062
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 53 KB/s], Decompressed: 2099
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 293 KB/s], Decompressed: 2141
Downloaded: 2188 file(s) [attempted 2188/8459 = 25%, 35 KB/s], Decompressed: 2185
Downloaded: 2229 file(s) [attempted 2229/8459 = 26%, 162 KB/s], Decompressed: 2223
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 63 KB/s], Decompressed: 2260
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 705 KB/s], Decompressed: 2294
Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 669 KB/s], Decompressed: 2342
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 258 KB/s], Decompressed: 2383
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 1252 KB/s], Decompressed: 2414
Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 358 KB/s], Decompressed: 2449
Downloaded: 2500 file(s) [attempted 2500/8459 = 29%, 336 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 159 KB/s], Decompressed: 2534
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 63 KB/s], Decompressed: 2568
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 23 KB/s], Decompressed: 2609
Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 535 KB/s], Decompressed: 2650
Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 766 KB/s], Decompressed: 2691
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 284 KB/s], Decompressed: 2729
Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 284 KB/s], Decompressed: 2770
Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 96 KB/s], Decompressed: 2811
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 323 KB/s], Decompressed: 2835
Downloaded: 2895 file(s) [attempted 2895/8459 = 34%, 521 KB/s], Decompressed: 2887
Downloaded: 2929 file(s) [attempted 2929/8459 = 34%, 369 KB/s], Decompressed: 2924
Downloaded: 2973 file(s) [attempted 2973/8459 = 35%, 97 KB/s], Decompressed: 2965
Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 461 KB/s], Decompressed: 3010
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 411 KB/s], Decompressed: 3047
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 363 KB/s], Decompressed: 3078
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 333 KB/s], Decompressed: 3119
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 66 KB/s], Decompressed: 3160
Downloaded: 3210 file(s) [attempted 3210/8459 = 37%, 1226 KB/s], Decompressed: 3201
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 219 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 100 KB/s], Decompressed: 3280
Downloaded: 3327 file(s) [attempted 3327/8459 = 39%, 1392 KB/s], Decompressed: 3321
Downloaded: 3369 file(s) [attempted 3369/8459 = 39%, 306 KB/s], Decompressed: 3359
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 192 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 48 KB/s], Decompressed: 3444
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 243 KB/s], Decompressed: 3482
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 81 KB/s], Decompressed: 3523
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 23 KB/s], Decompressed: 3564
Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 630 KB/s], Decompressed: 3605
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 245 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 52 KB/s], Decompressed: 3681
Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 987 KB/s], Decompressed: 3722
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 92 KB/s], Decompressed: 3766
Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 361 KB/s], Decompressed: 3814
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 206 KB/s], Decompressed: 3848
Downloaded: 3890 file(s) [attempted 3890/8459 = 45%, 416 KB/s], Decompressed: 3886
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 351 KB/s], Decompressed: 3927
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 434 KB/s], Decompressed: 3965
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 297 KB/s], Decompressed: 4006
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 277 KB/s], Decompressed: 4047
Downloaded: 4087 file(s) [attempted 4087/8459 = 48%, 52 KB/s], Decompressed: 4081
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 341 KB/s], Decompressed: 4119
Downloaded: 4167 file(s) [attempted 4167/8459 = 49%, 634 KB/s], Decompressed: 4156
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 1383 KB/s], Decompressed: 4201
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 505 KB/s], Decompressed: 4238
Downloaded: 4283 file(s) [attempted 4283/8459 = 50%, 209 KB/s], Decompressed: 4276
Downloaded: 4322 file(s) [attempted 4322/8459 = 51%, 775 KB/s], Decompressed: 4314
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 227 KB/s], Decompressed: 4355
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 169 KB/s], Decompressed: 4386
Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 112 KB/s], Decompressed: 4423
Downloaded: 4466 file(s) [attempted 4466/8459 = 52%, 591 KB/s], Decompressed: 4457
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 128 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 111 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 157 KB/s], Decompressed: 4581
Downloaded: 4622 file(s) [attempted 4622/8459 = 54%, 154 KB/s], Decompressed: 4618
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 112 KB/s], Decompressed: 4663
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 150 KB/s], Decompressed: 4704
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 233 KB/s], Decompressed: 4742
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 590 KB/s], Decompressed: 4783
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 238 KB/s], Decompressed: 4813
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 779 KB/s], Decompressed: 4858
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 168 KB/s], Decompressed: 4902
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 599 KB/s], Decompressed: 4937
Downloaded: 4985 file(s) [attempted 4985/8459 = 58%, 50 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 149 KB/s], Decompressed: 5019
Downloaded: 5061 file(s) [attempted 5061/8459 = 59%, 203 KB/s], Decompressed: 5056
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 739 KB/s], Decompressed: 5101
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 867 KB/s], Decompressed: 5142
Downloaded: 5181 file(s) [attempted 5181/8459 = 61%, 332 KB/s], Decompressed: 5176
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 326 KB/s], Decompressed: 5214
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 23 KB/s], Decompressed: 5255
Downloaded: 5303 file(s) [attempted 5303/8459 = 62%, 30 KB/s], Decompressed: 5296
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 146 KB/s], Decompressed: 5330
Downloaded: 5377 file(s) [attempted 5377/8459 = 63%, 881 KB/s], Decompressed: 5368
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 774 KB/s], Decompressed: 5409
Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 57 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 296 KB/s], Decompressed: 5498
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 39 KB/s], Decompressed: 5536
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 165 KB/s], Decompressed: 5566
Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 91 KB/s], Decompressed: 5611
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 155 KB/s], Decompressed: 5655
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 108 KB/s], Decompressed: 5693
Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 281 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 301 KB/s], Decompressed: 5765
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 654 KB/s], Decompressed: 5809
Downloaded: 5851 file(s) [attempted 5851/8459 = 69%, 591 KB/s], Decompressed: 5847
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 302 KB/s], Decompressed: 5878
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1041 KB/s], Decompressed: 5922
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 523 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 90 KB/s], Decompressed: 6001
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 19 KB/s], Decompressed: 6039
Downloaded: 6087 file(s) [attempted 6087/8459 = 71%, 350 KB/s], Decompressed: 6083
Downloaded: 6128 file(s) [attempted 6128/8459 = 72%, 85 KB/s], Decompressed: 6124
Downloaded: 6166 file(s) [attempted 6166/8459 = 72%, 160 KB/s], Decompressed: 6158
Downloaded: 6203 file(s) [attempted 6203/8459 = 73%, 509 KB/s], Decompressed: 6196
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 50 KB/s], Decompressed: 6234
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 571 KB/s], Decompressed: 6275
Downloaded: 6323 file(s) [attempted 6323/8459 = 74%, 445 KB/s], Decompressed: 6319
Downloaded: 6357 file(s) [attempted 6357/8459 = 75%, 83 KB/s], Decompressed: 6347
Downloaded: 6398 file(s) [attempted 6398/8459 = 75%, 163 KB/s], Decompressed: 6391
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 61 KB/s], Decompressed: 6429
Downloaded: 6474 file(s) [attempted 6474/8459 = 76%, 21 KB/s], Decompressed: 6470
Downloaded: 6515 file(s) [attempted 6515/8459 = 77%, 1687 KB/s], Decompressed: 6511
Downloaded: 6549 file(s) [attempted 6549/8459 = 77%, 102 KB/s], Decompressed: 6536
Downloaded: 6591 file(s) [attempted 6591/8459 = 77%, 126 KB/s], Decompressed: 6586
Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 108 KB/s], Decompressed: 6624
Downloaded: 6668 file(s) [attempted 6668/8459 = 78%, 391 KB/s], Decompressed: 6661
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 475 KB/s], Decompressed: 6703
Downloaded: 6744 file(s) [attempted 6744/8459 = 79%, 704 KB/s], Decompressed: 6740
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 472 KB/s], Decompressed: 6781
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 135 KB/s], Decompressed: 6822
Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 139 KB/s], Decompressed: 6860
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 819 KB/s], Decompressed: 6901
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 440 KB/s], Decompressed: 6939
Downloaded: 6977 file(s) [attempted 6977/8459 = 82%, 627 KB/s], Decompressed: 6973
Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 62 KB/s], Decompressed: 7011
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 313 KB/s], Decompressed: 7062
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 50 KB/s], Decompressed: 7106
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 426 KB/s], Decompressed: 7137
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 123 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 297 KB/s], Decompressed: 7219
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 265 KB/s], Decompressed: 7264
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 184 KB/s], Decompressed: 7301
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 537 KB/s], Decompressed: 7339
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 602 KB/s], Decompressed: 7373
Downloaded: 7419 file(s) [attempted 7419/8459 = 87%, 112 KB/s], Decompressed: 7408
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 67 KB/s], Decompressed: 7449
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 26 KB/s], Decompressed: 7493
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 525 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 165 KB/s], Decompressed: 7568
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 158 KB/s], Decompressed: 7616
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 150 KB/s], Decompressed: 7654
Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 253 KB/s], Decompressed: 7695
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 3048 KB/s], Decompressed: 7733
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 1605 KB/s], Decompressed: 7763
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 241 KB/s], Decompressed: 7808
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 304 KB/s], Decompressed: 7849
Downloaded: 7894 file(s) [attempted 7894/8459 = 93%, 55 KB/s], Decompressed: 7890
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 652 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 1931 KB/s], Decompressed: 7965
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 56 KB/s], Decompressed: 8010
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 61 KB/s], Decompressed: 8048
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 105 KB/s], Decompressed: 8082
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 721 KB/s], Decompressed: 8126
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 106 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 398 KB/s], Decompressed: 8212
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 140 KB/s], Decompressed: 8253
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 333 KB/s], Decompressed: 8290
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 209 KB/s], Decompressed: 8325
Downloaded: 8370 file(s) [attempted 8370/8459 = 98%, 288 KB/s], Decompressed: 8366
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 448 KB/s], Decompressed: 8407
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 456 KB/s], Decompressed: 8445
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 456 KB/s], Decompressed: 8455

lean_checker exit 0 duration 14m 27s · created 7/1/2026, 9:36:55 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 (82s)
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 (92s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (253s)
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) [0x7c723b1c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7c723b1bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7c723b1bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7c723b0f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7c723b0f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7c723b1caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7c723b032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7c723b032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7c723b033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7c723b0341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7c723b1c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7c723ae15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7c723b1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7c723b1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7c723b19b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7c723ae15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7c7236222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7c723600cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7c7235b69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7c7235b69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7c7232a4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7c7232a45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x64fc5721e8da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (31s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (296s)
warning: Iut/Stage1/IUTStage1Experiments.lean:155824: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:156192: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:156933: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:157137: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) [0x7469c97c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7469c97bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7469c97bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x7469c96eba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x7469c96ebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7469c97caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7469c9632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7469c9632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7469c9633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7469c96341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7469c97c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7469c9415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7469c979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7469c9415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7469c4822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7469c460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7469c4169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7469c4169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7469c104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7469c1045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff16018c8da]
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) [0x7469c97c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7469c97bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7469c97bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7469c96f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7469c96f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7469c97caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7469c9632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7469c9632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7469c9633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7469c96341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7469c97c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7469c9415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7469c97c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7469c979b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7469c9415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7469c4822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7469c460cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7469c4169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7469c4169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7469c104524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7469c1045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff16018c8da]
✔ [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/1/2026, 9:36:55 AM

lake build :blueprint

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

semantic_extract exit - duration 4h 0m · created 7/1/2026, 9:36:55 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":3600}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1706,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"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":10836,"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 807bbaac492c3a81adf44fd99e7005f2fbd011cba04d217b25553ed2f1455359
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-856-runtime-semantic_extract-2193316-1782851326644305551-3

semantic_extract exit - duration 4h 0m · created 7/1/2026, 9:36:55 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2639,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 807bbaac492c3a81adf44fd99e7005f2fbd011cba04d217b25553ed2f1455359
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":41,"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-856-runtime-semantic_extract-2193316-1782872314687928131-7

semantic_extract exit - duration 1h 0m · created 7/1/2026, 9:36:55 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":1601,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"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":107861,"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 a8a139eaa5337a1eb0db8aa76cc9ddee23d43be73fcf90f3094e82631b0e1a85
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-856-runtime-semantic_extract-2193316-1782894981517553391-9