Verification run
Run 10
succeeded commit
manual toolchain lean-v4-28-0-rc1 prover lean took 9m 38s · finished 6w ago
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
git clone --depth 1 --branch master --single-branch https://github.com/Gogopex/pfr.git /var/lib/apodeixis/repos/job-44-source
Cloning into '/var/lib/apodeixis/repos/job-44-source'...
lake_cache exit 0
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 21972 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.Init (330ms)
✔ [3/22] Built Cache.Lean (395ms)
✔ [4/22] Built Cache.Lean:c.o (352ms)
✔ [5/22] Built Cache.Init:c.o (386ms)
✔ [6/22] Built Cache.IO (1.3s)
✔ [7/22] Built Cache.Hashing (779ms)
✔ [8/22] Built Cache.IO:c.o (1.2s)
✔ [9/22] Built Cache.Hashing:c.o (409ms)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (153ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (211ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (201ms)
✔ [18/22] Built Cache.Requests (1.5s)
✔ [19/22] Built Cache.Main (731ms)
✔ [20/22] Built Cache.Main:c.o (441ms)
✔ [21/22] Built Cache.Requests:c.o (1.3s)
✔ [22/22] Built cache:exe (2.2s)
% 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 2529k 0 --:--:-- --:--:-- --:--:-- 2529k
Downloaded: 1 file(s) [attempted 1/7954 = 0%, 10 KB/s]
Downloaded: 15 file(s) [attempted 15/7954 = 0%, 26 KB/s]
Downloaded: 37 file(s) [attempted 37/7954 = 0%, 15 KB/s]
Downloaded: 65 file(s) [attempted 65/7954 = 0%, 206 KB/s]
Downloaded: 99 file(s) [attempted 99/7954 = 1%, 43 KB/s]
Downloaded: 127 file(s) [attempted 127/7954 = 1%, 73 KB/s]
Downloaded: 161 file(s) [attempted 161/7954 = 2%, 435 KB/s]
Downloaded: 196 file(s) [attempted 196/7954 = 2%, 539 KB/s]
Downloaded: 230 file(s) [attempted 230/7954 = 2%, 243 KB/s]
Downloaded: 275 file(s) [attempted 275/7954 = 3%, 86 KB/s]
Downloaded: 319 file(s) [attempted 319/7954 = 4%, 488 KB/s]
Downloaded: 357 file(s) [attempted 357/7954 = 4%, 469 KB/s]
Downloaded: 391 file(s) [attempted 391/7954 = 4%, 152 KB/s]
Downloaded: 425 file(s) [attempted 425/7954 = 5%, 471 KB/s]
Downloaded: 466 file(s) [attempted 466/7954 = 5%, 300 KB/s]
Downloaded: 513 file(s) [attempted 513/7954 = 6%, 377 KB/s]
Downloaded: 552 file(s) [attempted 552/7954 = 6%, 362 KB/s]
Downloaded: 590 file(s) [attempted 590/7954 = 7%, 1472 KB/s]
Downloaded: 617 file(s) [attempted 617/7954 = 7%, 255 KB/s]
Downloaded: 662 file(s) [attempted 662/7954 = 8%, 234 KB/s]
Downloaded: 706 file(s) [attempted 706/7954 = 8%, 352 KB/s]
Downloaded: 743 file(s) [attempted 743/7954 = 9%, 484 KB/s]
Downloaded: 778 file(s) [attempted 778/7954 = 9%, 747 KB/s]
Downloaded: 816 file(s) [attempted 816/7954 = 10%, 177 KB/s]
Downloaded: 857 file(s) [attempted 857/7954 = 10%, 159 KB/s]
Downloaded: 901 file(s) [attempted 901/7954 = 11%, 177 KB/s]
Downloaded: 936 file(s) [attempted 936/7954 = 11%, 49 KB/s]
Downloaded: 973 file(s) [attempted 973/7954 = 12%, 188 KB/s]
Downloaded: 1011 file(s) [attempted 1011/7954 = 12%, 718 KB/s]
Downloaded: 1049 file(s) [attempted 1049/7954 = 13%, 598 KB/s]
Downloaded: 1086 file(s) [attempted 1086/7954 = 13%, 212 KB/s]
Downloaded: 1124 file(s) [attempted 1124/7954 = 14%, 124 KB/s]
Downloaded: 1162 file(s) [attempted 1162/7954 = 14%, 189 KB/s]
Downloaded: 1203 file(s) [attempted 1203/7954 = 15%, 620 KB/s]
Downloaded: 1240 file(s) [attempted 1240/7954 = 15%, 421 KB/s]
Downloaded: 1281 file(s) [attempted 1281/7954 = 16%, 58 KB/s]
Downloaded: 1316 file(s) [attempted 1316/7954 = 16%, 272 KB/s]
Downloaded: 1353 file(s) [attempted 1353/7954 = 17%, 1512 KB/s]
Downloaded: 1394 file(s) [attempted 1394/7954 = 17%, 615 KB/s]
Downloaded: 1432 file(s) [attempted 1432/7954 = 18%, 1642 KB/s]
Downloaded: 1470 file(s) [attempted 1470/7954 = 18%, 390 KB/s]
Downloaded: 1504 file(s) [attempted 1504/7954 = 18%, 597 KB/s]
Downloaded: 1543 file(s) [attempted 1543/7954 = 19%, 227 KB/s]
Downloaded: 1586 file(s) [attempted 1586/7954 = 19%, 346 KB/s]
Downloaded: 1627 file(s) [attempted 1627/7954 = 20%, 654 KB/s]
Downloaded: 1665 file(s) [attempted 1665/7954 = 20%, 967 KB/s]
Downloaded: 1702 file(s) [attempted 1702/7954 = 21%, 270 KB/s]
Downloaded: 1740 file(s) [attempted 1740/7954 = 21%, 142 KB/s]
Downloaded: 1778 file(s) [attempted 1778/7954 = 22%, 330 KB/s]
Downloaded: 1822 file(s) [attempted 1822/7954 = 22%, 456 KB/s]
Downloaded: 1863 file(s) [attempted 1863/7954 = 23%, 200 KB/s]
Downloaded: 1901 file(s) [attempted 1901/7954 = 23%, 1267 KB/s]
Downloaded: 1935 file(s) [attempted 1935/7954 = 24%, 315 KB/s]
Downloaded: 1976 file(s) [attempted 1976/7954 = 24%, 102 KB/s]
Downloaded: 2017 file(s) [attempted 2017/7954 = 25%, 119 KB/s]
Downloaded: 2055 file(s) [attempted 2055/7954 = 25%, 1103 KB/s]
Downloaded: 2096 file(s) [attempted 2096/7954 = 26%, 202 KB/s]
Downloaded: 2140 file(s) [attempted 2140/7954 = 26%, 305 KB/s]
Downloaded: 2175 file(s) [attempted 2175/7954 = 27%, 188 KB/s]
Downloaded: 2216 file(s) [attempted 2216/7954 = 27%, 732 KB/s]
Downloaded: 2250 file(s) [attempted 2250/7954 = 28%, 367 KB/s]
Downloaded: 2288 file(s) [attempted 2288/7954 = 28%, 1281 KB/s]
Downloaded: 2329 file(s) [attempted 2329/7954 = 29%, 1634 KB/s]
Downloaded: 2366 file(s) [attempted 2366/7954 = 29%, 389 KB/s]
Downloaded: 2404 file(s) [attempted 2404/7954 = 30%, 1080 KB/s]
Downloaded: 2440 file(s) [attempted 2440/7954 = 30%, 311 KB/s]
Downloaded: 2479 file(s) [attempted 2479/7954 = 31%, 87 KB/s]
Downloaded: 2513 file(s) [attempted 2513/7954 = 31%, 579 KB/s]
Downloaded: 2551 file(s) [attempted 2551/7954 = 32%, 155 KB/s]
Downloaded: 2592 file(s) [attempted 2592/7954 = 32%, 676 KB/s]
Downloaded: 2630 file(s) [attempted 2630/7954 = 33%, 1119 KB/s]
Downloaded: 2664 file(s) [attempted 2664/7954 = 33%, 380 KB/s]
Downloaded: 2698 file(s) [attempted 2698/7954 = 33%, 94 KB/s]
Downloaded: 2739 file(s) [attempted 2739/7954 = 34%, 136 KB/s]
Downloaded: 2780 file(s) [attempted 2780/7954 = 34%, 707 KB/s]
Downloaded: 2821 file(s) [attempted 2821/7954 = 35%, 327 KB/s]
Downloaded: 2859 file(s) [attempted 2859/7954 = 35%, 1039 KB/s]
Downloaded: 2893 file(s) [attempted 2893/7954 = 36%, 339 KB/s]
Downloaded: 2938 file(s) [attempted 2938/7954 = 36%, 66 KB/s]
Downloaded: 2975 file(s) [attempted 2975/7954 = 37%, 950 KB/s]
Downloaded: 3013 file(s) [attempted 3013/7954 = 37%, 176 KB/s]
Downloaded: 3054 file(s) [attempted 3054/7954 = 38%, 41 KB/s]
Downloaded: 3092 file(s) [attempted 3092/7954 = 38%, 648 KB/s]
Downloaded: 3133 file(s) [attempted 3133/7954 = 39%, 369 KB/s]
Downloaded: 3174 file(s) [attempted 3174/7954 = 39%, 111 KB/s]
Downloaded: 3215 file(s) [attempted 3215/7954 = 40%, 80 KB/s]
Downloaded: 3249 file(s) [attempted 3249/7954 = 40%, 414 KB/s]
Downloaded: 3290 file(s) [attempted 3290/7954 = 41%, 274 KB/s]
Downloaded: 3331 file(s) [attempted 3331/7954 = 41%, 238 KB/s]
Downloaded: 3369 file(s) [attempted 3369/7954 = 42%, 34 KB/s]
Downloaded: 3403 file(s) [attempted 3403/7954 = 42%, 744 KB/s]
Downloaded: 3448 file(s) [attempted 3448/7954 = 43%, 302 KB/s]
Downloaded: 3489 file(s) [attempted 3489/7954 = 43%, 73 KB/s]
Downloaded: 3526 file(s) [attempted 3526/7954 = 44%, 96 KB/s]
Downloaded: 3564 file(s) [attempted 3564/7954 = 44%, 230 KB/s]
Downloaded: 3605 file(s) [attempted 3605/7954 = 45%, 277 KB/s]
Downloaded: 3646 file(s) [attempted 3646/7954 = 45%, 236 KB/s]
Downloaded: 3684 file(s) [attempted 3684/7954 = 46%, 325 KB/s]
Downloaded: 3722 file(s) [attempted 3722/7954 = 46%, 98 KB/s]
Downloaded: 3759 file(s) [attempted 3759/7954 = 47%, 164 KB/s]
Downloaded: 3793 file(s) [attempted 3793/7954 = 47%, 133 KB/s]
Downloaded: 3834 file(s) [attempted 3834/7954 = 48%, 632 KB/s]
Downloaded: 3869 file(s) [attempted 3869/7954 = 48%, 337 KB/s]
Downloaded: 3906 file(s) [attempted 3906/7954 = 49%, 368 KB/s]
Downloaded: 3944 file(s) [attempted 3944/7954 = 49%, 39 KB/s]
Downloaded: 3982 file(s) [attempted 3982/7954 = 50%, 160 KB/s]
Downloaded: 4023 file(s) [attempted 4023/7954 = 50%, 79 KB/s]
Downloaded: 4064 file(s) [attempted 4064/7954 = 51%, 338 KB/s]
Downloaded: 4101 file(s) [attempted 4101/7954 = 51%, 102 KB/s]
Downloaded: 4142 file(s) [attempted 4142/7954 = 52%, 540 KB/s]
Downloaded: 4180 file(s) [attempted 4180/7954 = 52%, 196 KB/s]
Downloaded: 4218 file(s) [attempted 4218/7954 = 53%, 236 KB/s]
Downloaded: 4255 file(s) [attempted 4255/7954 = 53%, 334 KB/s]
Downloaded: 4296 file(s) [attempted 4296/7954 = 54%, 339 KB/s]
Downloaded: 4334 file(s) [attempted 4334/7954 = 54%, 65 KB/s]
Downloaded: 4372 file(s) [attempted 4372/7954 = 54%, 263 KB/s]
Downloaded: 4409 file(s) [attempted 4409/7954 = 55%, 114 KB/s]
Downloaded: 4450 file(s) [attempted 4450/7954 = 55%, 943 KB/s]
Downloaded: 4488 file(s) [attempted 4488/7954 = 56%, 403 KB/s]
Downloaded: 4533 file(s) [attempted 4533/7954 = 56%, 252 KB/s]
Downloaded: 4570 file(s) [attempted 4570/7954 = 57%, 257 KB/s]
Downloaded: 4607 file(s) [attempted 4607/7954 = 57%, 127 KB/s]
Downloaded: 4646 file(s) [attempted 4646/7954 = 58%, 516 KB/s]
Downloaded: 4683 file(s) [attempted 4683/7954 = 58%, 75 KB/s]
Downloaded: 4717 file(s) [attempted 4717/7954 = 59%, 105 KB/s]
Downloaded: 4755 file(s) [attempted 4755/7954 = 59%, 37 KB/s]
Downloaded: 4796 file(s) [attempted 4796/7954 = 60%, 81 KB/s]
Downloaded: 4834 file(s) [attempted 4834/7954 = 60%, 82 KB/s]
Downloaded: 4871 file(s) [attempted 4871/7954 = 61%, 469 KB/s]
Downloaded: 4909 file(s) [attempted 4909/7954 = 61%, 64 KB/s]
Downloaded: 4950 file(s) [attempted 4950/7954 = 62%, 225 KB/s]
Downloaded: 4995 file(s) [attempted 4995/7954 = 62%, 135 KB/s]
Downloaded: 5032 file(s) [attempted 5032/7954 = 63%, 209 KB/s]
Downloaded: 5073 file(s) [attempted 5073/7954 = 63%, 350 KB/s]
Downloaded: 5111 file(s) [attempted 5111/7954 = 64%, 1030 KB/s]
Downloaded: 5145 file(s) [attempted 5145/7954 = 64%, 81 KB/s]
Downloaded: 5186 file(s) [attempted 5186/7954 = 65%, 427 KB/s]
Downloaded: 5227 file(s) [attempted 5227/7954 = 65%, 148 KB/s]
Downloaded: 5272 file(s) [attempted 5272/7954 = 66%, 234 KB/s]
Downloaded: 5313 file(s) [attempted 5313/7954 = 66%, 1018 KB/s]
Downloaded: 5350 file(s) [attempted 5350/7954 = 67%, 792 KB/s]
Downloaded: 5388 file(s) [attempted 5388/7954 = 67%, 547 KB/s]
Downloaded: 5422 file(s) [attempted 5422/7954 = 68%, 811 KB/s]
Downloaded: 5463 file(s) [attempted 5463/7954 = 68%, 220 KB/s]
Downloaded: 5505 file(s) [attempted 5505/7954 = 69%, 707 KB/s]
Downloaded: 5542 file(s) [attempted 5542/7954 = 69%, 604 KB/s]
Downloaded: 5580 file(s) [attempted 5580/7954 = 70%, 367 KB/s]
Downloaded: 5614 file(s) [attempted 5614/7954 = 70%, 64 KB/s]
Downloaded: 5659 file(s) [attempted 5659/7954 = 71%, 91 KB/s]
Downloaded: 5697 file(s) [attempted 5697/7954 = 71%, 943 KB/s]
Downloaded: 5734 file(s) [attempted 5734/7954 = 72%, 756 KB/s]
Downloaded: 5775 file(s) [attempted 5775/7954 = 72%, 154 KB/s]
Downloaded: 5802 file(s) [attempted 5802/7954 = 72%, 788 KB/s]
Downloaded: 5847 file(s) [attempted 5847/7954 = 73%, 159 KB/s]
Downloaded: 5891 file(s) [attempted 5891/7954 = 74%, 107 KB/s]
Downloaded: 5936 file(s) [attempted 5936/7954 = 74%, 53 KB/s]
Downloaded: 5973 file(s) [attempted 5973/7954 = 75%, 243 KB/s]
Downloaded: 6011 file(s) [attempted 6011/7954 = 75%, 46 KB/s]
Downloaded: 6042 file(s) [attempted 6042/7954 = 75%, 459 KB/s]
Downloaded: 6086 file(s) [attempted 6086/7954 = 76%, 461 KB/s]
Downloaded: 6127 file(s) [attempted 6127/7954 = 77%, 145 KB/s]
Downloaded: 6165 file(s) [attempted 6165/7954 = 77%, 309 KB/s]
Downloaded: 6199 file(s) [attempted 6199/7954 = 77%, 112 KB/s]
Downloaded: 6240 file(s) [attempted 6240/7954 = 78%, 455 KB/s]
Downloaded: 6285 file(s) [attempted 6285/7954 = 79%, 657 KB/s]
Downloaded: 6325 file(s) [attempted 6325/7954 = 79%, 240 KB/s]
Downloaded: 6360 file(s) [attempted 6360/7954 = 79%, 66 KB/s]
Downloaded: 6398 file(s) [attempted 6398/7954 = 80%, 104 KB/s]
Downloaded: 6439 file(s) [attempted 6439/7954 = 80%, 59 KB/s]
Downloaded: 6476 file(s) [attempted 6476/7954 = 81%, 539 KB/s]
Downloaded: 6517 file(s) [attempted 6517/7954 = 81%, 230 KB/s]
Downloaded: 6559 file(s) [attempted 6559/7954 = 82%, 737 KB/s]
Downloaded: 6596 file(s) [attempted 6596/7954 = 82%, 382 KB/s]
Downloaded: 6637 file(s) [attempted 6637/7954 = 83%, 894 KB/s]
Downloaded: 6675 file(s) [attempted 6675/7954 = 83%, 1840 KB/s]
Downloaded: 6711 file(s) [attempted 6711/7954 = 84%, 129 KB/s]
Downloaded: 6750 file(s) [attempted 6750/7954 = 84%, 44 KB/s]
Downloaded: 6788 file(s) [attempted 6788/7954 = 85%, 2823 KB/s]
Downloaded: 6832 file(s) [attempted 6832/7954 = 85%, 43 KB/s]
Downloaded: 6877 file(s) [attempted 6877/7954 = 86%, 188 KB/s]
Downloaded: 6914 file(s) [attempted 6914/7954 = 86%, 240 KB/s]
Downloaded: 6952 file(s) [attempted 6952/7954 = 87%, 113 KB/s]
Downloaded: 6997 file(s) [attempted 6997/7954 = 87%, 132 KB/s]
Downloaded: 7034 file(s) [attempted 7034/7954 = 88%, 1396 KB/s]
Downloaded: 7079 file(s) [attempted 7079/7954 = 88%, 1065 KB/s]
Downloaded: 7120 file(s) [attempted 7120/7954 = 89%, 851 KB/s]
Downloaded: 7157 file(s) [attempted 7157/7954 = 89%, 127 KB/s]
Downloaded: 7198 file(s) [attempted 7198/7954 = 90%, 560 KB/s]
Downloaded: 7236 file(s) [attempted 7236/7954 = 90%, 85 KB/s]
Downloaded: 7274 file(s) [attempted 7274/7954 = 91%, 87 KB/s]
Downloaded: 7311 file(s) [attempted 7311/7954 = 91%, 202 KB/s]
Downloaded: 7351 file(s) [attempted 7351/7954 = 92%, 44 KB/s]
Downloaded: 7387 file(s) [attempted 7387/7954 = 92%, 31 KB/s]
Downloaded: 7424 file(s) [attempted 7424/7954 = 93%, 2500 KB/s]
Downloaded: 7465 file(s) [attempted 7465/7954 = 93%, 134 KB/s]
Downloaded: 7503 file(s) [attempted 7503/7954 = 94%, 218 KB/s]
Downloaded: 7543 file(s) [attempted 7543/7954 = 94%, 522 KB/s]
Downloaded: 7582 file(s) [attempted 7582/7954 = 95%, 95 KB/s]
Downloaded: 7623 file(s) [attempted 7623/7954 = 95%, 216 KB/s]
Downloaded: 7660 file(s) [attempted 7660/7954 = 96%, 757 KB/s]
Downloaded: 7702 file(s) [attempted 7702/7954 = 96%, 100 KB/s]
Downloaded: 7739 file(s) [attempted 7739/7954 = 97%, 483 KB/s]
Downloaded: 7777 file(s) [attempted 7777/7954 = 97%, 170 KB/s]
Downloaded: 7818 file(s) [attempted 7818/7954 = 98%, 145 KB/s]
Downloaded: 7856 file(s) [attempted 7856/7954 = 98%, 931 KB/s]
Downloaded: 7897 file(s) [attempted 7897/7954 = 99%, 54 KB/s]
Downloaded: 7941 file(s) [attempted 7941/7954 = 99%, 227 KB/s]
Downloaded: 7951 file(s) [attempted 7951/7954 = 99%, 667 KB/s]
Downloaded: 7954 file(s) [attempted 7954/7954 = 100%, 667 KB/s]
lean_checker exit 0
lake build
✔ [1886/1916] Built PFR.ForMathlib.Pair (4.9s) ✔ [2125/2202] Built PFR.Mathlib.MeasureTheory.Constructions.Pi (5.6s) ✔ [2600/2622] Built PFR.Mathlib.LinearAlgebra.Basis.VectorSpace (7.4s) ✔ [2601/2623] Built PFR.Mathlib.Probability.Independence.Kernel.IndepFun (7.8s) ✔ [2610/2626] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic (3.3s) ✔ [2660/2683] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable (2.8s) ✔ [2661/2683] Built PFR.ForMathlib.FiniteRange.Defs (4.8s) ✔ [2662/2683] Built PFR.Mathlib.MeasureTheory.Measure.Dirac (2.4s) ✔ [2664/2683] Built PFR.Mathlib.Data.Set.Basic (1.0s) ✔ [2666/2683] Built PFR.Mathlib.MeasureTheory.Measure.Prod (3.7s) ✔ [2667/2683] Built PFR.Mathlib.Probability.Independence.Basic (6.1s) ✔ [2669/2683] Built PFR.Mathlib.Data.Set.Insert (2.0s) ✔ [2670/2683] Built PFR.ForMathlib.FiniteRange.ConditionalProbability (2.7s) ✔ [2675/2689] Built PFR.Mathlib.MeasureTheory.Measure.Real (2.6s) ✔ [2676/2698] Built PFR.ForMathlib.ThreeVariables (2.9s) ✔ [2762/2783] Built PFR.Mathlib.Data.Set.Card (1.8s) ✔ [2764/2783] Built PFR.Mathlib.Probability.ConditionalProbability (2.4s) ✔ [2771/2789] Built PFR.Mathlib.MeasureTheory.Integral.Bochner.Set (3.5s) ✔ [2776/2792] Built PFR.Mathlib.Probability.IdentDistrib (9.6s) ✔ [2779/2792] Built PFR.Mathlib.Probability.UniformOn (4.2s) ✔ [2781/2792] Built PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog (6.7s) ✔ [2782/2793] Built PFR.Mathlib.Probability.Kernel.Disintegration (12s) ✔ [2784/2806] Built PFR.ForMathlib.ConditionalIndependence (8.8s) ✔ [2789/2811] Built PFR.Mathlib.Probability.Kernel.Composition.Comp (6.5s) ✔ [2795/2811] Built PFR.ForMathlib.Uniform (9.5s) ✔ [2815/2840] Built PFR.ForMathlib.FiniteRange.IdentDistrib (4.7s) ✔ [2821/2858] Built PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure (4.0s) ✔ [2841/2867] Built PFR.ForMathlib.Entropy.Measure (14s) ✔ [2842/2867] Built APAP.Prereqs.Function.Indicator.Defs (4.9s) ✔ [2843/2868] Built PFR.Tactic.RPowSimp (7.2s) ✔ [2845/2868] Built PFR.ForMathlib.FourVariables (8.5s) ✔ [2846/2889] Built APAP.Prereqs.Function.Indicator.Basic (2.2s) ✔ [2850/2889] Built APAP.Prereqs.DummyPositivity (1.5s) ✔ [2851/2889] Built PFR.Mathlib.Data.Fin.Basic (2.5s) ✔ [2852/2889] Built PFR.Mathlib.Algebra.BigOperators.Fin (3.3s) ✔ [2853/2890] Built PFR.ForMathlib.Entropy.Kernel.Basic (7.6s) ✔ [2855/2890] Built APAP.Prereqs.Convolution.Discrete.Defs (12s) ✔ [2856/2890] Built PFR.Mathlib.MeasureTheory.Group.Arithmetic (2.9s) ✔ [2857/2890] Built PFR.Mathlib.Order.Interval.Finset.Fin (1.9s) ✔ [2859/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.Finrank (1.9s) ✔ [2860/2901] Built PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (1.7s) ✔ [2862/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (2.1s) ✔ [2863/2901] Built PFR.Mathlib.LinearAlgebra.Quotient.Basic (2.1s) ✔ [2864/2901] Built PFR.ForMathlib.AffineSpaceDim (3.5s) ✔ [2867/2901] Built APAP.Prereqs.Convolution.Order (4.6s) ✔ [2868/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpace (980ms) ✔ [2869/2901] Built PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic (2.1s) ✔ [2870/2901] Built PFR.ForMathlib.Entropy.Kernel.MutualInfo (6.6s) ✔ [2871/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef (2.4s) ✔ [2872/2901] Built APAP.Prereqs.Convolution.Discrete.Basic (7.3s) ✔ [2873/2901] Built PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability (3.1s) ✔ [2874/2901] Built PFR.ForMathlib.Entropy.Kernel.Group (5.9s) ✔ [2875/2901] Built PFR.ForMathlib.Entropy.Basic (13s) ✔ [2876/2901] Built PFR.ForMathlib.Entropy.Kernel.RuzsaDist (7.0s) ✔ [2877/2901] Built PFR.ForMathlib.Entropy.Group (5.4s) ✔ [2878/2901] Built PFR.Kullback (7.2s) ✔ [2879/2901] Built APAP.Extras.BSG (20s) ✔ [2880/2901] Built PFR.ForMathlib.Entropy.RuzsaDist (12s) ✔ [2881/2901] Built PFR.Fibring (4.9s) ✔ [2882/2901] Built PFR.ForMathlib.Entropy.RuzsaSetDist (5.2s) ✔ [2883/2901] Built PFR.HundredPercent (6.3s) ✔ [2884/2901] Built PFR.TauFunctional (6.4s) ✔ [2885/2901] Built PFR.FirstEstimate (6.9s) ✔ [2886/2901] Built PFR.SecondEstimate (6.0s) ✔ [2887/2901] Built PFR.Endgame (20s) ✔ [2888/2901] Built PFR.EntropyPFR (3.5s) ✔ [2889/2901] Built PFR.Main (7.5s) ✔ [2890/2901] Built PFR.MoreRuzsaDist (60s) ✔ [2891/2901] Built PFR.MultiTauFunctional (7.4s) ✔ [2892/2901] Built PFR.ImprovedPFR (38s) ✔ [2893/2901] Built PFR.RhoFunctional (51s) ✔ [2894/2901] Built PFR.WeakPFR (23s) ✔ [2895/2901] Built PFR.HomPFR (11s) ✔ [2896/2901] Built PFR.BoundingMutual (40s) ✔ [2897/2901] Built PFR.ApproxHomPFR (16s) ✔ [2898/2901] Built PFR.Examples (9.9s) ✔ [2899/2901] Built PFR.TorsionEndgame (28s) ✔ [2900/2901] Built PFR (2.1s) Build completed successfully (2901 jobs).
blueprint_build exit 1
lake build :blueprint
error: unknown package facet `package.blueprint`
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh