Verification run

Run 539

promachina/iut-lean branch master triggered via poller

failed commit dc997b5c90dc toolchain lean-v4-30-0 prover lean took 13h 6m · 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-758-source
exit_code=Some(0) duration_ms=3112
stderr:
Cloning into '/var/lib/apodeixis/repos/job-758-source'...


$ git checkout dc997b5c90dcd8cd24ba49503a06b34f384fbb39
exit_code=Some(0) duration_ms=139
stderr:
Note: switching to 'dc997b5c90dcd8cd24ba49503a06b34f384fbb39'.

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 dc997b5 Lower compact-open endpoint to arithmetic divisors

Resolved source revision: dc997b5c90dcd8cd24ba49503a06b34f384fbb39

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=dc997b5c90dcd8cd24ba49503a06b34f384fbb39 provenance={"branch":"master","checked_out_revision":"dc997b5c90dcd8cd24ba49503a06b34f384fbb39","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"dc997b5c90dcd8cd24ba49503a06b34f384fbb39","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: 24/31 module hit(s), 7 miss(es)
Lean semantic module cache: stable superset runner maps 7 missing module(s) to 6 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 7 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: stable superset runner target set maps to 6 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 4 remaining module(s)
Lean semantic module cache: stable superset runner timed out for extract-stable-superset; retrying 4 remaining module(s) across 4 stable target retry batch(es): [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: 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=74663
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%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 29 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 347 KB/s], Decompressed: 61
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 433 KB/s], Decompressed: 82
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 24 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 145
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 150 KB/s], Decompressed: 165
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 787 KB/s], Decompressed: 165
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 264 KB/s], Decompressed: 172
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 24 KB/s], Decompressed: 306
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 27 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 313 KB/s], Decompressed: 381
Downloaded: 422 file(s) [attempted 422/8459 = 4%, 294 KB/s], Decompressed: 408
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 59 KB/s], Decompressed: 454
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 179 KB/s], Decompressed: 497
Downloaded: 538 file(s) [attempted 538/8459 = 6%, 302 KB/s], Decompressed: 535
Downloaded: 576 file(s) [attempted 576/8459 = 6%, 551 KB/s], Decompressed: 569
Downloaded: 614 file(s) [attempted 614/8459 = 7%, 61 KB/s], Decompressed: 604
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 331 KB/s], Decompressed: 648
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 194 KB/s], Decompressed: 693
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 240 KB/s], Decompressed: 741
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 128 KB/s], Decompressed: 788
Downloaded: 839 file(s) [attempted 839/8459 = 9%, 194 KB/s], Decompressed: 830
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 36 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 44 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 353 KB/s], Decompressed: 946
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 203 KB/s], Decompressed: 987
Downloaded: 1035 file(s) [attempted 1035/8459 = 12%, 107 KB/s], Decompressed: 1021
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 267 KB/s], Decompressed: 1032
Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 61 KB/s], Decompressed: 1032
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 371 KB/s], Decompressed: 1042
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 179 KB/s], Decompressed: 1042
Downloaded: 1227 file(s) [attempted 1227/8459 = 14%, 278 KB/s], Decompressed: 1127
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 35 KB/s], Decompressed: 1254
Downloaded: 1302 file(s) [attempted 1302/8459 = 15%, 182 KB/s], Decompressed: 1295
Downloaded: 1344 file(s) [attempted 1344/8459 = 15%, 44 KB/s], Decompressed: 1340
Downloaded: 1381 file(s) [attempted 1381/8459 = 16%, 472 KB/s], Decompressed: 1377
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 73 KB/s], Decompressed: 1412
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 316 KB/s], Decompressed: 1456
Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 181 KB/s], Decompressed: 1490
Downloaded: 1536 file(s) [attempted 1536/8459 = 18%, 119 KB/s], Decompressed: 1507
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 313 KB/s], Decompressed: 1507
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 323 KB/s], Decompressed: 1617
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 347 KB/s], Decompressed: 1658
Downloaded: 1695 file(s) [attempted 1695/8459 = 20%, 461 KB/s], Decompressed: 1689
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 433 KB/s], Decompressed: 1726
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 704 KB/s], Decompressed: 1771
Downloaded: 1815 file(s) [attempted 1815/8459 = 21%, 160 KB/s], Decompressed: 1788
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 31 KB/s], Decompressed: 1788
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 137 KB/s], Decompressed: 1795
Downloaded: 1926 file(s) [attempted 1926/8459 = 22%, 69 KB/s], Decompressed: 1921
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 155 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 74 KB/s], Decompressed: 1990
Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 237 KB/s], Decompressed: 2041
Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 228 KB/s], Decompressed: 2075
Downloaded: 2115 file(s) [attempted 2115/8459 = 25%, 116 KB/s], Decompressed: 2106
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 161 KB/s], Decompressed: 2151
Downloaded: 2193 file(s) [attempted 2193/8459 = 25%, 207 KB/s], Decompressed: 2188
Downloaded: 2229 file(s) [attempted 2229/8459 = 26%, 321 KB/s], Decompressed: 2223
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 97 KB/s], Decompressed: 2257
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 186 KB/s], Decompressed: 2295
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 237 KB/s], Decompressed: 2336
Downloaded: 2385 file(s) [attempted 2385/8459 = 28%, 447 KB/s], Decompressed: 2370
Downloaded: 2425 file(s) [attempted 2425/8459 = 28%, 394 KB/s], Decompressed: 2411
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 91 KB/s], Decompressed: 2452
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 77 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 562 KB/s], Decompressed: 2531
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 53 KB/s], Decompressed: 2572
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 2292 KB/s], Decompressed: 2606
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 1224 KB/s], Decompressed: 2647
Downloaded: 2692 file(s) [attempted 2692/8459 = 31%, 333 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 67 KB/s], Decompressed: 2722
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 333 KB/s], Decompressed: 2763
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 996 KB/s], Decompressed: 2798
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 175 KB/s], Decompressed: 2832
Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 79 KB/s], Decompressed: 2832
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 121 KB/s], Decompressed: 2832
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 144 KB/s], Decompressed: 2839
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 900 KB/s], Decompressed: 2839
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 212 KB/s], Decompressed: 2839
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 111 KB/s], Decompressed: 2839
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 181 KB/s], Decompressed: 3088
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 300 KB/s], Decompressed: 3154
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 23 KB/s], Decompressed: 3177
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 189 KB/s], Decompressed: 3177
Downloaded: 3275 file(s) [attempted 3275/8459 = 38%, 895 KB/s], Decompressed: 3184
Downloaded: 3310 file(s) [attempted 3310/8459 = 39%, 162 KB/s], Decompressed: 3304
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 480 KB/s], Decompressed: 3346
Downloaded: 3392 file(s) [attempted 3392/8459 = 40%, 584 KB/s], Decompressed: 3379
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 109 KB/s], Decompressed: 3427
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 92 KB/s], Decompressed: 3465
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 715 KB/s], Decompressed: 3506
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 227 KB/s], Decompressed: 3547
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 260 KB/s], Decompressed: 3588
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 58 KB/s], Decompressed: 3626
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 199 KB/s], Decompressed: 3633
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 163 KB/s], Decompressed: 3633
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 825 KB/s], Decompressed: 3742
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 121 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 430 KB/s], Decompressed: 3831
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 116 KB/s], Decompressed: 3862
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 54 KB/s], Decompressed: 3913
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 109 KB/s], Decompressed: 3954
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 183 KB/s], Decompressed: 3992
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 97 KB/s], Decompressed: 4009
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 731 KB/s], Decompressed: 4009
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 207 KB/s], Decompressed: 4095
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 44 KB/s], Decompressed: 4153
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 319 KB/s], Decompressed: 4187
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 235 KB/s], Decompressed: 4235
Downloaded: 4278 file(s) [attempted 4278/8459 = 50%, 336 KB/s], Decompressed: 4269
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 427 KB/s], Decompressed: 4310
Downloaded: 4352 file(s) [attempted 4352/8459 = 51%, 222 KB/s], Decompressed: 4345
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 183 KB/s], Decompressed: 4389
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 97 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 50 KB/s], Decompressed: 4468
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 286 KB/s], Decompressed: 4481
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 292 KB/s], Decompressed: 4481
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 587 KB/s], Decompressed: 4574
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 92 KB/s], Decompressed: 4574
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 103 KB/s], Decompressed: 4574
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 156 KB/s], Decompressed: 4574
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 260 KB/s], Decompressed: 4574
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 340 KB/s], Decompressed: 4786
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 168 KB/s], Decompressed: 4824
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 186 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 443 KB/s], Decompressed: 4906
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 416 KB/s], Decompressed: 4940
Downloaded: 4981 file(s) [attempted 4981/8459 = 58%, 53 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 150 KB/s], Decompressed: 5019
Downloaded: 5060 file(s) [attempted 5060/8459 = 59%, 198 KB/s], Decompressed: 5056
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 717 KB/s], Decompressed: 5097
Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 874 KB/s], Decompressed: 5132
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 86 KB/s], Decompressed: 5173
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 121 KB/s], Decompressed: 5207
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 86 KB/s], Decompressed: 5248
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 55 KB/s], Decompressed: 5289
Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 195 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 1073 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 504 KB/s], Decompressed: 5405
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 161 KB/s], Decompressed: 5443
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 153 KB/s], Decompressed: 5477
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 161 KB/s], Decompressed: 5515
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 305 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 165 KB/s], Decompressed: 5635
Downloaded: 5675 file(s) [attempted 5675/8459 = 67%, 313 KB/s], Decompressed: 5666
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 190 KB/s], Decompressed: 5696
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 436 KB/s], Decompressed: 5744
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 39 KB/s], Decompressed: 5789
Downloaded: 5832 file(s) [attempted 5832/8459 = 68%, 168 KB/s], Decompressed: 5826
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5861
Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 428 KB/s], Decompressed: 5902
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 97 KB/s], Decompressed: 5943
Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 143 KB/s], Decompressed: 5987
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 139 KB/s], Decompressed: 6018
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 352 KB/s], Decompressed: 6063
Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 302 KB/s], Decompressed: 6104
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 1182 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 193 KB/s], Decompressed: 6186
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 138 KB/s], Decompressed: 6223
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 47 KB/s], Decompressed: 6265
Downloaded: 6308 file(s) [attempted 6308/8459 = 74%, 1151 KB/s], Decompressed: 6299
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 2872 KB/s], Decompressed: 6333
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 414 KB/s], Decompressed: 6384
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 198 KB/s], Decompressed: 6432
Downloaded: 6486 file(s) [attempted 6486/8459 = 76%, 14 KB/s], Decompressed: 6480
Downloaded: 6528 file(s) [attempted 6528/8459 = 77%, 435 KB/s], Decompressed: 6521
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 133 KB/s], Decompressed: 6566
Downloaded: 6602 file(s) [attempted 6602/8459 = 78%, 229 KB/s], Decompressed: 6593
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 243 KB/s], Decompressed: 6631
Downloaded: 6679 file(s) [attempted 6679/8459 = 78%, 146 KB/s], Decompressed: 6675
Downloaded: 6724 file(s) [attempted 6724/8459 = 79%, 754 KB/s], Decompressed: 6720
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 424 KB/s], Decompressed: 6754
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 138 KB/s], Decompressed: 6795
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 227 KB/s], Decompressed: 6836
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 592 KB/s], Decompressed: 6874
Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 190 KB/s], Decompressed: 6918
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 186 KB/s], Decompressed: 6956
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 95 KB/s], Decompressed: 6997
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 324 KB/s], Decompressed: 7045
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 45 KB/s], Decompressed: 7079
Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 23 KB/s], Decompressed: 7117
Downloaded: 7165 file(s) [attempted 7165/8459 = 84%, 446 KB/s], Decompressed: 7161
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 141 KB/s], Decompressed: 7199
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 293 KB/s], Decompressed: 7213
Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 105 KB/s], Decompressed: 7213
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 71 KB/s], Decompressed: 7315
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 287 KB/s], Decompressed: 7360
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 2250 KB/s], Decompressed: 7401
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 313 KB/s], Decompressed: 7449
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 160 KB/s], Decompressed: 7497
Downloaded: 7545 file(s) [attempted 7545/8459 = 89%, 760 KB/s], Decompressed: 7541
Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 149 KB/s], Decompressed: 7562
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 103 KB/s], Decompressed: 7569
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 200 KB/s], Decompressed: 7569
Downloaded: 7699 file(s) [attempted 7699/8459 = 91%, 245 KB/s], Decompressed: 7668
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 152 KB/s], Decompressed: 7668
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 603 KB/s], Decompressed: 7767
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 91 KB/s], Decompressed: 7815
Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 23 KB/s], Decompressed: 7853
Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 182 KB/s], Decompressed: 7894
Downloaded: 7942 file(s) [attempted 7942/8459 = 93%, 543 KB/s], Decompressed: 7938
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 211 KB/s], Decompressed: 7976
Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 147 KB/s], Decompressed: 8010
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 112 KB/s], Decompressed: 8044
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 206 KB/s], Decompressed: 8089
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 8133
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 277 KB/s], Decompressed: 8171
Downloaded: 8213 file(s) [attempted 8213/8459 = 97%, 88 KB/s], Decompressed: 8209
Downloaded: 8250 file(s) [attempted 8250/8459 = 97%, 1630 KB/s], Decompressed: 8246
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 304 KB/s], Decompressed: 8277
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 522 KB/s], Decompressed: 8325
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 452 KB/s], Decompressed: 8366
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 789 KB/s], Decompressed: 8400
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 921 KB/s], Decompressed: 8445
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 921 KB/s], Decompressed: 8452


$ lake build
exit_code=Some(0) duration_ms=1046563
stdout:
✔ [763/767] Built Iut.Foundations.QualitativeData (51s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (64s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.6s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (66s)
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 `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
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`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.1s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.1s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (14s)
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 (75s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (249s)
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) [0x7523e73c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7523e73bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7523e73bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7523e72f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7523e72f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7523e73caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7523e7232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7523e7232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7523e7233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7523e72341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7523e73c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7523e7015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7523e73c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7523e73c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7523e739b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7523e7015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7523e2422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7523e220cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7523e1d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7523e1d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7523dec4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7523dec45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff0806b38da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (82s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (209s)
warning: Iut/Stage1/IUTStage1Experiments.lean:144902: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:145270: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:145573: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:145777: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) [0x73c458bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c458bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c458bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x73c458aeba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x73c458aebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c458bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c458a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c458a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c458a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c458a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c458bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c458815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c458b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c458815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c453c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c453a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c453569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c453569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c45044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c450445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5834994b68da]
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) [0x73c458bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c458bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c458bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73c458af3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73c458af4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c458bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c458a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c458a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c458a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c458a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c458bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c458815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c458b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c458815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c453c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c453a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c453569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c453569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c45044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c450445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5834994b68da]
✔ [3423/3425] Built Iut.Basic (119s)
✔ [3424/3425] Built Iut (2.5s)
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=4154
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=14400004
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":7307}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2518,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":34731,"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 8264080301d566477fc64f3fdb9b472b7b9ce44dbb4c4f3786edc619dc259e5f
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-758-runtime-semantic_extract-50135-1782733816438405570-3

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=None duration_ms=14400009
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2879,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8264080301d566477fc64f3fdb9b472b7b9ce44dbb4c4f3786edc619dc259e5f
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":34,"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-758-runtime-semantic_extract-50135-1782761561371415808-7

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=None duration_ms=3600009
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":569,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":6854,"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 9e064258683b242a3a660bddd3901e7015729e94727d64beb0545b59033ff32c
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-758-runtime-semantic_extract-50135-1782775972226152658-8
Stored Lean workspace build cache

Command runs

git_clone exit 0 duration 3s · created 6/30/2026, 12:33:28 AM

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

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

git_checkout exit 0 duration 139 ms · created 6/30/2026, 12:33:28 AM

git checkout dc997b5c90dcd8cd24ba49503a06b34f384fbb39

Note: switching to 'dc997b5c90dcd8cd24ba49503a06b34f384fbb39'.

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 dc997b5 Lower compact-open endpoint to arithmetic divisors

lake_cache exit 0 duration 1m 15s · created 6/30/2026, 12:33:28 AM

lake exe cache get

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

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 29 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 347 KB/s], Decompressed: 61
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 433 KB/s], Decompressed: 82
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 24 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 145
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 150 KB/s], Decompressed: 165
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 787 KB/s], Decompressed: 165
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 264 KB/s], Decompressed: 172
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 24 KB/s], Decompressed: 306
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 27 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 313 KB/s], Decompressed: 381
Downloaded: 422 file(s) [attempted 422/8459 = 4%, 294 KB/s], Decompressed: 408
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 59 KB/s], Decompressed: 454
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 179 KB/s], Decompressed: 497
Downloaded: 538 file(s) [attempted 538/8459 = 6%, 302 KB/s], Decompressed: 535
Downloaded: 576 file(s) [attempted 576/8459 = 6%, 551 KB/s], Decompressed: 569
Downloaded: 614 file(s) [attempted 614/8459 = 7%, 61 KB/s], Decompressed: 604
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 331 KB/s], Decompressed: 648
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 194 KB/s], Decompressed: 693
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 240 KB/s], Decompressed: 741
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 128 KB/s], Decompressed: 788
Downloaded: 839 file(s) [attempted 839/8459 = 9%, 194 KB/s], Decompressed: 830
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 36 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 44 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 353 KB/s], Decompressed: 946
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 203 KB/s], Decompressed: 987
Downloaded: 1035 file(s) [attempted 1035/8459 = 12%, 107 KB/s], Decompressed: 1021
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 267 KB/s], Decompressed: 1032
Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 61 KB/s], Decompressed: 1032
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 371 KB/s], Decompressed: 1042
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 179 KB/s], Decompressed: 1042
Downloaded: 1227 file(s) [attempted 1227/8459 = 14%, 278 KB/s], Decompressed: 1127
Downloaded: 1264 file(s) [attempted 1264/8459 = 14%, 35 KB/s], Decompressed: 1254
Downloaded: 1302 file(s) [attempted 1302/8459 = 15%, 182 KB/s], Decompressed: 1295
Downloaded: 1344 file(s) [attempted 1344/8459 = 15%, 44 KB/s], Decompressed: 1340
Downloaded: 1381 file(s) [attempted 1381/8459 = 16%, 472 KB/s], Decompressed: 1377
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 73 KB/s], Decompressed: 1412
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 316 KB/s], Decompressed: 1456
Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 181 KB/s], Decompressed: 1490
Downloaded: 1536 file(s) [attempted 1536/8459 = 18%, 119 KB/s], Decompressed: 1507
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 313 KB/s], Decompressed: 1507
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 323 KB/s], Decompressed: 1617
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 347 KB/s], Decompressed: 1658
Downloaded: 1695 file(s) [attempted 1695/8459 = 20%, 461 KB/s], Decompressed: 1689
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 433 KB/s], Decompressed: 1726
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 704 KB/s], Decompressed: 1771
Downloaded: 1815 file(s) [attempted 1815/8459 = 21%, 160 KB/s], Decompressed: 1788
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 31 KB/s], Decompressed: 1788
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 137 KB/s], Decompressed: 1795
Downloaded: 1926 file(s) [attempted 1926/8459 = 22%, 69 KB/s], Decompressed: 1921
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 155 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 74 KB/s], Decompressed: 1990
Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 237 KB/s], Decompressed: 2041
Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 228 KB/s], Decompressed: 2075
Downloaded: 2115 file(s) [attempted 2115/8459 = 25%, 116 KB/s], Decompressed: 2106
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 161 KB/s], Decompressed: 2151
Downloaded: 2193 file(s) [attempted 2193/8459 = 25%, 207 KB/s], Decompressed: 2188
Downloaded: 2229 file(s) [attempted 2229/8459 = 26%, 321 KB/s], Decompressed: 2223
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 97 KB/s], Decompressed: 2257
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 186 KB/s], Decompressed: 2295
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 237 KB/s], Decompressed: 2336
Downloaded: 2385 file(s) [attempted 2385/8459 = 28%, 447 KB/s], Decompressed: 2370
Downloaded: 2425 file(s) [attempted 2425/8459 = 28%, 394 KB/s], Decompressed: 2411
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 91 KB/s], Decompressed: 2452
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 77 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 562 KB/s], Decompressed: 2531
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 53 KB/s], Decompressed: 2572
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 2292 KB/s], Decompressed: 2606
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 1224 KB/s], Decompressed: 2647
Downloaded: 2692 file(s) [attempted 2692/8459 = 31%, 333 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 67 KB/s], Decompressed: 2722
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 333 KB/s], Decompressed: 2763
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 996 KB/s], Decompressed: 2798
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 175 KB/s], Decompressed: 2832
Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 79 KB/s], Decompressed: 2832
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 121 KB/s], Decompressed: 2832
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 144 KB/s], Decompressed: 2839
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 900 KB/s], Decompressed: 2839
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 212 KB/s], Decompressed: 2839
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 111 KB/s], Decompressed: 2839
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 181 KB/s], Decompressed: 3088
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 300 KB/s], Decompressed: 3154
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 23 KB/s], Decompressed: 3177
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 189 KB/s], Decompressed: 3177
Downloaded: 3275 file(s) [attempted 3275/8459 = 38%, 895 KB/s], Decompressed: 3184
Downloaded: 3310 file(s) [attempted 3310/8459 = 39%, 162 KB/s], Decompressed: 3304
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 480 KB/s], Decompressed: 3346
Downloaded: 3392 file(s) [attempted 3392/8459 = 40%, 584 KB/s], Decompressed: 3379
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 109 KB/s], Decompressed: 3427
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 92 KB/s], Decompressed: 3465
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 715 KB/s], Decompressed: 3506
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 227 KB/s], Decompressed: 3547
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 260 KB/s], Decompressed: 3588
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 58 KB/s], Decompressed: 3626
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 199 KB/s], Decompressed: 3633
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 163 KB/s], Decompressed: 3633
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 825 KB/s], Decompressed: 3742
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 121 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 430 KB/s], Decompressed: 3831
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 116 KB/s], Decompressed: 3862
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 54 KB/s], Decompressed: 3913
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 109 KB/s], Decompressed: 3954
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 183 KB/s], Decompressed: 3992
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 97 KB/s], Decompressed: 4009
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 731 KB/s], Decompressed: 4009
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 207 KB/s], Decompressed: 4095
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 44 KB/s], Decompressed: 4153
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 319 KB/s], Decompressed: 4187
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 235 KB/s], Decompressed: 4235
Downloaded: 4278 file(s) [attempted 4278/8459 = 50%, 336 KB/s], Decompressed: 4269
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 427 KB/s], Decompressed: 4310
Downloaded: 4352 file(s) [attempted 4352/8459 = 51%, 222 KB/s], Decompressed: 4345
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 183 KB/s], Decompressed: 4389
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 97 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 50 KB/s], Decompressed: 4468
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 286 KB/s], Decompressed: 4481
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 292 KB/s], Decompressed: 4481
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 587 KB/s], Decompressed: 4574
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 92 KB/s], Decompressed: 4574
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 103 KB/s], Decompressed: 4574
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 156 KB/s], Decompressed: 4574
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 260 KB/s], Decompressed: 4574
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 340 KB/s], Decompressed: 4786
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 168 KB/s], Decompressed: 4824
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 186 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 443 KB/s], Decompressed: 4906
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 416 KB/s], Decompressed: 4940
Downloaded: 4981 file(s) [attempted 4981/8459 = 58%, 53 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 150 KB/s], Decompressed: 5019
Downloaded: 5060 file(s) [attempted 5060/8459 = 59%, 198 KB/s], Decompressed: 5056
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 717 KB/s], Decompressed: 5097
Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 874 KB/s], Decompressed: 5132
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 86 KB/s], Decompressed: 5173
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 121 KB/s], Decompressed: 5207
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 86 KB/s], Decompressed: 5248
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 55 KB/s], Decompressed: 5289
Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 195 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 1073 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 504 KB/s], Decompressed: 5405
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 161 KB/s], Decompressed: 5443
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 153 KB/s], Decompressed: 5477
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 161 KB/s], Decompressed: 5515
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 305 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 165 KB/s], Decompressed: 5635
Downloaded: 5675 file(s) [attempted 5675/8459 = 67%, 313 KB/s], Decompressed: 5666
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 190 KB/s], Decompressed: 5696
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 436 KB/s], Decompressed: 5744
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 39 KB/s], Decompressed: 5789
Downloaded: 5832 file(s) [attempted 5832/8459 = 68%, 168 KB/s], Decompressed: 5826
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5861
Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 428 KB/s], Decompressed: 5902
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 97 KB/s], Decompressed: 5943
Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 143 KB/s], Decompressed: 5987
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 139 KB/s], Decompressed: 6018
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 352 KB/s], Decompressed: 6063
Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 302 KB/s], Decompressed: 6104
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 1182 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 193 KB/s], Decompressed: 6186
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 138 KB/s], Decompressed: 6223
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 47 KB/s], Decompressed: 6265
Downloaded: 6308 file(s) [attempted 6308/8459 = 74%, 1151 KB/s], Decompressed: 6299
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 2872 KB/s], Decompressed: 6333
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 414 KB/s], Decompressed: 6384
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 198 KB/s], Decompressed: 6432
Downloaded: 6486 file(s) [attempted 6486/8459 = 76%, 14 KB/s], Decompressed: 6480
Downloaded: 6528 file(s) [attempted 6528/8459 = 77%, 435 KB/s], Decompressed: 6521
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 133 KB/s], Decompressed: 6566
Downloaded: 6602 file(s) [attempted 6602/8459 = 78%, 229 KB/s], Decompressed: 6593
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 243 KB/s], Decompressed: 6631
Downloaded: 6679 file(s) [attempted 6679/8459 = 78%, 146 KB/s], Decompressed: 6675
Downloaded: 6724 file(s) [attempted 6724/8459 = 79%, 754 KB/s], Decompressed: 6720
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 424 KB/s], Decompressed: 6754
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 138 KB/s], Decompressed: 6795
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 227 KB/s], Decompressed: 6836
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 592 KB/s], Decompressed: 6874
Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 190 KB/s], Decompressed: 6918
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 186 KB/s], Decompressed: 6956
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 95 KB/s], Decompressed: 6997
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 324 KB/s], Decompressed: 7045
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 45 KB/s], Decompressed: 7079
Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 23 KB/s], Decompressed: 7117
Downloaded: 7165 file(s) [attempted 7165/8459 = 84%, 446 KB/s], Decompressed: 7161
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 141 KB/s], Decompressed: 7199
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 293 KB/s], Decompressed: 7213
Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 105 KB/s], Decompressed: 7213
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 71 KB/s], Decompressed: 7315
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 287 KB/s], Decompressed: 7360
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 2250 KB/s], Decompressed: 7401
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 313 KB/s], Decompressed: 7449
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 160 KB/s], Decompressed: 7497
Downloaded: 7545 file(s) [attempted 7545/8459 = 89%, 760 KB/s], Decompressed: 7541
Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 149 KB/s], Decompressed: 7562
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 103 KB/s], Decompressed: 7569
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 200 KB/s], Decompressed: 7569
Downloaded: 7699 file(s) [attempted 7699/8459 = 91%, 245 KB/s], Decompressed: 7668
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 152 KB/s], Decompressed: 7668
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 603 KB/s], Decompressed: 7767
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 91 KB/s], Decompressed: 7815
Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 23 KB/s], Decompressed: 7853
Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 182 KB/s], Decompressed: 7894
Downloaded: 7942 file(s) [attempted 7942/8459 = 93%, 543 KB/s], Decompressed: 7938
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 211 KB/s], Decompressed: 7976
Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 147 KB/s], Decompressed: 8010
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 112 KB/s], Decompressed: 8044
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 206 KB/s], Decompressed: 8089
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 8133
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 277 KB/s], Decompressed: 8171
Downloaded: 8213 file(s) [attempted 8213/8459 = 97%, 88 KB/s], Decompressed: 8209
Downloaded: 8250 file(s) [attempted 8250/8459 = 97%, 1630 KB/s], Decompressed: 8246
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 304 KB/s], Decompressed: 8277
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 522 KB/s], Decompressed: 8325
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 452 KB/s], Decompressed: 8366
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 789 KB/s], Decompressed: 8400
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 921 KB/s], Decompressed: 8445
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 921 KB/s], Decompressed: 8452

lean_checker exit 0 duration 17m 27s · created 6/30/2026, 12:33:28 AM

lake build

✔ [763/767] Built Iut.Foundations.QualitativeData (51s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (64s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.6s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (66s)
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 `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
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`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.1s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.1s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (14s)
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 (75s)
ℹ [3419/3425] Built Iut.Stage1.IUTStage1FrobenioidShift (249s)
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) [0x7523e73c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7523e73bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7523e73bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7523e72f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7523e72f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7523e73caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7523e7232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7523e7232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7523e7233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7523e72341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7523e73c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7523e7015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7523e73c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7523e73c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7523e739b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7523e7015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7523e2422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7523e220cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7523e1d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7523e1d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7523dec4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7523dec45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5ff0806b38da]
✔ [3420/3425] Built Iut.Stage1.IUTStage1EndpointAudit (82s)
✔ [3421/3425] Built Iut.Stage1.IUTStage1Source (3.3s)
⚠ [3422/3425] Built Iut.Stage1.IUTStage1Experiments (209s)
warning: Iut/Stage1/IUTStage1Experiments.lean:144902: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:145270: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:145573: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:145777: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) [0x73c458bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c458bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c458bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_3 [private]+0x25) [0x73c458aeba65]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.initFn._lam_2 [boxed]+0x9) [0x73c458aebb89]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c458bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c458a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c458a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c458a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c458a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c458bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c458815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c458b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c458815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c453c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c453a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c453569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c453569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c45044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c450445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5834994b68da]
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) [0x73c458bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c458bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c458bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73c458af3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73c458af4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c458bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c458a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c458a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c458a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c458a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c458bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c458815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c458bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c458b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c458815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c453c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c453a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c453569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c453569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c45044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c450445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5834994b68da]
✔ [3423/3425] Built Iut.Basic (119s)
✔ [3424/3425] Built Iut (2.5s)
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 4s · created 6/30/2026, 12:33:28 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 6/30/2026, 12:33:28 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":7307}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2518,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":34731,"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 8264080301d566477fc64f3fdb9b472b7b9ce44dbb4c4f3786edc619dc259e5f
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-758-runtime-semantic_extract-50135-1782733816438405570-3

semantic_extract exit - duration 4h 0m · created 6/30/2026, 12:33:28 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":2879,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8264080301d566477fc64f3fdb9b472b7b9ce44dbb4c4f3786edc619dc259e5f
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":34,"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-758-runtime-semantic_extract-50135-1782761561371415808-7

semantic_extract exit - duration 1h 0m · created 6/30/2026, 12:33:28 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":569,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":6854,"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 9e064258683b242a3a660bddd3901e7015729e94727d64beb0545b59033ff32c
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-758-runtime-semantic_extract-50135-1782775972226152658-8