Verification run

Run 7

Gogopex/pfr branch master triggered via manual

failed commit manual toolchain lean-v4-28-0-rc1 prover lean took 8m 50s · finished 6w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code 1 (toolchain lean-v4-28-0-rc1, command: elan run leanprover/lean4:v4.28.0-rc1 -- ./.apodeixis/tools/lean-semantic-extract.sh)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 574 ms · created 6/1/2026, 5:57:52 PM

git clone --depth 1 --branch master --single-branch https://github.com/Gogopex/pfr.git /var/lib/apodeixis/repos/job-7-source

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

lake_cache exit 0 duration 1m 44s · created 6/1/2026, 5:57:52 PM

lake exe cache get

installing leantar 0.1.16
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
Attempting to download 7954 file(s) from leanprover-community/mathlib4 cache
Decompressing 7954 file(s)
Unpacked in 17630 ms
Completed successfully!

info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: APAP: cloning https://github.com/YaelDillies/apap.git
info: APAP: checking out revision '13fd6dd3a47445b6dd10826f0ffc1116f4e13144'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '507f18fc9044549fc730d8d0270521e3b090360a'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '7311586e1a56af887b1081d05e80c11b6c41d212'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '5ce7f0a355f522a952a3d678d696bd563bb4fd28'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'b5908dbac486279f1133cb937648c63c30b455af'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'f08e838d4f9aea519f3cde06260cfb686fd4bab0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '23324752757bf28124a518ec284044c8db79fee5'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '0100f1a3222df01286db33fcb6a1f98564f5439d'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '28e0856d4424863a85b18f38868c5420c55f9bae'
✔ [2/22] Built Cache.Lean (470ms)
✔ [3/22] Built Cache.Init (438ms)
✔ [4/22] Built Cache.Init:c.o (443ms)
✔ [5/22] Built Cache.Lean:c.o (416ms)
✔ [6/22] Built Cache.IO (1.5s)
✔ [7/22] Built Cache.Hashing (808ms)
✔ [8/22] Built Cache.IO:c.o (1.2s)
✔ [9/22] Built Cache.Hashing:c.o (408ms)
✔ [15/22] Built Batteries.Data.Array.Match:c.o (207ms)
✔ [16/22] Built Batteries.Data.String.Basic:c.o (114ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (193ms)
✔ [18/22] Built Cache.Requests (1.5s)
✔ [19/22] Built Cache.Main (748ms)
✔ [20/22] Built Cache.Main:c.o (442ms)
✔ [21/22] Built Cache.Requests:c.o (1.3s)
✔ [22/22] Built cache:exe (2.1s)
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0

100 1125k  100 1125k    0     0  1904k      0 --:--:-- --:--:-- --:--:-- 1904k


Downloaded: 1 file(s) [attempted 1/7954 = 0%, 11 KB/s]
Downloaded: 14 file(s) [attempted 14/7954 = 0%, 2 KB/s]
Downloaded: 39 file(s) [attempted 39/7954 = 0%, 20 KB/s]
Downloaded: 65 file(s) [attempted 65/7954 = 0%, 210 KB/s]
Downloaded: 96 file(s) [attempted 96/7954 = 1%, 694 KB/s]
Downloaded: 134 file(s) [attempted 134/7954 = 1%, 106 KB/s]
Downloaded: 175 file(s) [attempted 175/7954 = 2%, 142 KB/s]
Downloaded: 210 file(s) [attempted 210/7954 = 2%, 47 KB/s]
Downloaded: 247 file(s) [attempted 247/7954 = 3%, 275 KB/s]
Downloaded: 285 file(s) [attempted 285/7954 = 3%, 154 KB/s]
Downloaded: 329 file(s) [attempted 329/7954 = 4%, 60 KB/s]
Downloaded: 371 file(s) [attempted 371/7954 = 4%, 611 KB/s]
Downloaded: 412 file(s) [attempted 412/7954 = 5%, 133 KB/s]
Downloaded: 449 file(s) [attempted 449/7954 = 5%, 448 KB/s]
Downloaded: 490 file(s) [attempted 490/7954 = 6%, 118 KB/s]
Downloaded: 528 file(s) [attempted 528/7954 = 6%, 51 KB/s]
Downloaded: 569 file(s) [attempted 569/7954 = 7%, 190 KB/s]
Downloaded: 614 file(s) [attempted 614/7954 = 7%, 190 KB/s]
Downloaded: 651 file(s) [attempted 651/7954 = 8%, 163 KB/s]
Downloaded: 696 file(s) [attempted 696/7954 = 8%, 142 KB/s]
Downloaded: 734 file(s) [attempted 734/7954 = 9%, 204 KB/s]
Downloaded: 775 file(s) [attempted 775/7954 = 9%, 1092 KB/s]
Downloaded: 819 file(s) [attempted 819/7954 = 10%, 115 KB/s]
Downloaded: 864 file(s) [attempted 864/7954 = 10%, 86 KB/s]
Downloaded: 901 file(s) [attempted 901/7954 = 11%, 329 KB/s]
Downloaded: 939 file(s) [attempted 939/7954 = 11%, 373 KB/s]
Downloaded: 980 file(s) [attempted 980/7954 = 12%, 448 KB/s]
Downloaded: 1025 file(s) [attempted 1025/7954 = 12%, 302 KB/s]
Downloaded: 1066 file(s) [attempted 1066/7954 = 13%, 458 KB/s]
Downloaded: 1100 file(s) [attempted 1100/7954 = 13%, 379 KB/s]
Downloaded: 1141 file(s) [attempted 1141/7954 = 14%, 84 KB/s]
Downloaded: 1182 file(s) [attempted 1182/7954 = 14%, 162 KB/s]
Downloaded: 1223 file(s) [attempted 1223/7954 = 15%, 150 KB/s]
Downloaded: 1264 file(s) [attempted 1264/7954 = 15%, 281 KB/s]
Downloaded: 1302 file(s) [attempted 1302/7954 = 16%, 229 KB/s]
Downloaded: 1343 file(s) [attempted 1343/7954 = 16%, 408 KB/s]
Downloaded: 1384 file(s) [attempted 1384/7954 = 17%, 165 KB/s]
Downloaded: 1429 file(s) [attempted 1429/7954 = 17%, 222 KB/s]
Downloaded: 1470 file(s) [attempted 1470/7954 = 18%, 417 KB/s]
Downloaded: 1507 file(s) [attempted 1507/7954 = 18%, 303 KB/s]
Downloaded: 1548 file(s) [attempted 1548/7954 = 19%, 61 KB/s]
Downloaded: 1593 file(s) [attempted 1593/7954 = 20%, 289 KB/s]
Downloaded: 1637 file(s) [attempted 1637/7954 = 20%, 126 KB/s]
Downloaded: 1682 file(s) [attempted 1682/7954 = 21%, 1846 KB/s]
Downloaded: 1716 file(s) [attempted 1716/7954 = 21%, 888 KB/s]
Downloaded: 1754 file(s) [attempted 1754/7954 = 22%, 824 KB/s]
Downloaded: 1795 file(s) [attempted 1795/7954 = 22%, 83 KB/s]
Downloaded: 1836 file(s) [attempted 1836/7954 = 23%, 65 KB/s]
Downloaded: 1873 file(s) [attempted 1873/7954 = 23%, 172 KB/s]
Downloaded: 1915 file(s) [attempted 1915/7954 = 24%, 145 KB/s]
Downloaded: 1952 file(s) [attempted 1952/7954 = 24%, 55 KB/s]
Downloaded: 1997 file(s) [attempted 1997/7954 = 25%, 147 KB/s]
Downloaded: 2038 file(s) [attempted 2038/7954 = 25%, 141 KB/s]
Downloaded: 2082 file(s) [attempted 2082/7954 = 26%, 46 KB/s]
Downloaded: 2127 file(s) [attempted 2127/7954 = 26%, 192 KB/s]
Downloaded: 2168 file(s) [attempted 2168/7954 = 27%, 370 KB/s]
Downloaded: 2212 file(s) [attempted 2212/7954 = 27%, 96 KB/s]
Downloaded: 2253 file(s) [attempted 2253/7954 = 28%, 710 KB/s]
Downloaded: 2291 file(s) [attempted 2291/7954 = 28%, 222 KB/s]
Downloaded: 2332 file(s) [attempted 2332/7954 = 29%, 1444 KB/s]
Downloaded: 2377 file(s) [attempted 2377/7954 = 29%, 479 KB/s]
Downloaded: 2421 file(s) [attempted 2421/7954 = 30%, 135 KB/s]
Downloaded: 2462 file(s) [attempted 2462/7954 = 30%, 377 KB/s]
Downloaded: 2500 file(s) [attempted 2500/7954 = 31%, 111 KB/s]
Downloaded: 2544 file(s) [attempted 2544/7954 = 31%, 48 KB/s]
Downloaded: 2582 file(s) [attempted 2582/7954 = 32%, 603 KB/s]
Downloaded: 2619 file(s) [attempted 2619/7954 = 32%, 425 KB/s]
Downloaded: 2663 file(s) [attempted 2663/7954 = 33%, 76 KB/s]
Downloaded: 2698 file(s) [attempted 2698/7954 = 33%, 617 KB/s]
Downloaded: 2743 file(s) [attempted 2743/7954 = 34%, 543 KB/s]
Downloaded: 2780 file(s) [attempted 2780/7954 = 34%, 318 KB/s]
Downloaded: 2811 file(s) [attempted 2811/7954 = 35%, 331 KB/s]
Downloaded: 2852 file(s) [attempted 2852/7954 = 35%, 301 KB/s]
Downloaded: 2897 file(s) [attempted 2897/7954 = 36%, 308 KB/s]
Downloaded: 2941 file(s) [attempted 2941/7954 = 36%, 335 KB/s]
Downloaded: 2982 file(s) [attempted 2982/7954 = 37%, 661 KB/s]
Downloaded: 3023 file(s) [attempted 3023/7954 = 38%, 336 KB/s]
Downloaded: 3057 file(s) [attempted 3057/7954 = 38%, 574 KB/s]
Downloaded: 3102 file(s) [attempted 3102/7954 = 38%, 239 KB/s]
Downloaded: 3150 file(s) [attempted 3150/7954 = 39%, 553 KB/s]
Downloaded: 3198 file(s) [attempted 3198/7954 = 40%, 219 KB/s]
Downloaded: 3235 file(s) [attempted 3235/7954 = 40%, 98 KB/s]
Downloaded: 3280 file(s) [attempted 3280/7954 = 41%, 312 KB/s]
Downloaded: 3321 file(s) [attempted 3321/7954 = 41%, 303 KB/s]
Downloaded: 3359 file(s) [attempted 3359/7954 = 42%, 173 KB/s]
Downloaded: 3403 file(s) [attempted 3403/7954 = 42%, 906 KB/s]
Downloaded: 3448 file(s) [attempted 3448/7954 = 43%, 225 KB/s]
Downloaded: 3489 file(s) [attempted 3489/7954 = 43%, 74 KB/s]
Downloaded: 3530 file(s) [attempted 3530/7954 = 44%, 70 KB/s]
Downloaded: 3567 file(s) [attempted 3567/7954 = 44%, 208 KB/s]
Downloaded: 3609 file(s) [attempted 3609/7954 = 45%, 384 KB/s]
Downloaded: 3650 file(s) [attempted 3650/7954 = 45%, 143 KB/s]
Downloaded: 3691 file(s) [attempted 3691/7954 = 46%, 705 KB/s]
Downloaded: 3732 file(s) [attempted 3732/7954 = 46%, 738 KB/s]
Downloaded: 3769 file(s) [attempted 3769/7954 = 47%, 728 KB/s]
Downloaded: 3810 file(s) [attempted 3810/7954 = 47%, 221 KB/s]
Downloaded: 3855 file(s) [attempted 3855/7954 = 48%, 743 KB/s]
Downloaded: 3893 file(s) [attempted 3893/7954 = 48%, 70 KB/s]
Downloaded: 3934 file(s) [attempted 3934/7954 = 49%, 768 KB/s]
Downloaded: 3975 file(s) [attempted 3975/7954 = 49%, 659 KB/s]
Downloaded: 4016 file(s) [attempted 4016/7954 = 50%, 405 KB/s]
Downloaded: 4060 file(s) [attempted 4060/7954 = 51%, 840 KB/s]
Downloaded: 4098 file(s) [attempted 4098/7954 = 51%, 961 KB/s]
Downloaded: 4142 file(s) [attempted 4142/7954 = 52%, 92 KB/s]
Downloaded: 4183 file(s) [attempted 4183/7954 = 52%, 429 KB/s]
Downloaded: 4221 file(s) [attempted 4221/7954 = 53%, 243 KB/s]
Downloaded: 4262 file(s) [attempted 4262/7954 = 53%, 250 KB/s]
Downloaded: 4296 file(s) [attempted 4296/7954 = 54%, 350 KB/s]
Downloaded: 4337 file(s) [attempted 4337/7954 = 54%, 128 KB/s]
Downloaded: 4379 file(s) [attempted 4379/7954 = 55%, 76 KB/s]
Downloaded: 4420 file(s) [attempted 4420/7954 = 55%, 1270 KB/s]
Downloaded: 4461 file(s) [attempted 4461/7954 = 56%, 564 KB/s]
Downloaded: 4502 file(s) [attempted 4502/7954 = 56%, 64 KB/s]
Downloaded: 4539 file(s) [attempted 4539/7954 = 57%, 220 KB/s]
Downloaded: 4580 file(s) [attempted 4580/7954 = 57%, 348 KB/s]
Downloaded: 4621 file(s) [attempted 4621/7954 = 58%, 1752 KB/s]
Downloaded: 4663 file(s) [attempted 4663/7954 = 58%, 409 KB/s]
Downloaded: 4704 file(s) [attempted 4704/7954 = 59%, 400 KB/s]
Downloaded: 4745 file(s) [attempted 4745/7954 = 59%, 118 KB/s]
Downloaded: 4789 file(s) [attempted 4789/7954 = 60%, 598 KB/s]
Downloaded: 4830 file(s) [attempted 4830/7954 = 60%, 117 KB/s]
Downloaded: 4871 file(s) [attempted 4871/7954 = 61%, 302 KB/s]
Downloaded: 4912 file(s) [attempted 4912/7954 = 61%, 135 KB/s]
Downloaded: 4953 file(s) [attempted 4953/7954 = 62%, 225 KB/s]
Downloaded: 4995 file(s) [attempted 4995/7954 = 62%, 144 KB/s]
Downloaded: 5036 file(s) [attempted 5036/7954 = 63%, 867 KB/s]
Downloaded: 5077 file(s) [attempted 5077/7954 = 63%, 236 KB/s]
Downloaded: 5121 file(s) [attempted 5121/7954 = 64%, 507 KB/s]
Downloaded: 5162 file(s) [attempted 5162/7954 = 64%, 141 KB/s]
Downloaded: 5203 file(s) [attempted 5203/7954 = 65%, 96 KB/s]
Downloaded: 5244 file(s) [attempted 5244/7954 = 65%, 58 KB/s]
Downloaded: 5289 file(s) [attempted 5289/7954 = 66%, 138 KB/s]
Downloaded: 5330 file(s) [attempted 5330/7954 = 67%, 55 KB/s]
Downloaded: 5368 file(s) [attempted 5368/7954 = 67%, 441 KB/s]
Downloaded: 5412 file(s) [attempted 5412/7954 = 68%, 423 KB/s]
Downloaded: 5453 file(s) [attempted 5453/7954 = 68%, 196 KB/s]
Downloaded: 5494 file(s) [attempted 5494/7954 = 69%, 58 KB/s]
Downloaded: 5542 file(s) [attempted 5542/7954 = 69%, 668 KB/s]
Downloaded: 5576 file(s) [attempted 5576/7954 = 70%, 225 KB/s]
Downloaded: 5617 file(s) [attempted 5617/7954 = 70%, 95 KB/s]
Downloaded: 5662 file(s) [attempted 5662/7954 = 71%, 401 KB/s]
Downloaded: 5706 file(s) [attempted 5706/7954 = 71%, 50 KB/s]
Downloaded: 5751 file(s) [attempted 5751/7954 = 72%, 473 KB/s]
Downloaded: 5792 file(s) [attempted 5792/7954 = 72%, 553 KB/s]
Downloaded: 5830 file(s) [attempted 5830/7954 = 73%, 179 KB/s]
Downloaded: 5867 file(s) [attempted 5867/7954 = 73%, 1043 KB/s]
Downloaded: 5908 file(s) [attempted 5908/7954 = 74%, 76 KB/s]
Downloaded: 5949 file(s) [attempted 5949/7954 = 74%, 418 KB/s]
Downloaded: 5987 file(s) [attempted 5987/7954 = 75%, 349 KB/s]
Downloaded: 6031 file(s) [attempted 6031/7954 = 75%, 173 KB/s]
Downloaded: 6069 file(s) [attempted 6069/7954 = 76%, 639 KB/s]
Downloaded: 6110 file(s) [attempted 6110/7954 = 76%, 406 KB/s]
Downloaded: 6151 file(s) [attempted 6151/7954 = 77%, 511 KB/s]
Downloaded: 6189 file(s) [attempted 6189/7954 = 77%, 514 KB/s]
Downloaded: 6226 file(s) [attempted 6226/7954 = 78%, 177 KB/s]
Downloaded: 6268 file(s) [attempted 6268/7954 = 78%, 149 KB/s]
Downloaded: 6312 file(s) [attempted 6312/7954 = 79%, 262 KB/s]
Downloaded: 6350 file(s) [attempted 6350/7954 = 79%, 186 KB/s]
Downloaded: 6391 file(s) [attempted 6391/7954 = 80%, 566 KB/s]
Downloaded: 6422 file(s) [attempted 6422/7954 = 80%, 241 KB/s]
Downloaded: 6466 file(s) [attempted 6466/7954 = 81%, 83 KB/s]
Downloaded: 6507 file(s) [attempted 6507/7954 = 81%, 190 KB/s]
Downloaded: 6548 file(s) [attempted 6548/7954 = 82%, 87 KB/s]
Downloaded: 6589 file(s) [attempted 6589/7954 = 82%, 489 KB/s]
Downloaded: 6623 file(s) [attempted 6623/7954 = 83%, 39 KB/s]
Downloaded: 6661 file(s) [attempted 6661/7954 = 83%, 461 KB/s]
Downloaded: 6706 file(s) [attempted 6706/7954 = 84%, 356 KB/s]
Downloaded: 6750 file(s) [attempted 6750/7954 = 84%, 44 KB/s]
Downloaded: 6791 file(s) [attempted 6791/7954 = 85%, 300 KB/s]
Downloaded: 6828 file(s) [attempted 6828/7954 = 85%, 516 KB/s]
Downloaded: 6866 file(s) [attempted 6866/7954 = 86%, 1856 KB/s]
Downloaded: 6908 file(s) [attempted 6908/7954 = 86%, 313 KB/s]
Downloaded: 6949 file(s) [attempted 6949/7954 = 87%, 262 KB/s]
Downloaded: 6993 file(s) [attempted 6993/7954 = 87%, 151 KB/s]
Downloaded: 7034 file(s) [attempted 7034/7954 = 88%, 147 KB/s]
Downloaded: 7075 file(s) [attempted 7075/7954 = 88%, 131 KB/s]
Downloaded: 7120 file(s) [attempted 7120/7954 = 89%, 139 KB/s]
Downloaded: 7154 file(s) [attempted 7154/7954 = 89%, 331 KB/s]
Downloaded: 7192 file(s) [attempted 7192/7954 = 90%, 121 KB/s]
Downloaded: 7236 file(s) [attempted 7236/7954 = 90%, 71 KB/s]
Downloaded: 7277 file(s) [attempted 7277/7954 = 91%, 154 KB/s]
Downloaded: 7318 file(s) [attempted 7318/7954 = 92%, 765 KB/s]
Downloaded: 7352 file(s) [attempted 7352/7954 = 92%, 100 KB/s]
Downloaded: 7393 file(s) [attempted 7393/7954 = 92%, 100 KB/s]
Downloaded: 7438 file(s) [attempted 7438/7954 = 93%, 47 KB/s]
Downloaded: 7482 file(s) [attempted 7482/7954 = 94%, 192 KB/s]
Downloaded: 7523 file(s) [attempted 7523/7954 = 94%, 2415 KB/s]
Downloaded: 7561 file(s) [attempted 7561/7954 = 95%, 151 KB/s]
Downloaded: 7599 file(s) [attempted 7599/7954 = 95%, 334 KB/s]
Downloaded: 7643 file(s) [attempted 7643/7954 = 96%, 171 KB/s]
Downloaded: 7684 file(s) [attempted 7684/7954 = 96%, 68 KB/s]
Downloaded: 7729 file(s) [attempted 7729/7954 = 97%, 285 KB/s]
Downloaded: 7766 file(s) [attempted 7766/7954 = 97%, 197 KB/s]
Downloaded: 7804 file(s) [attempted 7804/7954 = 98%, 33 KB/s]
Downloaded: 7845 file(s) [attempted 7845/7954 = 98%, 253 KB/s]
Downloaded: 7886 file(s) [attempted 7886/7954 = 99%, 147 KB/s]
Downloaded: 7927 file(s) [attempted 7927/7954 = 99%, 56 KB/s]
Downloaded: 7951 file(s) [attempted 7951/7954 = 99%, 519 KB/s]
Downloaded: 7954 file(s) [attempted 7954/7954 = 100%, 519 KB/s]

lean_checker exit 0 duration 3m 18s · created 6/1/2026, 5:57:52 PM

lake build

✔ [1886/1896] Built PFR.ForMathlib.Pair (4.6s)
✔ [2176/2250] Built PFR.Mathlib.MeasureTheory.Constructions.Pi (5.4s)
✔ [2596/2622] Built PFR.Mathlib.LinearAlgebra.Basis.VectorSpace (6.9s)
✔ [2597/2623] Built PFR.Mathlib.Probability.Independence.Kernel.IndepFun (7.2s)
✔ [2611/2630] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic (2.3s)
✔ [2660/2683] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable (2.3s)
✔ [2661/2683] Built PFR.ForMathlib.FiniteRange.Defs (3.4s)
✔ [2662/2683] Built PFR.Mathlib.MeasureTheory.Measure.Dirac (2.2s)
✔ [2664/2683] Built PFR.Mathlib.Data.Set.Basic (1.7s)
✔ [2665/2683] Built PFR.Mathlib.Probability.Independence.Basic (4.2s)
✔ [2667/2683] Built PFR.Mathlib.MeasureTheory.Measure.Prod (2.5s)
✔ [2669/2683] Built PFR.Mathlib.Data.Set.Insert (1.2s)
✔ [2670/2683] Built PFR.ForMathlib.FiniteRange.ConditionalProbability (2.3s)
✔ [2675/2683] Built PFR.Mathlib.MeasureTheory.Measure.Real (2.3s)
✔ [2676/2702] Built PFR.ForMathlib.ThreeVariables (2.6s)
✔ [2762/2783] Built PFR.Mathlib.Data.Set.Card (1.6s)
✔ [2770/2789] Built PFR.Mathlib.MeasureTheory.Integral.Bochner.Set (2.6s)
✔ [2771/2789] Built PFR.Mathlib.Probability.ConditionalProbability (2.1s)
✔ [2775/2792] Built PFR.Mathlib.Probability.IdentDistrib (7.4s)
✔ [2778/2792] Built PFR.Mathlib.Probability.UniformOn (3.4s)
✔ [2781/2792] Built PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog (5.3s)
✔ [2782/2798] Built PFR.Mathlib.Probability.Kernel.Disintegration (9.1s)
✔ [2784/2806] Built PFR.ForMathlib.ConditionalIndependence (6.1s)
✔ [2789/2811] Built PFR.Mathlib.Probability.Kernel.Composition.Comp (4.8s)
✔ [2797/2836] Built PFR.ForMathlib.FiniteRange.IdentDistrib (4.4s)
✔ [2815/2842] Built PFR.ForMathlib.Uniform (7.4s)
✔ [2821/2849] Built PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure (2.9s)
✔ [2841/2867] Built PFR.ForMathlib.Entropy.Measure (12s)
✔ [2842/2867] Built APAP.Prereqs.Function.Indicator.Defs (3.5s)
✔ [2843/2867] Built PFR.Tactic.RPowSimp (5.6s)
✔ [2845/2870] Built PFR.ForMathlib.FourVariables (6.4s)
✔ [2846/2889] Built APAP.Prereqs.DummyPositivity (1.0s)
✔ [2850/2889] Built APAP.Prereqs.Function.Indicator.Basic (1.6s)
✔ [2851/2889] Built PFR.Mathlib.Data.Fin.Basic (1.8s)
✔ [2852/2889] Built PFR.Mathlib.Algebra.BigOperators.Fin (2.3s)
✔ [2853/2890] Built PFR.ForMathlib.Entropy.Kernel.Basic (6.0s)
✔ [2855/2890] Built PFR.Mathlib.Order.Interval.Finset.Fin (1.4s)
✔ [2856/2890] Built PFR.Mathlib.MeasureTheory.Group.Arithmetic (2.3s)
✔ [2857/2890] Built APAP.Prereqs.Convolution.Discrete.Defs (9.2s)
✔ [2858/2890] Built PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (1.4s)
✔ [2860/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.Finrank (1.7s)
✔ [2862/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (1.9s)
✔ [2863/2901] Built PFR.Mathlib.LinearAlgebra.Quotient.Basic (1.5s)
✔ [2864/2901] Built PFR.ForMathlib.AffineSpaceDim (3.1s)
✔ [2867/2901] Built APAP.Prereqs.Convolution.Order (4.3s)
✔ [2868/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpace (238ms)
✔ [2869/2901] Built PFR.ForMathlib.Entropy.Kernel.MutualInfo (4.9s)
✔ [2870/2901] Built PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic (1.4s)
✔ [2871/2901] Built APAP.Prereqs.Convolution.Discrete.Basic (5.4s)
✔ [2872/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef (1.9s)
✔ [2873/2901] Built PFR.ForMathlib.Entropy.Kernel.Group (3.6s)
✔ [2874/2901] Built PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability (2.4s)
✔ [2875/2901] Built PFR.ForMathlib.Entropy.Kernel.RuzsaDist (6.5s)
✔ [2876/2901] Built PFR.ForMathlib.Entropy.Basic (10s)
✔ [2877/2901] Built PFR.ForMathlib.Entropy.Group (4.6s)
✔ [2878/2901] Built PFR.Kullback (5.0s)
✔ [2879/2901] Built APAP.Extras.BSG (16s)
✔ [2880/2901] Built PFR.ForMathlib.Entropy.RuzsaDist (10s)
✔ [2881/2901] Built PFR.Fibring (4.6s)
✔ [2882/2901] Built PFR.ForMathlib.Entropy.RuzsaSetDist (4.5s)
✔ [2883/2901] Built PFR.HundredPercent (4.8s)
✔ [2884/2901] Built PFR.TauFunctional (5.1s)
✔ [2885/2901] Built PFR.FirstEstimate (6.1s)
✔ [2886/2901] Built PFR.SecondEstimate (5.9s)
✔ [2887/2901] Built PFR.Endgame (19s)
✔ [2888/2901] Built PFR.EntropyPFR (2.7s)
✔ [2889/2901] Built PFR.Main (6.5s)
✔ [2890/2901] Built PFR.MoreRuzsaDist (49s)
✔ [2891/2901] Built PFR.MultiTauFunctional (4.7s)
✔ [2892/2901] Built PFR.ImprovedPFR (28s)
✔ [2893/2901] Built PFR.RhoFunctional (40s)
✔ [2894/2901] Built PFR.BoundingMutual (30s)
✔ [2895/2901] Built PFR.WeakPFR (18s)
✔ [2896/2901] Built PFR.HomPFR (7.8s)
✔ [2897/2901] Built PFR.ApproxHomPFR (13s)
✔ [2898/2901] Built PFR.TorsionEndgame (24s)
✔ [2899/2901] Built PFR.Examples (9.3s)
✔ [2900/2901] Built PFR (2.1s)
Build completed successfully (2901 jobs).

semantic_extract exit 1 duration 2m 44s · created 6/1/2026, 5:57:52 PM

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

lean semantic extractor failed: missing required command 'python3' to normalize repository semantics output
remediation: install python3 or ensure the Lean extractor emits the semantic envelope directly