Verification run
Run 9
succeeded commit
manual toolchain lean-v4-28-0-rc1 prover lean took 8m 49s · 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-9-source
Cloning into '/var/lib/apodeixis/repos/job-9-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 17309 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 (367ms)
✔ [3/22] Built Cache.Init (309ms)
✔ [4/22] Built Cache.Lean:c.o (177ms)
✔ [5/22] Built Cache.Init:c.o (218ms)
✔ [6/22] Built Cache.IO (1.3s)
✔ [7/22] Built Cache.Hashing (673ms)
✔ [8/22] Built Cache.Hashing:c.o (409ms)
✔ [9/22] Built Cache.IO:c.o (1.2s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (118ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (202ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (183ms)
✔ [18/22] Built Cache.Requests (1.3s)
✔ [19/22] Built Cache.Main (665ms)
✔ [20/22] Built Cache.Main:c.o (445ms)
✔ [21/22] Built Cache.Requests:c.o (1.3s)
✔ [22/22] Built cache:exe (2.3s)
% 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 2539k 0 --:--:-- --:--:-- --:--:-- 2539k
Downloaded: 1 file(s) [attempted 1/7954 = 0%, 10 KB/s]
Downloaded: 13 file(s) [attempted 13/7954 = 0%, 2 KB/s]
Downloaded: 34 file(s) [attempted 34/7954 = 0%, 18 KB/s]
Downloaded: 60 file(s) [attempted 60/7954 = 0%, 62 KB/s]
Downloaded: 89 file(s) [attempted 89/7954 = 1%, 514 KB/s]
Downloaded: 127 file(s) [attempted 127/7954 = 1%, 97 KB/s]
Downloaded: 161 file(s) [attempted 161/7954 = 2%, 440 KB/s]
Downloaded: 189 file(s) [attempted 189/7954 = 2%, 337 KB/s]
Downloaded: 230 file(s) [attempted 230/7954 = 2%, 628 KB/s]
Downloaded: 275 file(s) [attempted 275/7954 = 3%, 91 KB/s]
Downloaded: 323 file(s) [attempted 323/7954 = 4%, 240 KB/s]
Downloaded: 367 file(s) [attempted 367/7954 = 4%, 98 KB/s]
Downloaded: 405 file(s) [attempted 405/7954 = 5%, 36 KB/s]
Downloaded: 443 file(s) [attempted 443/7954 = 5%, 735 KB/s]
Downloaded: 480 file(s) [attempted 480/7954 = 6%, 95 KB/s]
Downloaded: 525 file(s) [attempted 525/7954 = 6%, 81 KB/s]
Downloaded: 566 file(s) [attempted 566/7954 = 7%, 166 KB/s]
Downloaded: 600 file(s) [attempted 600/7954 = 7%, 95 KB/s]
Downloaded: 641 file(s) [attempted 641/7954 = 8%, 450 KB/s]
Downloaded: 686 file(s) [attempted 686/7954 = 8%, 137 KB/s]
Downloaded: 730 file(s) [attempted 730/7954 = 9%, 231 KB/s]
Downloaded: 768 file(s) [attempted 768/7954 = 9%, 821 KB/s]
Downloaded: 802 file(s) [attempted 802/7954 = 10%, 183 KB/s]
Downloaded: 843 file(s) [attempted 843/7954 = 10%, 53 KB/s]
Downloaded: 888 file(s) [attempted 888/7954 = 11%, 312 KB/s]
Downloaded: 932 file(s) [attempted 932/7954 = 11%, 436 KB/s]
Downloaded: 977 file(s) [attempted 977/7954 = 12%, 233 KB/s]
Downloaded: 1014 file(s) [attempted 1014/7954 = 12%, 1890 KB/s]
Downloaded: 1059 file(s) [attempted 1059/7954 = 13%, 528 KB/s]
Downloaded: 1093 file(s) [attempted 1093/7954 = 13%, 238 KB/s]
Downloaded: 1134 file(s) [attempted 1134/7954 = 14%, 88 KB/s]
Downloaded: 1179 file(s) [attempted 1179/7954 = 14%, 285 KB/s]
Downloaded: 1219 file(s) [attempted 1219/7954 = 15%, 1102 KB/s]
Downloaded: 1260 file(s) [attempted 1260/7954 = 15%, 802 KB/s]
Downloaded: 1299 file(s) [attempted 1299/7954 = 16%, 463 KB/s]
Downloaded: 1336 file(s) [attempted 1336/7954 = 16%, 108 KB/s]
Downloaded: 1381 file(s) [attempted 1381/7954 = 17%, 356 KB/s]
Downloaded: 1418 file(s) [attempted 1418/7954 = 17%, 147 KB/s]
Downloaded: 1459 file(s) [attempted 1459/7954 = 18%, 141 KB/s]
Downloaded: 1499 file(s) [attempted 1499/7954 = 18%, 134 KB/s]
Downloaded: 1541 file(s) [attempted 1541/7954 = 19%, 201 KB/s]
Downloaded: 1586 file(s) [attempted 1586/7954 = 19%, 148 KB/s]
Downloaded: 1624 file(s) [attempted 1624/7954 = 20%, 143 KB/s]
Downloaded: 1664 file(s) [attempted 1664/7954 = 20%, 117 KB/s]
Downloaded: 1706 file(s) [attempted 1706/7954 = 21%, 843 KB/s]
Downloaded: 1743 file(s) [attempted 1743/7954 = 21%, 280 KB/s]
Downloaded: 1784 file(s) [attempted 1784/7954 = 22%, 135 KB/s]
Downloaded: 1822 file(s) [attempted 1822/7954 = 22%, 78 KB/s]
Downloaded: 1856 file(s) [attempted 1856/7954 = 23%, 525 KB/s]
Downloaded: 1897 file(s) [attempted 1897/7954 = 23%, 155 KB/s]
Downloaded: 1938 file(s) [attempted 1938/7954 = 24%, 268 KB/s]
Downloaded: 1980 file(s) [attempted 1980/7954 = 24%, 96 KB/s]
Downloaded: 2017 file(s) [attempted 2017/7954 = 25%, 118 KB/s]
Downloaded: 2058 file(s) [attempted 2058/7954 = 25%, 790 KB/s]
Downloaded: 2096 file(s) [attempted 2096/7954 = 26%, 167 KB/s]
Downloaded: 2137 file(s) [attempted 2137/7954 = 26%, 321 KB/s]
Downloaded: 2181 file(s) [attempted 2181/7954 = 27%, 90 KB/s]
Downloaded: 2219 file(s) [attempted 2219/7954 = 27%, 319 KB/s]
Downloaded: 2253 file(s) [attempted 2253/7954 = 28%, 291 KB/s]
Downloaded: 2298 file(s) [attempted 2298/7954 = 28%, 40 KB/s]
Downloaded: 2341 file(s) [attempted 2341/7954 = 29%, 59 KB/s]
Downloaded: 2380 file(s) [attempted 2380/7954 = 29%, 118 KB/s]
Downloaded: 2418 file(s) [attempted 2418/7954 = 30%, 239 KB/s]
Downloaded: 2455 file(s) [attempted 2455/7954 = 30%, 579 KB/s]
Downloaded: 2496 file(s) [attempted 2496/7954 = 31%, 1308 KB/s]
Downloaded: 2537 file(s) [attempted 2537/7954 = 31%, 72 KB/s]
Downloaded: 2582 file(s) [attempted 2582/7954 = 32%, 593 KB/s]
Downloaded: 2626 file(s) [attempted 2626/7954 = 33%, 1675 KB/s]
Downloaded: 2664 file(s) [attempted 2664/7954 = 33%, 1658 KB/s]
Downloaded: 2705 file(s) [attempted 2705/7954 = 34%, 576 KB/s]
Downloaded: 2746 file(s) [attempted 2746/7954 = 34%, 156 KB/s]
Downloaded: 2784 file(s) [attempted 2784/7954 = 35%, 218 KB/s]
Downloaded: 2821 file(s) [attempted 2821/7954 = 35%, 161 KB/s]
Downloaded: 2869 file(s) [attempted 2869/7954 = 36%, 312 KB/s]
Downloaded: 2914 file(s) [attempted 2914/7954 = 36%, 1715 KB/s]
Downloaded: 2955 file(s) [attempted 2955/7954 = 37%, 101 KB/s]
Downloaded: 2996 file(s) [attempted 2996/7954 = 37%, 82 KB/s]
Downloaded: 3030 file(s) [attempted 3030/7954 = 38%, 595 KB/s]
Downloaded: 3075 file(s) [attempted 3075/7954 = 38%, 399 KB/s]
Downloaded: 3116 file(s) [attempted 3116/7954 = 39%, 1308 KB/s]
Downloaded: 3157 file(s) [attempted 3157/7954 = 39%, 1909 KB/s]
Downloaded: 3205 file(s) [attempted 3205/7954 = 40%, 45 KB/s]
Downloaded: 3249 file(s) [attempted 3249/7954 = 40%, 191 KB/s]
Downloaded: 3290 file(s) [attempted 3290/7954 = 41%, 584 KB/s]
Downloaded: 3324 file(s) [attempted 3324/7954 = 41%, 85 KB/s]
Downloaded: 3366 file(s) [attempted 3366/7954 = 42%, 201 KB/s]
Downloaded: 3410 file(s) [attempted 3410/7954 = 42%, 358 KB/s]
Downloaded: 3458 file(s) [attempted 3458/7954 = 43%, 266 KB/s]
Downloaded: 3496 file(s) [attempted 3496/7954 = 43%, 50 KB/s]
Downloaded: 3533 file(s) [attempted 3533/7954 = 44%, 126 KB/s]
Downloaded: 3574 file(s) [attempted 3574/7954 = 44%, 815 KB/s]
Downloaded: 3612 file(s) [attempted 3612/7954 = 45%, 907 KB/s]
Downloaded: 3660 file(s) [attempted 3660/7954 = 46%, 399 KB/s]
Downloaded: 3704 file(s) [attempted 3704/7954 = 46%, 75 KB/s]
Downloaded: 3735 file(s) [attempted 3735/7954 = 46%, 382 KB/s]
Downloaded: 3776 file(s) [attempted 3776/7954 = 47%, 658 KB/s]
Downloaded: 3817 file(s) [attempted 3817/7954 = 47%, 253 KB/s]
Downloaded: 3858 file(s) [attempted 3858/7954 = 48%, 180 KB/s]
Downloaded: 3903 file(s) [attempted 3903/7954 = 49%, 540 KB/s]
Downloaded: 3939 file(s) [attempted 3939/7954 = 49%, 988 KB/s]
Downloaded: 3978 file(s) [attempted 3978/7954 = 50%, 554 KB/s]
Downloaded: 4023 file(s) [attempted 4023/7954 = 50%, 241 KB/s]
Downloaded: 4067 file(s) [attempted 4067/7954 = 51%, 190 KB/s]
Downloaded: 4108 file(s) [attempted 4108/7954 = 51%, 147 KB/s]
Downloaded: 4146 file(s) [attempted 4146/7954 = 52%, 420 KB/s]
Downloaded: 4187 file(s) [attempted 4187/7954 = 52%, 183 KB/s]
Downloaded: 4228 file(s) [attempted 4228/7954 = 53%, 215 KB/s]
Downloaded: 4272 file(s) [attempted 4272/7954 = 53%, 129 KB/s]
Downloaded: 4313 file(s) [attempted 4313/7954 = 54%, 236 KB/s]
Downloaded: 4355 file(s) [attempted 4355/7954 = 54%, 267 KB/s]
Downloaded: 4392 file(s) [attempted 4392/7954 = 55%, 1177 KB/s]
Downloaded: 4433 file(s) [attempted 4433/7954 = 55%, 225 KB/s]
Downloaded: 4478 file(s) [attempted 4478/7954 = 56%, 114 KB/s]
Downloaded: 4522 file(s) [attempted 4522/7954 = 56%, 630 KB/s]
Downloaded: 4563 file(s) [attempted 4563/7954 = 57%, 115 KB/s]
Downloaded: 4601 file(s) [attempted 4601/7954 = 57%, 132 KB/s]
Downloaded: 4639 file(s) [attempted 4639/7954 = 58%, 91 KB/s]
Downloaded: 4683 file(s) [attempted 4683/7954 = 58%, 392 KB/s]
Downloaded: 4731 file(s) [attempted 4731/7954 = 59%, 77 KB/s]
Downloaded: 4779 file(s) [attempted 4779/7954 = 60%, 145 KB/s]
Downloaded: 4821 file(s) [attempted 4821/7954 = 60%, 581 KB/s]
Downloaded: 4861 file(s) [attempted 4861/7954 = 61%, 178 KB/s]
Downloaded: 4899 file(s) [attempted 4899/7954 = 61%, 196 KB/s]
Downloaded: 4936 file(s) [attempted 4936/7954 = 62%, 366 KB/s]
Downloaded: 4981 file(s) [attempted 4981/7954 = 62%, 730 KB/s]
Downloaded: 5029 file(s) [attempted 5029/7954 = 63%, 100 KB/s]
Downloaded: 5073 file(s) [attempted 5073/7954 = 63%, 355 KB/s]
Downloaded: 5111 file(s) [attempted 5111/7954 = 64%, 90 KB/s]
Downloaded: 5152 file(s) [attempted 5152/7954 = 64%, 208 KB/s]
Downloaded: 5193 file(s) [attempted 5193/7954 = 65%, 460 KB/s]
Downloaded: 5234 file(s) [attempted 5234/7954 = 65%, 148 KB/s]
Downloaded: 5271 file(s) [attempted 5271/7954 = 66%, 114 KB/s]
Downloaded: 5313 file(s) [attempted 5313/7954 = 66%, 1989 KB/s]
Downloaded: 5357 file(s) [attempted 5357/7954 = 67%, 131 KB/s]
Downloaded: 5398 file(s) [attempted 5398/7954 = 67%, 132 KB/s]
Downloaded: 5439 file(s) [attempted 5439/7954 = 68%, 136 KB/s]
Downloaded: 5480 file(s) [attempted 5480/7954 = 68%, 87 KB/s]
Downloaded: 5516 file(s) [attempted 5516/7954 = 69%, 96 KB/s]
Downloaded: 5559 file(s) [attempted 5559/7954 = 69%, 1808 KB/s]
Downloaded: 5600 file(s) [attempted 5600/7954 = 70%, 101 KB/s]
Downloaded: 5645 file(s) [attempted 5645/7954 = 70%, 157 KB/s]
Downloaded: 5682 file(s) [attempted 5682/7954 = 71%, 118 KB/s]
Downloaded: 5723 file(s) [attempted 5723/7954 = 71%, 305 KB/s]
Downloaded: 5764 file(s) [attempted 5764/7954 = 72%, 118 KB/s]
Downloaded: 5806 file(s) [attempted 5806/7954 = 72%, 91 KB/s]
Downloaded: 5847 file(s) [attempted 5847/7954 = 73%, 58 KB/s]
Downloaded: 5884 file(s) [attempted 5884/7954 = 73%, 572 KB/s]
Downloaded: 5922 file(s) [attempted 5922/7954 = 74%, 91 KB/s]
Downloaded: 5963 file(s) [attempted 5963/7954 = 74%, 353 KB/s]
Downloaded: 6011 file(s) [attempted 6011/7954 = 75%, 137 KB/s]
Downloaded: 6059 file(s) [attempted 6059/7954 = 76%, 185 KB/s]
Downloaded: 6107 file(s) [attempted 6107/7954 = 76%, 185 KB/s]
Downloaded: 6151 file(s) [attempted 6151/7954 = 77%, 418 KB/s]
Downloaded: 6189 file(s) [attempted 6189/7954 = 77%, 152 KB/s]
Downloaded: 6226 file(s) [attempted 6226/7954 = 78%, 491 KB/s]
Downloaded: 6269 file(s) [attempted 6269/7954 = 78%, 154 KB/s]
Downloaded: 6312 file(s) [attempted 6312/7954 = 79%, 156 KB/s]
Downloaded: 6353 file(s) [attempted 6353/7954 = 79%, 676 KB/s]
Downloaded: 6394 file(s) [attempted 6394/7954 = 80%, 86 KB/s]
Downloaded: 6432 file(s) [attempted 6432/7954 = 80%, 363 KB/s]
Downloaded: 6473 file(s) [attempted 6473/7954 = 81%, 374 KB/s]
Downloaded: 6511 file(s) [attempted 6511/7954 = 81%, 205 KB/s]
Downloaded: 6548 file(s) [attempted 6548/7954 = 82%, 645 KB/s]
Downloaded: 6586 file(s) [attempted 6586/7954 = 82%, 178 KB/s]
Downloaded: 6623 file(s) [attempted 6623/7954 = 83%, 38 KB/s]
Downloaded: 6661 file(s) [attempted 6661/7954 = 83%, 133 KB/s]
Downloaded: 6702 file(s) [attempted 6702/7954 = 84%, 381 KB/s]
Downloaded: 6747 file(s) [attempted 6747/7954 = 84%, 519 KB/s]
Downloaded: 6788 file(s) [attempted 6788/7954 = 85%, 77 KB/s]
Downloaded: 6825 file(s) [attempted 6825/7954 = 85%, 306 KB/s]
Downloaded: 6863 file(s) [attempted 6863/7954 = 86%, 92 KB/s]
Downloaded: 6904 file(s) [attempted 6904/7954 = 86%, 223 KB/s]
Downloaded: 6949 file(s) [attempted 6949/7954 = 87%, 276 KB/s]
Downloaded: 6990 file(s) [attempted 6990/7954 = 87%, 87 KB/s]
Downloaded: 7034 file(s) [attempted 7034/7954 = 88%, 515 KB/s]
Downloaded: 7075 file(s) [attempted 7075/7954 = 88%, 418 KB/s]
Downloaded: 7109 file(s) [attempted 7109/7954 = 89%, 70 KB/s]
Downloaded: 7150 file(s) [attempted 7150/7954 = 89%, 65 KB/s]
Downloaded: 7192 file(s) [attempted 7192/7954 = 90%, 450 KB/s]
Downloaded: 7239 file(s) [attempted 7239/7954 = 91%, 132 KB/s]
Downloaded: 7287 file(s) [attempted 7287/7954 = 91%, 208 KB/s]
Downloaded: 7325 file(s) [attempted 7325/7954 = 92%, 199 KB/s]
Downloaded: 7366 file(s) [attempted 7366/7954 = 92%, 331 KB/s]
Downloaded: 7411 file(s) [attempted 7411/7954 = 93%, 447 KB/s]
Downloaded: 7455 file(s) [attempted 7455/7954 = 93%, 102 KB/s]
Downloaded: 7499 file(s) [attempted 7499/7954 = 94%, 233 KB/s]
Downloaded: 7537 file(s) [attempted 7537/7954 = 94%, 161 KB/s]
Downloaded: 7575 file(s) [attempted 7575/7954 = 95%, 286 KB/s]
Downloaded: 7616 file(s) [attempted 7616/7954 = 95%, 76 KB/s]
Downloaded: 7660 file(s) [attempted 7660/7954 = 96%, 201 KB/s]
Downloaded: 7705 file(s) [attempted 7705/7954 = 96%, 56 KB/s]
Downloaded: 7746 file(s) [attempted 7746/7954 = 97%, 256 KB/s]
Downloaded: 7780 file(s) [attempted 7780/7954 = 97%, 526 KB/s]
Downloaded: 7821 file(s) [attempted 7821/7954 = 98%, 281 KB/s]
Downloaded: 7862 file(s) [attempted 7862/7954 = 98%, 229 KB/s]
Downloaded: 7903 file(s) [attempted 7903/7954 = 99%, 263 KB/s]
Downloaded: 7944 file(s) [attempted 7944/7954 = 99%, 150 KB/s]
Downloaded: 7954 file(s) [attempted 7954/7954 = 100%, 150 KB/s]
lean_checker exit 0
lake build
✔ [1886/1916] Built PFR.ForMathlib.Pair (4.3s) ✔ [2393/2527] Built PFR.Mathlib.MeasureTheory.Constructions.Pi (5.2s) ✔ [2594/2622] Built PFR.Mathlib.LinearAlgebra.Basis.VectorSpace (6.7s) ✔ [2595/2623] Built PFR.Mathlib.Probability.Independence.Kernel.IndepFun (7.0s) ✔ [2599/2623] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic (2.1s) ✔ [2659/2683] Built PFR.ForMathlib.FiniteRange.Defs (3.1s) ✔ [2660/2683] Built PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable (2.1s) ✔ [2661/2683] Built PFR.Mathlib.MeasureTheory.Measure.Dirac (1.0s) ✔ [2664/2683] Built PFR.Mathlib.Data.Set.Basic (1.2s) ✔ [2666/2683] Built PFR.Mathlib.Data.Set.Insert (1.3s) ✔ [2668/2683] Built PFR.Mathlib.MeasureTheory.Measure.Prod (2.5s) ✔ [2669/2683] Built PFR.Mathlib.Probability.Independence.Basic (4.1s) ✔ [2671/2683] Built PFR.ForMathlib.FiniteRange.ConditionalProbability (2.3s) ✔ [2673/2683] Built PFR.Mathlib.Data.Set.Card (1.4s) ✔ [2676/2689] Built PFR.Mathlib.MeasureTheory.Measure.Real (1.0s) ✔ [2677/2706] Built PFR.ForMathlib.ThreeVariables (2.5s) ✔ [2696/2783] Built PFR.Mathlib.Probability.UniformOn (2.3s) ✔ [2764/2783] Built PFR.Mathlib.MeasureTheory.Integral.Bochner.Set (2.9s) ✔ [2765/2783] Built PFR.Mathlib.Probability.IdentDistrib (7.8s) ✔ [2773/2792] Built PFR.Mathlib.Probability.ConditionalProbability (2.3s) ✔ [2779/2792] Built PFR.ForMathlib.Uniform (8.1s) ✔ [2780/2793] Built PFR.Mathlib.Probability.Kernel.Disintegration (10s) ✔ [2783/2806] Built PFR.ForMathlib.ConditionalIndependence (5.9s) ✔ [2789/2814] Built PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog (5.2s) ✔ [2799/2816] Built PFR.Mathlib.Probability.Kernel.Composition.Comp (4.2s) ✔ [2815/2837] Built PFR.ForMathlib.FiniteRange.IdentDistrib (4.5s) ✔ [2821/2858] Built PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure (4.5s) ✔ [2841/2867] Built APAP.Prereqs.Function.Indicator.Defs (3.8s) ✔ [2842/2867] Built PFR.ForMathlib.Entropy.Measure (11s) ✔ [2843/2868] Built PFR.ForMathlib.FourVariables (6.5s) ✔ [2845/2870] Built PFR.Tactic.RPowSimp (5.8s) ✔ [2846/2889] Built APAP.Prereqs.Function.Indicator.Basic (1.7s) ✔ [2850/2889] Built APAP.Prereqs.DummyPositivity (1.3s) ✔ [2851/2889] Built PFR.Mathlib.Data.Fin.Basic (1.4s) ✔ [2852/2889] Built PFR.Mathlib.Algebra.BigOperators.Fin (1.8s) ✔ [2853/2890] Built PFR.Mathlib.MeasureTheory.Group.Arithmetic (3.1s) ✔ [2854/2890] Built PFR.Mathlib.Order.Interval.Finset.Fin (2.2s) ✔ [2856/2890] Built PFR.ForMathlib.Entropy.Kernel.Basic (6.5s) ✔ [2857/2890] Built PFR.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (1.6s) ✔ [2859/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.Finrank (1.9s) ✔ [2861/2901] Built APAP.Prereqs.Convolution.Discrete.Defs (9.1s) ✔ [2862/2901] Built PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (1.9s) ✔ [2865/2901] Built PFR.Mathlib.LinearAlgebra.Quotient.Basic (1.6s) ✔ [2866/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpace (285ms) ✔ [2867/2901] Built PFR.ForMathlib.AffineSpaceDim (1.0s) ✔ [2868/2901] Built PFR.Mathlib.MeasureTheory.MeasurableSpace.Basic (1.5s) ✔ [2869/2901] Built PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef (1.0s) ✔ [2870/2901] Built PFR.ForMathlib.Entropy.Kernel.MutualInfo (4.6s) ✔ [2871/2901] Built PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability (2.2s) ✔ [2872/2901] Built APAP.Prereqs.Convolution.Order (3.7s) ✔ [2873/2901] Built APAP.Prereqs.Convolution.Discrete.Basic (5.0s) ✔ [2874/2901] Built PFR.ForMathlib.Entropy.Kernel.Group (3.9s) ✔ [2875/2901] Built PFR.ForMathlib.Entropy.Kernel.RuzsaDist (6.8s) ✔ [2876/2901] Built PFR.ForMathlib.Entropy.Basic (10s) ✔ [2877/2901] Built PFR.ForMathlib.Entropy.Group (4.7s) ✔ [2878/2901] Built PFR.Kullback (6.1s) ✔ [2879/2901] Built APAP.Extras.BSG (16s) ✔ [2880/2901] Built PFR.ForMathlib.Entropy.RuzsaDist (10s) ✔ [2881/2901] Built PFR.Fibring (4.4s) ✔ [2882/2901] Built PFR.ForMathlib.Entropy.RuzsaSetDist (4.5s) ✔ [2883/2901] Built PFR.HundredPercent (4.7s) ✔ [2884/2901] Built PFR.TauFunctional (5.1s) ✔ [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.8s) ✔ [2889/2901] Built PFR.Main (6.7s) ✔ [2890/2901] Built PFR.MoreRuzsaDist (49s) ✔ [2891/2901] Built PFR.MultiTauFunctional (4.2s) ✔ [2892/2901] Built PFR.ImprovedPFR (30s) ✔ [2893/2901] Built PFR.RhoFunctional (38s) ✔ [2894/2901] Built PFR.BoundingMutual (28s) ✔ [2895/2901] Built PFR.HomPFR (8.1s) ✔ [2896/2901] Built PFR.WeakPFR (22s) ✔ [2897/2901] Built PFR.ApproxHomPFR (15s) ✔ [2898/2901] Built PFR.TorsionEndgame (28s) ✔ [2899/2901] Built PFR.Examples (9.4s) ✔ [2900/2901] Built PFR (2.2s) Build completed successfully (2901 jobs).
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh