coqbot-app[bot]
commented
2 weeks ago :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-neural-net-interp-computed-lite │ 301.05 309.71 -2.80 │ 1373591539739 1412751669576 -2.77 │ 3617766367642 3617716098469 0.00 │ 1113276 1113144 0.01 │
│ coq-stdlib │ 350.24 356.80 -1.84 │ 1472085070071 1494553106724 -1.50 │ 1257671625353 1258446638077 -0.06 │ 717912 715760 0.30 │
│ coq-equations │ 7.53 7.66 -1.70 │ 31012889458 31229660802 -0.69 │ 50922725539 50923406667 -0.00 │ 388244 388200 0.01 │
│ coq-verdi │ 48.39 48.97 -1.18 │ 216543893091 219203332339 -1.21 │ 336938158414 340876096350 -1.16 │ 529988 531420 -0.27 │
│ coq-compcert │ 279.54 282.13 -0.92 │ 1257477248335 1266214738617 -0.69 │ 1936830779553 1945638104407 -0.45 │ 1124484 1125020 -0.05 │
│ coq-metacoq-translations │ 16.90 17.05 -0.88 │ 74934086021 75162770948 -0.30 │ 125128202860 125140120081 -0.01 │ 846648 846412 0.03 │
│ coq-bignums │ 29.46 29.72 -0.87 │ 132732174529 133945045947 -0.91 │ 192283081367 192277203345 0.00 │ 478160 480060 -0.40 │
│ coq-coqutil │ 42.34 42.70 -0.84 │ 186107572187 187380488627 -0.68 │ 270881697619 270878393689 0.00 │ 561540 561068 0.08 │
│ coq-fiat-core │ 59.73 60.16 -0.71 │ 245607033947 248174800235 -1.03 │ 368650810229 368712632496 -0.02 │ 484152 482572 0.33 │
│ coq-performance-tests-lite │ 708.84 713.33 -0.63 │ 3173377657486 3195609761361 -0.70 │ 5685385981487 5684605298781 0.01 │ 2274712 2276544 -0.08 │
│ coq-metacoq-template │ 150.93 151.84 -0.60 │ 664145516851 666752260604 -0.39 │ 1044889058236 1046873871436 -0.19 │ 1511736 1511484 0.02 │
│ coq-math-classes │ 85.57 86.03 -0.53 │ 383496648333 384763424270 -0.33 │ 536939684610 536918473645 0.00 │ 503784 504188 -0.08 │
│ coq-metacoq-erasure │ 500.21 502.87 -0.53 │ 2266201184299 2277743082374 -0.51 │ 3542002560274 3581854908133 -1.11 │ 2109840 2100720 0.43 │
│ coq-coqprime │ 47.97 48.21 -0.50 │ 215124495751 216013100235 -0.41 │ 334478688107 334473600731 0.00 │ 784016 783916 0.01 │
│ coq-mathcomp-fingroup │ 30.52 30.67 -0.49 │ 138676139945 138737818619 -0.04 │ 207759108073 207735186155 0.01 │ 567328 570476 -0.55 │
│ coq-core │ 129.61 130.17 -0.43 │ 502516947322 501598151548 0.18 │ 531967836516 531915033985 0.01 │ 457416 458008 -0.13 │
│ coq-verdi-raft │ 578.35 580.81 -0.42 │ 2623583882343 2634811477740 -0.43 │ 4144185055595 4161481339271 -0.42 │ 848120 848100 0.00 │
│ coq-metacoq-pcuic │ 982.72 986.79 -0.41 │ 4384377198717 4402689473714 -0.42 │ 6432890672149 6470106807740 -0.58 │ 2681456 2678484 0.11 │
│ coq-metacoq-safechecker │ 420.21 421.41 -0.28 │ 1916161925175 1921652758307 -0.29 │ 3173149209200 3184137397852 -0.35 │ 2074760 2082244 -0.36 │
│ coq-hott │ 161.53 161.92 -0.24 │ 715084167144 717240235239 -0.30 │ 1146842024467 1146875113486 -0.00 │ 473548 472296 0.27 │
│ coq-fourcolor │ 1366.95 1369.12 -0.16 │ 6218299877516 6227545818004 -0.15 │ 12909620405611 12909405781018 0.00 │ 2139424 2137700 0.08 │
│ coq-rewriter │ 390.87 391.47 -0.15 │ 1762659581112 1766841858907 -0.24 │ 2990160562499 2990591611289 -0.01 │ 1475604 1477716 -0.14 │
│ coq-corn │ 715.63 715.22 0.06 │ 3235261565077 3236085376464 -0.03 │ 5077730508124 5077906733572 -0.00 │ 755220 755368 -0.02 │
│ coq-color │ 252.16 251.93 0.09 │ 1125521069682 1125658645114 -0.01 │ 1636191424226 1635946573068 0.01 │ 1221044 1175548 3.87 │
│ coq-vst │ 880.83 879.72 0.13 │ 3982525040238 3973883433977 0.22 │ 6735205893828 6743929549107 -0.13 │ 2117708 2165964 -2.23 │
│ coq-fiat-parsers │ 312.73 312.31 0.13 │ 1383564324562 1385073795756 -0.11 │ 2470976335896 2471332388171 -0.01 │ 2411180 2409032 0.09 │
│ coq-rewriter-perf-SuperFast │ 797.14 796.04 0.14 │ 3564674838922 3558614844505 0.17 │ 6256044501520 6257746218429 -0.03 │ 1577976 1574920 0.19 │
│ coq-fiat-crypto-with-bedrock │ 6250.14 6240.34 0.16 │ 28320503734144 28269432760970 0.18 │ 51207437519327 51229215012431 -0.04 │ 3245976 3245960 0.00 │
│ coq-iris-examples │ 468.66 466.75 0.41 │ 2121453091321 2111903006252 0.45 │ 3276255982613 3276826445280 -0.02 │ 1111020 1115132 -0.37 │
│ coq-category-theory │ 695.59 692.71 0.42 │ 3150851990835 3137564242010 0.42 │ 5263745951058 5263397039802 0.01 │ 960924 957040 0.41 │
│ coq-mathcomp-solvable │ 118.35 117.78 0.48 │ 539399687209 536441965202 0.55 │ 857083542735 857050008388 0.00 │ 878044 879800 -0.20 │
│ coq-mathcomp-character │ 109.81 109.23 0.53 │ 499517932423 496358018231 0.64 │ 790439576929 790457762136 -0.00 │ 1136764 1139008 -0.20 │
│ coq-unimath │ 2473.63 2456.13 0.71 │ 11217056780500 11134090421244 0.75 │ 22210747776595 22210993419165 -0.00 │ 1254512 1254220 0.02 │
│ coq-bedrock2 │ 364.02 361.32 0.75 │ 1647232790147 1631644728772 0.96 │ 3109684018956 3110439186767 -0.02 │ 856200 858756 -0.30 │
│ coq-mathcomp-ssreflect │ 222.11 220.20 0.87 │ 1002906067718 992345902700 1.06 │ 1675922880750 1676025094517 -0.01 │ 1718728 1718692 0.00 │
│ coq-mathcomp-algebra │ 262.87 260.38 0.96 │ 1188546109984 1177583940393 0.93 │ 2000640690491 2000595746511 0.00 │ 1332548 1335272 -0.20 │
│ coq-engine-bench-lite │ 157.85 156.25 1.02 │ 662131235616 654964885509 1.09 │ 1225355819272 1222405576122 0.24 │ 1322936 1324196 -0.10 │
│ coq-mathcomp-field │ 143.95 142.36 1.12 │ 649953740420 642681384406 1.13 │ 1074386779623 1074458107141 -0.01 │ 1484852 1483440 0.10 │
│ coq-coquelicot │ 40.01 39.56 1.14 │ 176695738079 175307055715 0.79 │ 249078969633 249057452059 0.01 │ 853180 855404 -0.26 │
│ coq-mathcomp-odd-order │ 795.67 775.70 2.57 │ 3633552726641 3542090632461 2.58 │ 6078463623317 6078601690574 -0.00 │ 1652700 1655048 -0.14 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
INFO: failed to install coq-test-suite
:turtle: Top 25 slow downs
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 76.2720 83.1870 6.9150 9.07% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 63.4730 69.2710 5.7980 9.13% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 61.5110 63.9040 2.3930 3.89% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 96.0030 97.8430 1.8400 1.92% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 72.4470 73.5800 1.1330 1.56% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 62.8100 63.8150 1.0050 1.60% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 46.3810 47.2850 0.9040 1.95% 926 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 153.7700 154.6350 0.8650 0.56% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 48.2060 49.0200 0.8140 1.69% 558 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 81.1950 82.0050 0.8100 1.00% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 27.3770 28.1640 0.7870 2.87% 147 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 16.7610 17.5200 0.7590 4.53% 607 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 38.3750 39.1020 0.7270 1.89% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 181.1440 181.8520 0.7080 0.39% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 29.0210 29.6510 0.6300 2.17% 144 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 24.6340 25.1940 0.5600 2.27% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 36.6070 37.1500 0.5430 1.48% 548 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 21.4270 21.9520 0.5250 2.45% 376 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html │ │ 26.7850 27.2960 0.5110 1.91% 453 coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html │ │ 24.0940 24.5930 0.4990 2.07% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 33.4600 33.9340 0.4740 1.42% 1333 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 24.6440 25.1020 0.4580 1.86% 375 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 19.6440 20.0650 0.4210 2.14% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.5580 0.9520 0.3940 70.61% 813 coq-stdlib/MSets/MSetRBT.v.html │ │ 25.2670 25.6590 0.3920 1.55% 242 coq-unimath/UniMath/ModelCategories/Examples.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
:rabbit2: Top 25 speed ups
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 267.8600 259.6500 -8.2100 -3.07% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 4.6700 2.1100 -2.5600 -54.82% 320 coq-metacoq-erasure/erasure/theories/ErasureProperties.v.html │ │ 219.4860 217.7660 -1.7200 -0.78% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 3.8900 2.6750 -1.2150 -31.23% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 24.5600 23.3960 -1.1640 -4.74% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 96.1270 95.1350 -0.9920 -1.03% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 96.0040 95.2650 -0.7390 -0.77% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 12.5220 11.8080 -0.7140 -5.70% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 2.3260 1.6310 -0.6950 -29.88% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 32.4850 31.9660 -0.5190 -1.60% 12 coq-fourcolor/theories/job439to465.v.html │ │ 27.5170 27.0230 -0.4940 -1.80% 35 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 4.4070 3.9150 -0.4920 -11.16% 3746 coq-metacoq-pcuic/pcuic/theories/PCUICExpandLetsCorrectness.v.html │ │ 29.3380 28.8680 -0.4700 -1.60% 32 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 4.7740 4.3050 -0.4690 -9.82% 537 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatImp.v.html │ │ 21.1420 20.7340 -0.4080 -1.93% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 256.9340 256.5280 -0.4060 -0.16% 1629 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 3.0310 2.6760 -0.3550 -11.71% 2408 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 2.5700 2.2190 -0.3510 -13.66% 572 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatImp.v.html │ │ 3.0710 2.7210 -0.3500 -11.40% 2097 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 26.2280 25.8910 -0.3370 -1.28% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 0.8930 0.5690 -0.3240 -36.28% 160 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 28.7810 28.4570 -0.3240 -1.13% 12 coq-fourcolor/theories/job589to610.v.html │ │ 25.8700 25.5680 -0.3020 -1.17% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 0.5880 0.2960 -0.2920 -49.66% 1364 coq-stdlib/FSets/FMapAVL.v.html │ │ 4.5990 4.3090 -0.2900 -6.31% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
SkySkimmer
ppedrot
@coqbot bench