Verification run

Run 6

Gogopex/pfr branch master triggered via manual

failed commit manual toolchain lean-v4-28-0-rc1 prover lean took 6m 3s · 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 579 ms · created 6/1/2026, 5:29:40 PM

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

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

lake_cache exit 0 duration 1m 37s · created 6/1/2026, 5:29:40 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 17509 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 (336ms)
✔ [3/22] Built Cache.Init (294ms)
✔ [4/22] Built Cache.Lean:c.o (134ms)
✔ [5/22] Built Cache.Init:c.o (160ms)
✔ [6/22] Built Cache.IO (1.3s)
✔ [7/22] Built Cache.Hashing (647ms)
✔ [8/22] Built Cache.Hashing:c.o (434ms)
✔ [9/22] Built Cache.IO:c.o (1.2s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (92ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (220ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (188ms)
✔ [18/22] Built Cache.Requests (1.3s)
✔ [19/22] Built Cache.Main (631ms)
✔ [20/22] Built Cache.Main:c.o (458ms)
✔ [21/22] Built Cache.Requests:c.o (1.3s)
✔ [22/22] Built cache:exe (2.0s)
  % 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  3106k      0 --:--:-- --:--:-- --:--:-- 3106k


Downloaded: 1 file(s) [attempted 1/7954 = 0%, 12 KB/s]
Downloaded: 13 file(s) [attempted 13/7954 = 0%, 10 KB/s]
Downloaded: 34 file(s) [attempted 34/7954 = 0%, 21 KB/s]
Downloaded: 65 file(s) [attempted 65/7954 = 0%, 29 KB/s]
Downloaded: 100 file(s) [attempted 100/7954 = 1%, 60 KB/s]
Downloaded: 137 file(s) [attempted 137/7954 = 1%, 105 KB/s]
Downloaded: 179 file(s) [attempted 179/7954 = 2%, 354 KB/s]
Downloaded: 213 file(s) [attempted 213/7954 = 2%, 189 KB/s]
Downloaded: 247 file(s) [attempted 247/7954 = 3%, 250 KB/s]
Downloaded: 285 file(s) [attempted 285/7954 = 3%, 913 KB/s]
Downloaded: 329 file(s) [attempted 329/7954 = 4%, 134 KB/s]
Downloaded: 377 file(s) [attempted 377/7954 = 4%, 610 KB/s]
Downloaded: 415 file(s) [attempted 415/7954 = 5%, 69 KB/s]
Downloaded: 449 file(s) [attempted 449/7954 = 5%, 458 KB/s]
Downloaded: 490 file(s) [attempted 490/7954 = 6%, 120 KB/s]
Downloaded: 532 file(s) [attempted 532/7954 = 6%, 929 KB/s]
Downloaded: 579 file(s) [attempted 579/7954 = 7%, 255 KB/s]
Downloaded: 627 file(s) [attempted 627/7954 = 7%, 1199 KB/s]
Downloaded: 665 file(s) [attempted 665/7954 = 8%, 197 KB/s]
Downloaded: 706 file(s) [attempted 706/7954 = 8%, 335 KB/s]
Downloaded: 747 file(s) [attempted 747/7954 = 9%, 115 KB/s]
Downloaded: 788 file(s) [attempted 788/7954 = 9%, 206 KB/s]
Downloaded: 830 file(s) [attempted 830/7954 = 10%, 389 KB/s]
Downloaded: 871 file(s) [attempted 871/7954 = 10%, 491 KB/s]
Downloaded: 912 file(s) [attempted 912/7954 = 11%, 387 KB/s]
Downloaded: 949 file(s) [attempted 949/7954 = 11%, 166 KB/s]
Downloaded: 991 file(s) [attempted 991/7954 = 12%, 864 KB/s]
Downloaded: 1028 file(s) [attempted 1028/7954 = 12%, 796 KB/s]
Downloaded: 1069 file(s) [attempted 1069/7954 = 13%, 198 KB/s]
Downloaded: 1110 file(s) [attempted 1110/7954 = 13%, 396 KB/s]
Downloaded: 1148 file(s) [attempted 1148/7954 = 14%, 185 KB/s]
Downloaded: 1189 file(s) [attempted 1189/7954 = 14%, 134 KB/s]
Downloaded: 1223 file(s) [attempted 1223/7954 = 15%, 288 KB/s]
Downloaded: 1264 file(s) [attempted 1264/7954 = 15%, 956 KB/s]
Downloaded: 1305 file(s) [attempted 1305/7954 = 16%, 120 KB/s]
Downloaded: 1346 file(s) [attempted 1346/7954 = 16%, 241 KB/s]
Downloaded: 1387 file(s) [attempted 1387/7954 = 17%, 186 KB/s]
Downloaded: 1422 file(s) [attempted 1422/7954 = 17%, 62 KB/s]
Downloaded: 1466 file(s) [attempted 1466/7954 = 18%, 127 KB/s]
Downloaded: 1507 file(s) [attempted 1507/7954 = 18%, 307 KB/s]
Downloaded: 1548 file(s) [attempted 1548/7954 = 19%, 359 KB/s]
Downloaded: 1596 file(s) [attempted 1596/7954 = 20%, 134 KB/s]
Downloaded: 1641 file(s) [attempted 1641/7954 = 20%, 115 KB/s]
Downloaded: 1678 file(s) [attempted 1678/7954 = 21%, 289 KB/s]
Downloaded: 1719 file(s) [attempted 1719/7954 = 21%, 310 KB/s]
Downloaded: 1761 file(s) [attempted 1761/7954 = 22%, 926 KB/s]
Downloaded: 1798 file(s) [attempted 1798/7954 = 22%, 355 KB/s]
Downloaded: 1839 file(s) [attempted 1839/7954 = 23%, 70 KB/s]
Downloaded: 1884 file(s) [attempted 1884/7954 = 23%, 45 KB/s]
Downloaded: 1928 file(s) [attempted 1928/7954 = 24%, 208 KB/s]
Downloaded: 1962 file(s) [attempted 1962/7954 = 24%, 810 KB/s]
Downloaded: 2004 file(s) [attempted 2004/7954 = 25%, 116 KB/s]
Downloaded: 2041 file(s) [attempted 2041/7954 = 25%, 136 KB/s]
Downloaded: 2079 file(s) [attempted 2079/7954 = 26%, 117 KB/s]
Downloaded: 2123 file(s) [attempted 2123/7954 = 26%, 192 KB/s]
Downloaded: 2161 file(s) [attempted 2161/7954 = 27%, 563 KB/s]
Downloaded: 2199 file(s) [attempted 2199/7954 = 27%, 219 KB/s]
Downloaded: 2240 file(s) [attempted 2240/7954 = 28%, 40 KB/s]
Downloaded: 2274 file(s) [attempted 2274/7954 = 28%, 195 KB/s]
Downloaded: 2311 file(s) [attempted 2311/7954 = 29%, 263 KB/s]
Downloaded: 2353 file(s) [attempted 2353/7954 = 29%, 344 KB/s]
Downloaded: 2390 file(s) [attempted 2390/7954 = 30%, 304 KB/s]
Downloaded: 2431 file(s) [attempted 2431/7954 = 30%, 384 KB/s]
Downloaded: 2469 file(s) [attempted 2469/7954 = 31%, 508 KB/s]
Downloaded: 2510 file(s) [attempted 2510/7954 = 31%, 220 KB/s]
Downloaded: 2548 file(s) [attempted 2548/7954 = 32%, 140 KB/s]
Downloaded: 2585 file(s) [attempted 2585/7954 = 32%, 225 KB/s]
Downloaded: 2626 file(s) [attempted 2626/7954 = 33%, 123 KB/s]
Downloaded: 2664 file(s) [attempted 2664/7954 = 33%, 65 KB/s]
Downloaded: 2708 file(s) [attempted 2708/7954 = 34%, 58 KB/s]
Downloaded: 2753 file(s) [attempted 2753/7954 = 34%, 422 KB/s]
Downloaded: 2794 file(s) [attempted 2794/7954 = 35%, 233 KB/s]
Downloaded: 2832 file(s) [attempted 2832/7954 = 35%, 35 KB/s]
Downloaded: 2873 file(s) [attempted 2873/7954 = 36%, 110 KB/s]
Downloaded: 2914 file(s) [attempted 2914/7954 = 36%, 165 KB/s]
Downloaded: 2958 file(s) [attempted 2958/7954 = 37%, 534 KB/s]
Downloaded: 2999 file(s) [attempted 2999/7954 = 37%, 247 KB/s]
Downloaded: 3044 file(s) [attempted 3044/7954 = 38%, 1251 KB/s]
Downloaded: 3081 file(s) [attempted 3081/7954 = 38%, 119 KB/s]
Downloaded: 3119 file(s) [attempted 3119/7954 = 39%, 187 KB/s]
Downloaded: 3164 file(s) [attempted 3164/7954 = 39%, 125 KB/s]
Downloaded: 3205 file(s) [attempted 3205/7954 = 40%, 344 KB/s]
Downloaded: 3242 file(s) [attempted 3242/7954 = 40%, 169 KB/s]
Downloaded: 3280 file(s) [attempted 3280/7954 = 41%, 310 KB/s]
Downloaded: 3321 file(s) [attempted 3321/7954 = 41%, 290 KB/s]
Downloaded: 3362 file(s) [attempted 3362/7954 = 42%, 121 KB/s]
Downloaded: 3407 file(s) [attempted 3407/7954 = 42%, 576 KB/s]
Downloaded: 3444 file(s) [attempted 3444/7954 = 43%, 110 KB/s]
Downloaded: 3485 file(s) [attempted 3485/7954 = 43%, 232 KB/s]
Downloaded: 3530 file(s) [attempted 3530/7954 = 44%, 127 KB/s]
Downloaded: 3567 file(s) [attempted 3567/7954 = 44%, 211 KB/s]
Downloaded: 3605 file(s) [attempted 3605/7954 = 45%, 285 KB/s]
Downloaded: 3646 file(s) [attempted 3646/7954 = 45%, 44 KB/s]
Downloaded: 3684 file(s) [attempted 3684/7954 = 46%, 2047 KB/s]
Downloaded: 3725 file(s) [attempted 3725/7954 = 46%, 136 KB/s]
Downloaded: 3766 file(s) [attempted 3766/7954 = 47%, 236 KB/s]
Downloaded: 3800 file(s) [attempted 3800/7954 = 47%, 734 KB/s]
Downloaded: 3841 file(s) [attempted 3841/7954 = 48%, 272 KB/s]
Downloaded: 3879 file(s) [attempted 3879/7954 = 48%, 136 KB/s]
Downloaded: 3923 file(s) [attempted 3923/7954 = 49%, 62 KB/s]
Downloaded: 3961 file(s) [attempted 3961/7954 = 49%, 107 KB/s]
Downloaded: 4002 file(s) [attempted 4002/7954 = 50%, 225 KB/s]
Downloaded: 4043 file(s) [attempted 4043/7954 = 50%, 83 KB/s]
Downloaded: 4081 file(s) [attempted 4081/7954 = 51%, 233 KB/s]
Downloaded: 4122 file(s) [attempted 4122/7954 = 51%, 186 KB/s]
Downloaded: 4160 file(s) [attempted 4160/7954 = 52%, 300 KB/s]
Downloaded: 4201 file(s) [attempted 4201/7954 = 52%, 616 KB/s]
Downloaded: 4242 file(s) [attempted 4242/7954 = 53%, 406 KB/s]
Downloaded: 4283 file(s) [attempted 4283/7954 = 53%, 1165 KB/s]
Downloaded: 4320 file(s) [attempted 4320/7954 = 54%, 570 KB/s]
Downloaded: 4361 file(s) [attempted 4361/7954 = 54%, 57 KB/s]
Downloaded: 4402 file(s) [attempted 4402/7954 = 55%, 558 KB/s]
Downloaded: 4444 file(s) [attempted 4444/7954 = 55%, 1091 KB/s]
Downloaded: 4485 file(s) [attempted 4485/7954 = 56%, 401 KB/s]
Downloaded: 4522 file(s) [attempted 4522/7954 = 56%, 166 KB/s]
Downloaded: 4560 file(s) [attempted 4560/7954 = 57%, 554 KB/s]
Downloaded: 4598 file(s) [attempted 4598/7954 = 57%, 226 KB/s]
Downloaded: 4642 file(s) [attempted 4642/7954 = 58%, 387 KB/s]
Downloaded: 4683 file(s) [attempted 4683/7954 = 58%, 520 KB/s]
Downloaded: 4724 file(s) [attempted 4724/7954 = 59%, 53 KB/s]
Downloaded: 4758 file(s) [attempted 4758/7954 = 59%, 339 KB/s]
Downloaded: 4796 file(s) [attempted 4796/7954 = 60%, 618 KB/s]
Downloaded: 4841 file(s) [attempted 4841/7954 = 60%, 127 KB/s]
Downloaded: 4882 file(s) [attempted 4882/7954 = 61%, 189 KB/s]
Downloaded: 4923 file(s) [attempted 4923/7954 = 61%, 1441 KB/s]
Downloaded: 4957 file(s) [attempted 4957/7954 = 62%, 1433 KB/s]
Downloaded: 4995 file(s) [attempted 4995/7954 = 62%, 513 KB/s]
Downloaded: 5039 file(s) [attempted 5039/7954 = 63%, 323 KB/s]
Downloaded: 5077 file(s) [attempted 5077/7954 = 63%, 380 KB/s]
Downloaded: 5121 file(s) [attempted 5121/7954 = 64%, 684 KB/s]
Downloaded: 5162 file(s) [attempted 5162/7954 = 64%, 141 KB/s]
Downloaded: 5200 file(s) [attempted 5200/7954 = 65%, 107 KB/s]
Downloaded: 5241 file(s) [attempted 5241/7954 = 65%, 93 KB/s]
Downloaded: 5279 file(s) [attempted 5279/7954 = 66%, 80 KB/s]
Downloaded: 5316 file(s) [attempted 5316/7954 = 66%, 884 KB/s]
Downloaded: 5357 file(s) [attempted 5357/7954 = 67%, 654 KB/s]
Downloaded: 5402 file(s) [attempted 5402/7954 = 67%, 126 KB/s]
Downloaded: 5446 file(s) [attempted 5446/7954 = 68%, 152 KB/s]
Downloaded: 5487 file(s) [attempted 5487/7954 = 68%, 124 KB/s]
Downloaded: 5522 file(s) [attempted 5522/7954 = 69%, 210 KB/s]
Downloaded: 5559 file(s) [attempted 5559/7954 = 69%, 492 KB/s]
Downloaded: 5600 file(s) [attempted 5600/7954 = 70%, 220 KB/s]
Downloaded: 5645 file(s) [attempted 5645/7954 = 70%, 241 KB/s]
Downloaded: 5679 file(s) [attempted 5679/7954 = 71%, 268 KB/s]
Downloaded: 5723 file(s) [attempted 5723/7954 = 71%, 130 KB/s]
Downloaded: 5765 file(s) [attempted 5765/7954 = 72%, 728 KB/s]
Downloaded: 5802 file(s) [attempted 5802/7954 = 72%, 54 KB/s]
Downloaded: 5843 file(s) [attempted 5843/7954 = 73%, 563 KB/s]
Downloaded: 5881 file(s) [attempted 5881/7954 = 73%, 675 KB/s]
Downloaded: 5922 file(s) [attempted 5922/7954 = 74%, 188 KB/s]
Downloaded: 5966 file(s) [attempted 5966/7954 = 75%, 354 KB/s]
Downloaded: 6007 file(s) [attempted 6007/7954 = 75%, 257 KB/s]
Downloaded: 6045 file(s) [attempted 6045/7954 = 75%, 559 KB/s]
Downloaded: 6086 file(s) [attempted 6086/7954 = 76%, 313 KB/s]
Downloaded: 6127 file(s) [attempted 6127/7954 = 77%, 46 KB/s]
Downloaded: 6168 file(s) [attempted 6168/7954 = 77%, 503 KB/s]
Downloaded: 6206 file(s) [attempted 6206/7954 = 78%, 290 KB/s]
Downloaded: 6250 file(s) [attempted 6250/7954 = 78%, 229 KB/s]
Downloaded: 6292 file(s) [attempted 6292/7954 = 79%, 509 KB/s]
Downloaded: 6333 file(s) [attempted 6333/7954 = 79%, 849 KB/s]
Downloaded: 6370 file(s) [attempted 6370/7954 = 80%, 1360 KB/s]
Downloaded: 6404 file(s) [attempted 6404/7954 = 80%, 149 KB/s]
Downloaded: 6449 file(s) [attempted 6449/7954 = 81%, 83 KB/s]
Downloaded: 6490 file(s) [attempted 6490/7954 = 81%, 213 KB/s]
Downloaded: 6535 file(s) [attempted 6535/7954 = 82%, 233 KB/s]
Downloaded: 6572 file(s) [attempted 6572/7954 = 82%, 905 KB/s]
Downloaded: 6610 file(s) [attempted 6610/7954 = 83%, 462 KB/s]
Downloaded: 6651 file(s) [attempted 6651/7954 = 83%, 158 KB/s]
Downloaded: 6689 file(s) [attempted 6689/7954 = 84%, 98 KB/s]
Downloaded: 6733 file(s) [attempted 6733/7954 = 84%, 126 KB/s]
Downloaded: 6777 file(s) [attempted 6777/7954 = 85%, 856 KB/s]
Downloaded: 6819 file(s) [attempted 6819/7954 = 85%, 1387 KB/s]
Downloaded: 6856 file(s) [attempted 6856/7954 = 86%, 296 KB/s]
Downloaded: 6890 file(s) [attempted 6890/7954 = 86%, 477 KB/s]
Downloaded: 6928 file(s) [attempted 6928/7954 = 87%, 318 KB/s]
Downloaded: 6973 file(s) [attempted 6973/7954 = 87%, 605 KB/s]
Downloaded: 7020 file(s) [attempted 7020/7954 = 88%, 322 KB/s]
Downloaded: 7060 file(s) [attempted 7060/7954 = 88%, 439 KB/s]
Downloaded: 7092 file(s) [attempted 7092/7954 = 89%, 343 KB/s]
Downloaded: 7130 file(s) [attempted 7130/7954 = 89%, 78 KB/s]
Downloaded: 7171 file(s) [attempted 7171/7954 = 90%, 1103 KB/s]
Downloaded: 7216 file(s) [attempted 7216/7954 = 90%, 250 KB/s]
Downloaded: 7253 file(s) [attempted 7253/7954 = 91%, 44 KB/s]
Downloaded: 7291 file(s) [attempted 7291/7954 = 91%, 102 KB/s]
Downloaded: 7325 file(s) [attempted 7325/7954 = 92%, 567 KB/s]
Downloaded: 7366 file(s) [attempted 7366/7954 = 92%, 392 KB/s]
Downloaded: 7407 file(s) [attempted 7407/7954 = 93%, 77 KB/s]
Downloaded: 7448 file(s) [attempted 7448/7954 = 93%, 367 KB/s]
Downloaded: 7491 file(s) [attempted 7491/7954 = 94%, 422 KB/s]
Downloaded: 7527 file(s) [attempted 7527/7954 = 94%, 460 KB/s]
Downloaded: 7565 file(s) [attempted 7565/7954 = 95%, 180 KB/s]
Downloaded: 7606 file(s) [attempted 7606/7954 = 95%, 417 KB/s]
Downloaded: 7647 file(s) [attempted 7647/7954 = 96%, 521 KB/s]
Downloaded: 7691 file(s) [attempted 7691/7954 = 96%, 96 KB/s]
Downloaded: 7736 file(s) [attempted 7736/7954 = 97%, 297 KB/s]
Downloaded: 7773 file(s) [attempted 7773/7954 = 97%, 140 KB/s]
Downloaded: 7808 file(s) [attempted 7808/7954 = 98%, 618 KB/s]
Downloaded: 7849 file(s) [attempted 7849/7954 = 98%, 86 KB/s]
Downloaded: 7893 file(s) [attempted 7893/7954 = 99%, 575 KB/s]
Downloaded: 7938 file(s) [attempted 7938/7954 = 99%, 822 KB/s]
Downloaded: 7951 file(s) [attempted 7951/7954 = 99%, 191 KB/s]
Downloaded: 7954 file(s) [attempted 7954/7954 = 100%, 191 KB/s]

lean_checker exit 0 duration 3m 14s · created 6/1/2026, 5:29:40 PM

lake build

✔ [1886/1941] Built PFR.ForMathlib.Pair (1.4s)
✔ [2602/2622] Built PFR.Mathlib.MeasureTheory.Constructions.Pi (3.8s)
✔ [2603/2622] Built PFR.Mathlib.LinearAlgebra.Basis.VectorSpace (5.2s)
✔ [2604/2623] Built PFR.Mathlib.Probability.Independence.Kernel.IndepFun (5.5s)
✔ [2607/2623] Built PFR.ForMathlib.FiniteRange.Defs (3.1s)
✔ [2611/2623] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic (1.9s)
✔ [2661/2683] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable (1.9s)
✔ [2662/2683] Built PFR.ForMathlib.FiniteRange.ConditionalProbability (2.3s)
✔ [2663/2683] Built PFR.Mathlib.MeasureTheory.Measure.Dirac (2.1s)
✔ [2671/2683] Built PFR.Mathlib.MeasureTheory.Measure.Prod (2.2s)
✔ [2672/2683] Built PFR.Mathlib.Data.Set.Insert (1.2s)
✔ [2673/2689] Built PFR.Mathlib.Data.Set.Basic (1.3s)
✔ [2674/2692] Built PFR.Mathlib.Probability.Independence.Basic (3.0s)
✔ [2676/2692] Built PFR.Mathlib.Data.Set.Card (1.4s)
✔ [2677/2693] Built PFR.Mathlib.MeasureTheory.Measure.Real (1.9s)
✔ [2679/2698] Built PFR.ForMathlib.ThreeVariables (2.3s)
✔ [2742/2783] Built PFR.Mathlib.Probability.UniformOn (2.1s)
✔ [2764/2783] Built PFR.Mathlib.MeasureTheory.Integral.Bochner.Set (3.9s)
✔ [2765/2783] Built PFR.Mathlib.Probability.IdentDistrib (8.7s)
✔ [2773/2789] Built PFR.Mathlib.Probability.ConditionalProbability (2.6s)
✔ [2776/2789] Built PFR.ForMathlib.Uniform (7.6s)
✔ [2777/2789] Built PFR.Mathlib.Probability.Kernel.Disintegration (12s)
✔ [2780/2806] Built PFR.ForMathlib.ConditionalIndependence (5.5s)
✔ [2789/2814] Built PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog (4.2s)
✔ [2798/2821] Built PFR.Mathlib.Probability.Kernel.Composition.Comp (4.2s)
✔ [2815/2836] Built PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure (3.4s)
✔ [2821/2846] Built PFR.ForMathlib.FiniteRange.IdentDistrib (4.3s)
✔ [2841/2867] Built PFR.ForMathlib.Entropy.Measure (11s)
✔ [2842/2867] Built APAP.Prereqs.Function.Indicator.Defs (3.7s)
✔ [2843/2867] Built PFR.ForMathlib.FourVariables (6.5s)
✔ [2844/2870] Built PFR.Tactic.RPowSimp (5.4s)
✔ [2846/2889] Built APAP.Prereqs.Function.Indicator.Basic (1.4s)
✔ [2850/2889] Built APAP.Prereqs.DummyPositivity (1.0s)
✔ [2851/2889] Built PFR.Mathlib.Data.Fin.Basic (1.5s)
✔ [2852/2889] Built PFR.Mathlib.Algebra.BigOperators.Fin (2.2s)
✔ [2853/2890] Built PFR.ForMathlib.Entropy.Kernel.Basic (5.4s)
✔ [2855/2890] Built PFR.Mathlib.MeasureTheory.Group.Arithmetic (2.4s)
✔ [2856/2890] Built PFR.Mathlib.Order.Interval.Finset.Fin (1.6s)
✔ [2857/2890] Built PFR.Mathlib.LinearAlgebra.Dimension.Finrank (1.7s)
✔ [2858/2891] Built PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (1.8s)
✔ [2860/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (2.1s)
✔ [2862/2901] Built PFR.Mathlib.LinearAlgebra.Quotient.Basic (1.5s)
✔ [2865/2901] Built APAP.Prereqs.Convolution.Discrete.Defs (8.9s)
✔ [2866/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpace (259ms)
✔ [2867/2901] Built PFR.ForMathlib.AffineSpaceDim (2.2s)
✔ [2868/2901] Built PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic (1.4s)
✔ [2869/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef (2.0s)
✔ [2870/2901] Built PFR.ForMathlib.Entropy.Kernel.MutualInfo (4.3s)
✔ [2871/2901] Built PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability (2.5s)
✔ [2872/2901] Built APAP.Prereqs.Convolution.Order (4.1s)
✔ [2873/2901] Built PFR.ForMathlib.Entropy.Kernel.Group (3.7s)
✔ [2874/2901] Built APAP.Prereqs.Convolution.Discrete.Basic (5.5s)
✔ [2875/2901] Built PFR.ForMathlib.Entropy.Kernel.RuzsaDist (6.5s)
✔ [2876/2901] Built PFR.ForMathlib.Entropy.Basic (9.0s)
✔ [2877/2901] Built PFR.ForMathlib.Entropy.Group (4.4s)
✔ [2878/2901] Built PFR.Kullback (6.1s)
✔ [2879/2901] Built APAP.Extras.BSG (15s)
✔ [2880/2901] Built PFR.ForMathlib.Entropy.RuzsaDist (10s)
✔ [2881/2901] Built PFR.Fibring (4.5s)
✔ [2882/2901] Built PFR.ForMathlib.Entropy.RuzsaSetDist (4.5s)
✔ [2883/2901] Built PFR.HundredPercent (4.8s)
✔ [2884/2901] Built PFR.TauFunctional (5.4s)
✔ [2885/2901] Built PFR.FirstEstimate (5.9s)
✔ [2886/2901] Built PFR.SecondEstimate (5.6s)
✔ [2887/2901] Built PFR.Endgame (20s)
✔ [2888/2901] Built PFR.EntropyPFR (2.9s)
✔ [2889/2901] Built PFR.Main (6.4s)
✔ [2890/2901] Built PFR.MoreRuzsaDist (49s)
✔ [2891/2901] Built PFR.MultiTauFunctional (3.0s)
✔ [2892/2901] Built PFR.ImprovedPFR (30s)
✔ [2893/2901] Built PFR.RhoFunctional (38s)
✔ [2894/2901] Built PFR.BoundingMutual (29s)
✔ [2895/2901] Built PFR.HomPFR (8.3s)
✔ [2896/2901] Built PFR.WeakPFR (17s)
✔ [2897/2901] Built PFR.ApproxHomPFR (13s)
✔ [2898/2901] Built PFR.TorsionEndgame (26s)
✔ [2899/2901] Built PFR.Examples (9.5s)
✔ [2900/2901] Built PFR (2.2s)
Build completed successfully (2901 jobs).

semantic_extract exit 1 duration 298 ms · created 6/1/2026, 5:29:40 PM

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

lean semantic helper failed: missing required command 'lean'
remediation: install Lean toolchain (elan + lake) and ensure PATH is configured