Drop useless content from module parameter types. - #22402
Closed
ppedrot wants to merge 2 commits into
Closed
coqbot-app / bench
completed
Aug 27, 2026 in 0s
Bench completed with failures
GitLab Job URL:
Details
🏁 Bench Summary:
┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│ │ user time [s] │ CPU instructions │ max resident mem [KB] │
│ │ │ │ │
│ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ rocq-metarocq-utils │ 24.30 24.56 -1.06 │ 155107817622 156324817484 -0.78 │ 589636 596864 -1.21 │
│ rocq-bignums │ 25.36 25.59 -0.90 │ 159388704674 160513135607 -0.70 │ 461080 465112 -0.87 │
│ coq-coqutil │ 48.32 48.66 -0.70 │ 295559694622 297452577190 -0.64 │ 562628 568328 -1.00 │
│ rocq-mathcomp-group-representation │ 95.77 96.40 -0.65 │ 666156215989 666061824344 0.01 │ 1525172 1521968 0.21 │
│ coq-engine-bench-lite │ 126.31 127.03 -0.57 │ 935267471781 939490720544 -0.45 │ 1132440 1135868 -0.30 │
│ rocq-metarocq-common │ 41.53 41.76 -0.55 │ 265107952117 266077059978 -0.36 │ 907964 915980 -0.88 │
│ coq-color │ 229.88 231.15 -0.55 │ 1440330373189 1448269468148 -0.55 │ 1174880 1200400 -2.13 │
│ rocq-stdlib │ 239.82 241.05 -0.51 │ 1483206457520 1492334138226 -0.61 │ 759980 761832 -0.24 │
│ rocq-equations │ 7.93 7.97 -0.50 │ 55549450498 55662534766 -0.20 │ 400976 402504 -0.38 │
│ coq-fiat-core │ 56.46 56.74 -0.49 │ 338090785943 340867799937 -0.81 │ 482440 484744 -0.48 │
│ coq-coqprime │ 55.88 56.15 -0.48 │ 381669616441 382875687537 -0.32 │ 828396 831760 -0.40 │
│ coq-hott │ 160.04 160.75 -0.44 │ 1070085329686 1070079553780 0.00 │ 474552 475172 -0.13 │
│ coq-corn │ 644.50 647.32 -0.44 │ 4314213460003 4324519790447 -0.24 │ 623648 632900 -1.46 │
│ coq-iris-examples │ 370.57 371.69 -0.30 │ 2395211011080 2400104608399 -0.20 │ 1084468 1094384 -0.91 │
│ coq-category-theory │ 1353.45 1357.08 -0.27 │ 9826057468586 9842778215119 -0.17 │ 6744368 6748980 -0.07 │
│ rocq-mathcomp-algebra │ 366.05 366.93 -0.24 │ 2639438189766 2639372751633 0.00 │ 1572312 1568896 0.22 │
│ coq-rewriter-perf-SuperFast │ 463.26 464.33 -0.23 │ 3534640490319 3539822542210 -0.15 │ 1257528 1293144 -2.75 │
│ rocq-metarocq-erasure │ 438.96 439.92 -0.22 │ 2956137005973 2959951191630 -0.13 │ 1827008 1831708 -0.26 │
│ rocq-metarocq-safechecker │ 313.20 313.78 -0.18 │ 2307877508778 2308509687655 -0.03 │ 1723368 1728220 -0.28 │
│ rocq-mathcomp-solvable │ 98.20 98.38 -0.18 │ 660052055174 660090341064 -0.01 │ 1081344 1082960 -0.15 │
│ coq-performance-tests-lite │ 872.14 873.71 -0.18 │ 6955148122301 6966968431987 -0.17 │ 1625796 1559944 4.22 │
│ coq-compcert │ 306.98 307.49 -0.17 │ 1979147353445 1985022622940 -0.30 │ 1285296 1201060 7.01 │
│ coq-math-classes │ 82.44 82.57 -0.16 │ 494570458483 497310575722 -0.55 │ 513816 519520 -1.10 │
│ coq-rewriter │ 330.35 330.83 -0.15 │ 2431371087568 2435109067920 -0.15 │ 1407612 1498524 -6.07 │
│ coq-fiat-parsers │ 274.18 274.54 -0.13 │ 2077427497146 2086906251399 -0.45 │ 2263500 2258248 0.23 │
│ coq-unimath │ 1938.95 1940.49 -0.08 │ 15984168062338 15984077994728 0.00 │ 1799772 1801664 -0.11 │
│ coq-vst │ 812.16 812.70 -0.07 │ 6056954395066 6063672342595 -0.11 │ 2088800 2000492 4.41 │
│ coq-fiat-crypto-with-bedrock │ 8216.88 8222.05 -0.06 │ 68144630313187 68167620338813 -0.03 │ 3887236 4010288 -3.07 │
│ rocq-mathcomp-analysis │ 1379.27 1380.12 -0.06 │ 10383540778966 10383929502297 -0.00 │ 2196028 2195984 0.00 │
│ rocq-mathcomp-order │ 93.63 93.61 0.02 │ 668118806843 668142298644 -0.00 │ 920788 922856 -0.22 │
│ coq-fourcolor │ 1352.71 1351.89 0.06 │ 12416206233193 12428325909880 -0.10 │ 1013264 1030460 -1.67 │
│ rocq-runtime │ 77.14 76.99 0.19 │ 555785119065 555706858688 0.01 │ 495740 497980 -0.45 │
│ rocq-mathcomp-field │ 200.11 199.65 0.23 │ 1441742402056 1441615430454 0.01 │ 2228608 2228384 0.01 │
│ rocq-metarocq-template │ 81.64 81.44 0.25 │ 557441563027 556734335545 0.13 │ 1118708 1120572 -0.17 │
│ coq-mathcomp-odd-order │ 606.46 604.84 0.27 │ 4243029252068 4243289642407 -0.01 │ 2721140 2721476 -0.01 │
│ rocq-mathcomp-finite-group │ 26.88 26.80 0.30 │ 172859924464 172847468216 0.01 │ 574192 574040 0.03 │
│ rocq-metarocq-pcuic │ 606.19 603.89 0.38 │ 3866634755759 3845542938274 0.55 │ 2362428 1697516 39.17 │
│ coq-bedrock2 │ 334.26 332.96 0.39 │ 2678512236070 2684320305392 -0.22 │ 851472 874768 -2.66 │
│ rocq-mathcomp-boot │ 39.89 39.72 0.43 │ 234115649288 234097620988 0.01 │ 668004 666008 0.30 │
│ rocq-metarocq-translations │ 16.55 16.42 0.79 │ 115334263202 115162652480 0.15 │ 876772 889028 -1.38 │
│ coq-neural-net-interp-computed-lite │ 237.12 235.06 0.88 │ 2260268916173 2261191582865 -0.04 │ 877328 848536 3.39 │
│ rocq-core │ 9.06 8.96 1.12 │ 63184169131 63180873634 0.01 │ 504532 503384 0.23 │
│ rocq-elpi │ 16.93 16.70 1.38 │ 120037125362 120013119180 0.02 │ 470744 470460 0.06 │
│ rocq-mathcomp-ssreflect │ 1.16 1.12 3.57 │ 7373568718 7367212995 0.09 │ 613292 615088 -0.29 │
│ coq-core │ 2.84 2.74 3.65 │ 19086604871 19078997631 0.04 │ 92688 92892 -0.22 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
INFO: failed to install
coq-coquelicot (dependency install failed in NEW)
🐢 Top 25 slow downs:
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 62.9 65.4 2.4629 3.91% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 200 202 2.1316 1.07% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 236 237 1.2264 0.52% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 12.8 13.7 0.9864 7.74% 548 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 133 134 0.8976 0.68% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 49.6 50.5 0.8935 1.80% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 44.6 45.1 0.5471 1.23% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 39.7 40.2 0.5468 1.38% 81 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html │ │ 38.731 39.173 0.4420 1.14% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 44.7 45.1 0.4240 0.95% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 22.4 22.8 0.3930 1.75% 1073 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 27.4 27.7 0.3245 1.18% 13 coq-fourcolor/theories/proof/job287to290.v.html │ │ 44.6 45.0 0.3130 0.70% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 36.4 36.7 0.2782 0.76% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 126 126 0.2775 0.22% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 25.4 25.7 0.2744 1.08% 13 coq-fourcolor/theories/proof/job223to226.v.html │ │ 12.1 12.4 0.2742 2.26% 800 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html │ │ 67.4 67.6 0.2715 0.40% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 1.31 1.58 0.2643 20.13% 4 rocq-mathcomp-analysis/theories/pi_irrational.v.html │ │ 5.082 5.345 0.2630 5.18% 888 coq-vst/veric/binop_lemmas4.v.html │ │ 0.0330 0.293 0.2596 786.01% 95 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 103 103 0.2536 0.25% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 31.0 31.2 0.2434 0.79% 13 coq-fourcolor/theories/proof/job254to270.v.html │ │ 17.5 17.7 0.2432 1.39% 243 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 4.30 4.54 0.2418 5.63% 162 coq-category-theory/Instance/Coq/Par.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups:
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 41.2 39.6 -1.5704 -3.81% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 36.3 35.0 -1.3485 -3.71% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 5.37 4.69 -0.6810 -12.68% 1828 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 65.0 64.3 -0.6183 -0.95% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 16.5 15.9 -0.5864 -3.56% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 29.1 28.5 -0.5591 -1.92% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 27.1 26.6 -0.5483 -2.02% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 50.0 49.5 -0.4936 -0.99% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 105 104 -0.4870 -0.46% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 42.7 42.2 -0.4867 -1.14% 115 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 18.6 18.1 -0.4175 -2.25% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 0.683 0.273 -0.4108 -60.10% 398 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 6.414 6.022 -0.3920 -6.11% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 41.0 40.6 -0.3739 -0.91% 269 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 15.9 15.6 -0.3684 -2.31% 57 coq-category-theory/Instance/Fact.v.html │ │ 24.5 24.2 -0.3597 -1.47% 13 coq-fourcolor/theories/proof/job486to489.v.html │ │ 57.3 56.9 -0.3454 -0.60% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 64.8 64.5 -0.3073 -0.47% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 23.2 22.9 -0.3025 -1.30% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 0.296 0.000447 -0.2951 -99.85% 64 rocq-mathcomp-analysis/theories/topology_theory/connected.v.html │ │ 1.399 1.113 -0.2860 -20.44% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 4.37 4.10 -0.2729 -6.24% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v.html │ │ 0.284 0.0254 -0.2585 -91.07% 96 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 54.0 53.8 -0.2541 -0.47% 276 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 15.1 14.9 -0.2502 -1.65% 841 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
Loading