coq
coq copied to clipboard
coq
Attempt to avoid exporting mono univs from Qed proofs
and warn when we must export a constraint between non private univs
Full warning output from compiling stdlib: https://gist.github.com/SkySkimmer/4bd60e230bb3b3d1f6a6f92bd13ed94f
Code is a bit bugged (especially Derive and Next Obligation don't like close_proof with keep_body_ucst_separate AFAICT, but without it the higher layers merge the body and type univ declarations) but gives an idea of what happens.
Overlays:
- https://github.com/LPCIC/coq-elpi/pull/625
It seems like a non-negligible number of opaque universe constraints comes from the use of rewrite. Perhaps forcing the universe of eq_ind_r to be identical to the one of eq would improve things. Indeed, the failing lemmas presumably have equalities as hypotheses, so the corresponding constraint is already public and no private constraint would be needed anymore.
Perhaps forcing the universe of eq_ind_r to be identical to the one of eq would improve things
See new commit and revision 2 of https://gist.github.com/SkySkimmer/4bd60e230bb3b3d1f6a6f92bd13ed94f tldr about -300 lines (warning location and message take a line each per Qed so probably more like -100 constraints) (diff isn't only deletions because of building with parallel jobs)
No check suite 31373 for head commit coq/coq@fc35769049b0fc54fa921efe331f58eed5a5c544.
![coqbot-app[bot] avatar](https://avatars.githubusercontent.com/in/31373?v=4 "Published by a pub.dev verified publisher"){kind=small}
:checkered_flag: Bench results:
┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │
│ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-category-theory │ 676.23 682.95 -0.98 │ 3080265382112 3109375072385 -0.94 │ 5133440722293 5232596154677 -1.89 │ 972256 958960 1.39 │
│ coq-core │ 128.45 129.31 -0.67 │ 505124860691 501603325606 0.70 │ 531492270161 531442120764 0.01 │ 458020 457680 0.07 │
│ coq-bedrock2 │ 357.66 359.88 -0.62 │ 1629792635199 1642001418490 -0.74 │ 3092606724098 3091507932830 0.04 │ 857916 859500 -0.18 │
│ coq-vst │ 871.82 876.62 -0.55 │ 3970400562139 3989576318894 -0.48 │ 6708176675125 6727884031522 -0.29 │ 2182344 2185548 -0.15 │
│ coq-iris-examples │ 464.61 464.72 -0.02 │ 2112463322621 2113713676150 -0.06 │ 3260473711126 3260322194588 0.00 │ 1115952 1118156 -0.20 │
│ coq │ 0.11 0.11 0.00 │ 409668220 404524229 1.27 │ 705269045 701368499 0.56 │ 86272 87660 -1.58 │
│ coq-verdi-raft │ 576.81 576.72 0.02 │ 2626597607732 2626878194888 -0.01 │ 4149884524535 4150133968553 -0.01 │ 848112 847520 0.07 │
│ coq-compcert │ 280.78 280.66 0.04 │ 1270502405997 1269660308715 0.07 │ 1934136648091 1936323048609 -0.11 │ 1166048 1113408 4.73 │
│ coq-fiat-parsers │ 308.35 308.18 0.06 │ 1378261539144 1375485847722 0.20 │ 2414394087195 2417751406140 -0.14 │ 2381456 2393852 -0.52 │
│ coq-stdlib │ 363.10 362.07 0.28 │ 1540707082973 1538238133560 0.16 │ 1281324620816 1286664187320 -0.41 │ 715656 719768 -0.57 │
│ coq-engine-bench-lite │ 156.27 155.82 0.29 │ 662696824971 661993034704 0.11 │ 1225241330156 1224052711973 0.10 │ 1299212 1301504 -0.18 │
│ coq-unimath │ 2422.14 2413.42 0.36 │ 11042798822770 11003215440520 0.36 │ 21905631961638 21885925011157 0.09 │ 1246800 1274604 -2.18 │
│ coq-verdi │ 48.49 48.31 0.37 │ 218468488771 218056529553 0.19 │ 336380829081 336564430066 -0.05 │ 535148 532092 0.57 │
│ coq-hott │ 165.87 165.23 0.39 │ 742474384325 738472595047 0.54 │ 1179599255258 1179684037863 -0.01 │ 658772 657288 0.23 │
│ coq-coqprime │ 47.82 47.63 0.40 │ 214646027591 214422785746 0.10 │ 329829119469 330023604479 -0.06 │ 783000 783412 -0.05 │
│ coq-bignums │ 29.42 29.27 0.51 │ 133683545837 132690162428 0.75 │ 191894515115 192046260893 -0.08 │ 472540 473984 -0.30 │
│ coq-math-classes │ 85.15 84.68 0.56 │ 382365317337 381344629637 0.27 │ 533365562818 533064875893 0.06 │ 502940 503764 -0.16 │
│ coq-neural-net-interp-computed-lite │ 292.00 290.36 0.56 │ 1333706782590 1326035908112 0.58 │ 3420692378972 3420856776622 -0.00 │ 1114472 1126388 -1.06 │
│ coq-corn │ 715.82 711.10 0.66 │ 3252078034916 3233187908555 0.58 │ 5038311027136 5062066622179 -0.47 │ 795892 762780 4.34 │
│ coq-coqutil │ 41.82 41.53 0.70 │ 185983922794 184199103909 0.97 │ 265979487362 266051881942 -0.03 │ 560756 561032 -0.05 │
│ coq-color │ 250.72 248.31 0.97 │ 1127674188678 1118731653984 0.80 │ 1622398006246 1624229854626 -0.11 │ 1214188 1207032 0.59 │
│ coq-equations │ 7.51 7.40 1.49 │ 30541062321 30392436603 0.49 │ 49554435902 49607362120 -0.11 │ 387116 386388 0.19 │
│ coq-fiat-core │ 58.37 57.37 1.74 │ 243409255752 241083224616 0.96 │ 357942677560 358890863624 -0.26 │ 482904 483116 -0.04 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
INFO: failed to install coq-performance-tests-lite coq-mathcomp-ssreflect (dependency install failed in NEW) coq-metacoq-template (dependency install failed in NEW) coq-metacoq-pcuic (dependency install failed in NEW) coq-rewriter
coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed) coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed) coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed) coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed) coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed) coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed) coq-metacoq-safechecker (dependency coq-metacoq-pcuic failed) coq-metacoq-erasure (dependency coq-metacoq-template failed) coq-metacoq-translations (dependency coq-metacoq-template failed) coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed) coq-coquelicot (dependency coq-mathcomp-ssreflect failed) coq-fourcolor (dependency coq-mathcomp-ssreflect failed) coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
:turtle: Top 25 slow downs
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 249.2770 250.9860 1.7090 0.69% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 18.4440 19.3740 0.9300 5.04% 957 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html │ │ 40.9080 41.6400 0.7320 1.79% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 7.7850 8.4340 0.6490 8.34% 1225 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html │ │ 9.0250 9.5580 0.5330 5.91% 952 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html │ │ 7.2330 7.7560 0.5230 7.23% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.3890 7.8960 0.5070 6.86% 488 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.v.html │ │ 6.9980 7.4450 0.4470 6.39% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 72.7840 73.2040 0.4200 0.58% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 0.9860 1.3610 0.3750 38.03% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 12.1540 12.5120 0.3580 2.95% 409 coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html │ │ 10.3710 10.6930 0.3220 3.10% 985 coq-vst/floyd/closed_lemmas.v.html │ │ 1.4680 1.7810 0.3130 21.32% 557 coq-vst/veric/expr_lemmas3.v.html │ │ 9.6770 9.9660 0.2890 2.99% 418 coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html │ │ 3.9170 4.1990 0.2820 7.20% 240 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 44.0000 44.2470 0.2470 0.56% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 4.0910 4.3260 0.2350 5.74% 278 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html │ │ 0.4610 0.6750 0.2140 46.42% 2108 coq-stdlib/FSets/FMapFacts.v.html │ │ 25.4190 25.6330 0.2140 0.84% 242 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 7.5540 7.7670 0.2130 2.82% 250 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.v.html │ │ 24.9690 25.1690 0.2000 0.80% 458 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 1.6920 1.8760 0.1840 10.87% 765 coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html │ │ 2.7130 2.8930 0.1800 6.63% 218 coq-corn/transc/ArTanH.v.html │ │ 2.7360 2.9080 0.1720 6.29% 450 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Fiberwise/DependentProducts.v.html │ │ 3.3780 3.5490 0.1710 5.06% 2265 coq-unimath/UniMath/PAdics/padics.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
:rabbit2: Top 25 speed ups
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 65.0600 62.3220 -2.7380 -4.21% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 9.4290 8.6940 -0.7350 -7.80% 447 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html │ │ 47.5320 46.8580 -0.6740 -1.42% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 30.5250 29.9260 -0.5990 -1.96% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 2.2120 1.6970 -0.5150 -23.28% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 31.3730 30.8770 -0.4960 -1.58% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 8.0430 7.5680 -0.4750 -5.91% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 33.6130 33.1630 -0.4500 -1.34% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 4.7570 4.3510 -0.4060 -8.53% 733 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 97.5560 97.1740 -0.3820 -0.39% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 2.1200 1.7460 -0.3740 -17.64% 860 coq-category-theory/Functor/Construction/Product/Monoidal.v.html │ │ 3.6730 3.3620 -0.3110 -8.47% 1060 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/FunctorCategory.v.html │ │ 4.9250 4.6500 -0.2750 -5.58% 318 coq-unimath/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.v.html │ │ 2.1340 1.8730 -0.2610 -12.23% 1088 coq-category-theory/Functor/Construction/Product/Monoidal.v.html │ │ 7.4650 7.2080 -0.2570 -3.44% 1217 coq-vst/floyd/Component.v.html │ │ 11.4110 11.1570 -0.2540 -2.23% 126 coq-vst/veric/binop_lemmas6.v.html │ │ 17.5340 17.2960 -0.2380 -1.36% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 6.4320 6.1990 -0.2330 -3.62% 587 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.v.html │ │ 0.6740 0.4580 -0.2160 -32.05% 82 coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html │ │ 13.2050 12.9950 -0.2100 -1.59% 1028 coq-unimath/UniMath/CategoryTheory/LocalizingClass.v.html │ │ 23.0950 22.9010 -0.1940 -0.84% 595 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 0.3410 0.1480 -0.1930 -56.60% 1603 coq-stdlib/micromega/Tauto.v.html │ │ 3.1760 2.9860 -0.1900 -5.98% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.3180 0.1330 -0.1850 -58.18% 11 coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html │ │ 2.9120 2.7330 -0.1790 -6.15% 637 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/Presheaves.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
:checkered_flag: Bench results:
┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │
│ │ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-verdi │ 48.08 49.03 -1.94 │ 217070964605 220325361403 -1.48 │ 336818264206 336993161730 -0.05 │ 530268 531984 -0.32 │
│ coq-mathcomp-odd-order │ 780.18 792.41 -1.54 │ 3572194521731 3629203889222 -1.57 │ 6063763341196 6095252668356 -0.52 │ 1650604 1640804 0.60 │
│ coq-category-theory │ 678.48 687.00 -1.24 │ 3091099888756 3128200185051 -1.19 │ 5142065696297 5237136119681 -1.82 │ 972092 958836 1.38 │
│ coq-neural-net-interp-computed-lite │ 298.68 302.36 -1.22 │ 1365063696178 1381501805728 -1.19 │ 3611817575590 3611979556926 -0.00 │ 1124140 1126456 -0.21 │
│ coq-fiat-parsers │ 307.95 310.93 -0.96 │ 1375266907814 1389246332748 -1.01 │ 2452647933785 2455557997788 -0.12 │ 2381528 2395820 -0.60 │
│ coq-math-classes │ 85.07 85.67 -0.70 │ 383333220889 385560042205 -0.58 │ 534289983606 534015024593 0.05 │ 502288 503272 -0.20 │
│ coq-bignums │ 29.39 29.57 -0.61 │ 133197855333 133983913661 -0.59 │ 191904661978 192064811134 -0.08 │ 472692 472256 0.09 │
│ coq-mathcomp-solvable │ 118.39 119.07 -0.57 │ 540442153778 543676288077 -0.59 │ 858478734973 859031418473 -0.06 │ 885200 879680 0.63 │
│ coq-fiat-core │ 58.12 58.44 -0.55 │ 242292644341 244886536186 -1.06 │ 359441186847 360378013038 -0.26 │ 482176 483100 -0.19 │
│ coq-verdi-raft │ 577.70 580.55 -0.49 │ 2630828488305 2643479242347 -0.48 │ 4143455969635 4142645023611 0.02 │ 846096 846232 -0.02 │
│ coq-coqutil │ 41.86 42.06 -0.48 │ 185031422767 185618719035 -0.32 │ 267001906934 267071893540 -0.03 │ 561668 561244 0.08 │
│ coq-coquelicot │ 38.84 39.01 -0.44 │ 173472831835 174043362464 -0.33 │ 244152762010 244356908437 -0.08 │ 851952 851888 0.01 │
│ coq-hott │ 160.98 161.56 -0.36 │ 720071709391 721694947262 -0.22 │ 1147806226889 1147706946742 0.01 │ 576060 575752 0.05 │
│ coq-vst │ 873.55 876.60 -0.35 │ 3975652333818 3990521715459 -0.37 │ 6711724069705 6731131777037 -0.29 │ 2183956 2183356 0.03 │
│ coq-corn │ 708.85 711.17 -0.33 │ 3220933942709 3232723067943 -0.36 │ 5042038959630 5065514926155 -0.46 │ 796272 764068 4.21 │
│ coq-compcert │ 281.49 282.12 -0.22 │ 1273420677023 1275224630855 -0.14 │ 1943712821788 1945505611957 -0.09 │ 1163112 1116076 4.21 │
│ coq-iris-examples │ 465.82 466.23 -0.09 │ 2118400383948 2120286487986 -0.09 │ 3262255394868 3262068826881 0.01 │ 1116668 1115652 0.09 │
│ coq-color │ 249.99 250.11 -0.05 │ 1125005750766 1127398134023 -0.21 │ 1624663094684 1626382559467 -0.11 │ 1215244 1205244 0.83 │
│ coq-coqprime │ 47.96 47.98 -0.04 │ 214478765331 215784136966 -0.60 │ 332013850574 332176446699 -0.05 │ 783716 783988 -0.03 │
│ coq-mathcomp-fingroup │ 30.39 30.36 0.10 │ 138303613135 138310730966 -0.01 │ 207515106135 207737039993 -0.11 │ 562796 562908 -0.02 │
│ coq-stdlib │ 360.78 360.31 0.13 │ 1528377462127 1531040093895 -0.17 │ 1281472456385 1286719306735 -0.41 │ 715628 717500 -0.26 │
│ coq-mathcomp-character │ 109.43 109.22 0.19 │ 500250935203 498463121561 0.36 │ 789436498243 792985540461 -0.45 │ 1147072 1153084 -0.52 │
│ coq-mathcomp-ssreflect │ 218.47 217.93 0.25 │ 997697341687 995338801086 0.24 │ 1666962596945 1673216969556 -0.37 │ 1720796 1739216 -1.06 │
│ coq-fourcolor │ 1363.86 1360.34 0.26 │ 6237253539878 6221474578804 0.25 │ 12914562857032 12910202270763 0.03 │ 2127828 2128760 -0.04 │
│ coq-engine-bench-lite │ 156.48 155.95 0.34 │ 663663301652 661119942661 0.38 │ 1221954426557 1225325367161 -0.28 │ 1298964 1298636 0.03 │
│ coq-unimath │ 2465.34 2451.67 0.56 │ 11235307127309 11174549162495 0.54 │ 22183742069208 22166280585948 0.08 │ 1245652 1273464 -2.18 │
│ coq-core │ 129.68 128.59 0.85 │ 501412704161 500175462355 0.25 │ 531643003980 531308179231 0.06 │ 457428 457148 0.06 │
│ coq-mathcomp-algebra │ 262.45 260.03 0.93 │ 1196613965641 1185702183109 0.92 │ 2003948469679 2003112054707 0.04 │ 1304752 1293404 0.88 │
│ coq-bedrock2 │ 360.50 357.08 0.96 │ 1642922112801 1627326510692 0.96 │ 3098307392277 3098009767301 0.01 │ 859172 857444 0.20 │
│ coq-equations │ 7.54 7.45 1.21 │ 30579120619 30824199818 -0.80 │ 49872624089 49942495675 -0.14 │ 391252 386520 1.22 │
│ coq-mathcomp-field │ 144.25 141.87 1.68 │ 658456717811 647685642133 1.66 │ 1078046915498 1076869153416 0.11 │ 1392024 1469288 -5.26 │
│ coq │ 0.12 0.11 9.09 │ 409207199 408965997 0.06 │ 705270809 704987937 0.04 │ 86464 88192 -1.96 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
INFO: failed to install coq-performance-tests-lite coq-metacoq-template (dependency install failed in NEW) coq-metacoq-pcuic (dependency install failed in NEW) coq-rewriter
coq-metacoq-safechecker (dependency coq-metacoq-pcuic failed) coq-metacoq-erasure (dependency coq-metacoq-template failed) coq-metacoq-translations (dependency coq-metacoq-template failed) coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed) coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
:turtle: Top 25 slow downs
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 14.2630 15.9780 1.7150 12.02% 1505 coq-vst/floyd/VSU.v.html │ │ 62.4750 64.0310 1.5560 2.49% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 18.6200 19.6130 0.9930 5.33% 957 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html │ │ 45.8260 46.5990 0.7730 1.69% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 16.6690 17.3700 0.7010 4.21% 607 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 16.9460 17.6340 0.6880 4.06% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 7.8630 8.4380 0.5750 7.31% 1225 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html │ │ 21.8490 22.3710 0.5220 2.39% 12 coq-fourcolor/theories/job303to306.v.html │ │ 33.7800 34.2950 0.5150 1.52% 839 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 96.1250 96.6000 0.4750 0.49% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 19.6680 20.0500 0.3820 1.94% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 4.8350 5.1970 0.3620 7.49% 1258 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 11.2770 11.6350 0.3580 3.17% 2103 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 22.9810 23.3360 0.3550 1.54% 12 coq-fourcolor/theories/job495to498.v.html │ │ 30.1060 30.4530 0.3470 1.15% 12 coq-fourcolor/theories/job254to270.v.html │ │ 4.1000 4.4160 0.3160 7.71% 278 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html │ │ 1.4690 1.7770 0.3080 20.97% 557 coq-vst/veric/expr_lemmas3.v.html │ │ 7.4580 7.7540 0.2960 3.97% 488 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.v.html │ │ 3.9490 4.2420 0.2930 7.42% 240 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 19.5990 19.8740 0.2750 1.40% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 9.5490 9.8010 0.2520 2.64% 952 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html │ │ 24.7160 24.9510 0.2350 0.95% 12 coq-fourcolor/theories/job499to502.v.html │ │ 24.3390 24.5720 0.2330 0.96% 12 coq-fourcolor/theories/job291to294.v.html │ │ 46.5470 46.7760 0.2290 0.49% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 17.9690 18.1970 0.2280 1.27% 12 coq-fourcolor/theories/job311to314.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
:rabbit2: Top 25 speed ups
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 83.4330 77.9980 -5.4350 -6.51% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 69.5300 64.4950 -5.0350 -7.24% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 261.3220 257.7190 -3.6030 -1.38% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 7.9830 7.0760 -0.9070 -11.36% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.5770 6.8220 -0.7550 -9.96% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 44.9240 44.1990 -0.7250 -1.61% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 42.1290 41.4480 -0.6810 -1.62% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 8.0880 7.4900 -0.5980 -7.39% 577 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 1.4230 0.9870 -0.4360 -30.64% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 18.0870 17.6510 -0.4360 -2.41% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 7.9370 7.5290 -0.4080 -5.14% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 4.1660 3.7760 -0.3900 -9.36% 66 coq-category-theory/Instance/Coq/Par.v.html │ │ 2.1240 1.8130 -0.3110 -14.64% 860 coq-category-theory/Functor/Construction/Product/Monoidal.v.html │ │ 2.1510 1.8400 -0.3110 -14.46% 1088 coq-category-theory/Functor/Construction/Product/Monoidal.v.html │ │ 73.4090 73.1000 -0.3090 -0.42% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 0.8360 0.5500 -0.2860 -34.21% 160 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 4.4750 4.1920 -0.2830 -6.32% 504 coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html │ │ 19.9830 19.7030 -0.2800 -1.40% 1286 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 4.9250 4.6500 -0.2750 -5.58% 318 coq-unimath/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.v.html │ │ 6.4940 6.2220 -0.2720 -4.19% 587 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.v.html │ │ 0.5450 0.3180 -0.2270 -41.65% 868 coq-stdlib/MSets/MSetRBT.v.html │ │ 32.1940 31.9710 -0.2230 -0.69% 12 coq-fourcolor/theories/job439to465.v.html │ │ 1.2450 1.0230 -0.2220 -17.83% 9 coq-mathcomp-odd-order/theories/stripped_odd_order_theorem.v.html │ │ 0.2140 0.0070 -0.2070 -96.73% 26 coq-mathcomp-odd-order/theories/PFsection14.v.html │ │ 0.2090 0.0050 -0.2040 -97.61% 28 coq-mathcomp-odd-order/theories/PFsection12.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
I thought it would have produced a slowdown (I don't trust the perf of constraints_for / restrict_universe_context) but apparently it's a bit faster if anything.
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.
Actually I was going to run this PR with my infra to report leaks, would be indeed great if we could repair this at some point
