change computation of uniform parameters #21498
Open
coqbot-app / bench
succeeded
Jan 14, 2026 in 0s
Bench completed successfully
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 │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-bedrock2 │ 350.82 356.01 -1.46 │ 2918448077214 2918831134627 -0.01 │ 833532 837648 -0.49 │
│ coq-neural-net-interp-computed-lite │ 236.68 239.23 -1.07 │ 2268249393528 2268188956738 0.00 │ 872384 873572 -0.14 │
│ rocq-bignums │ 25.00 25.22 -0.87 │ 159113139207 159101923018 0.01 │ 460492 459488 0.22 │
│ rocq-metarocq-translations │ 15.57 15.70 -0.83 │ 110704930443 110723179616 -0.02 │ 777224 775460 0.23 │
│ rocq-mathcomp-order │ 80.52 81.15 -0.78 │ 599949217825 600018660944 -0.01 │ 2021684 2024160 -0.12 │
│ coq-engine-bench-lite │ 127.89 128.87 -0.76 │ 957467814539 959576059733 -0.22 │ 1037116 1037244 -0.01 │
│ coq-coqprime │ 52.96 53.27 -0.58 │ 362113432029 362217939534 -0.03 │ 823616 825660 -0.25 │
│ rocq-mathcomp-fingroup │ 26.62 26.77 -0.56 │ 173982760499 174000992103 -0.01 │ 601668 601556 0.02 │
│ coq-category-theory │ 552.42 554.92 -0.45 │ 4048251203140 4049925205502 -0.04 │ 930720 931548 -0.09 │
│ coq-corn │ 648.62 651.55 -0.45 │ 4381154856386 4381276724116 -0.00 │ 768052 766860 0.16 │
│ coq-vst │ 840.93 844.61 -0.44 │ 6367478477302 6367410490920 0.00 │ 2063160 2061132 0.10 │
│ rocq-mathcomp-solvable │ 103.00 103.45 -0.43 │ 720856976779 720859750297 -0.00 │ 1528032 1528132 -0.01 │
│ coq-coquelicot │ 46.58 46.78 -0.43 │ 274568482104 274548594651 0.01 │ 841100 840684 0.05 │
│ coq-fiat-crypto-with-bedrock │ 7076.13 7105.81 -0.42 │ 58141213985563 58140580459726 0.00 │ 3117540 3105308 0.39 │
│ coq-rewriter │ 333.91 335.29 -0.41 │ 2488972941032 2489071434538 -0.00 │ 1492264 1495064 -0.19 │
│ rocq-metarocq-pcuic │ 628.52 630.86 -0.37 │ 4024774053046 4024786509265 -0.00 │ 1919120 1921328 -0.11 │
│ coq-iris-examples │ 366.61 367.84 -0.33 │ 2415816463426 2415816875371 -0.00 │ 1128484 1127652 0.07 │
│ rocq-mathcomp-algebra │ 332.15 333.23 -0.32 │ 2487722418604 2487708091285 0.00 │ 1628028 1624800 0.20 │
│ coq-fiat-parsers │ 276.24 277.07 -0.30 │ 2114131958940 2114085921299 0.00 │ 2259128 2256164 0.13 │
│ rocq-metarocq-common │ 40.57 40.69 -0.29 │ 261095278811 261073821573 0.01 │ 905692 905544 0.02 │
│ coq-mathcomp-odd-order │ 608.38 609.95 -0.26 │ 4380404144232 4380499909965 -0.00 │ 3369772 3369592 0.01 │
│ coq-hott │ 154.32 154.71 -0.25 │ 1043894431904 1043826399245 0.01 │ 465956 468244 -0.49 │
│ rocq-metarocq-safechecker │ 358.47 359.35 -0.24 │ 2644054675529 2644550457338 -0.02 │ 1845204 1854284 -0.49 │
│ coq-math-classes │ 83.23 83.42 -0.23 │ 506116242604 506120371061 -0.00 │ 512708 513692 -0.19 │
│ rocq-elpi │ 16.00 16.03 -0.19 │ 112372538776 112339754518 0.03 │ 579516 576120 0.59 │
│ rocq-mathcomp-character │ 101.69 101.88 -0.19 │ 726534925632 726480683870 0.01 │ 2148332 2148048 0.01 │
│ coq-mathcomp-analysis │ 1083.07 1084.29 -0.11 │ 8189121565487 8188054669498 0.01 │ 2630272 2628708 0.06 │
│ coq-rewriter-perf-SuperFast │ 479.20 479.54 -0.07 │ 3737547146175 3737110856992 0.01 │ 1252456 1262172 -0.77 │
│ coq-unimath │ 1803.31 1803.38 -0.00 │ 14950670506162 14950374284949 0.00 │ 1072072 1073716 -0.15 │
│ coq-verdi │ 43.55 43.55 0.00 │ 289089929855 289079005242 0.00 │ 525968 526000 -0.01 │
│ coq-compcert │ 311.39 311.34 0.02 │ 2044127205747 2043898347668 0.01 │ 1186068 1186556 -0.04 │
│ coq-coqutil │ 46.71 46.69 0.04 │ 291984613935 291987392222 -0.00 │ 564572 564176 0.07 │
│ coq-fourcolor │ 1366.46 1365.77 0.05 │ 12570687729889 12570408146267 0.00 │ 1416616 1418568 -0.14 │
│ coq-performance-tests-lite │ 913.57 912.37 0.13 │ 7318191679221 7314148367531 0.06 │ 1840200 1840132 0.00 │
│ rocq-mathcomp-boot │ 39.61 39.53 0.20 │ 233311398857 233287939420 0.01 │ 752728 751552 0.16 │
│ rocq-metarocq-template │ 82.73 82.56 0.21 │ 568094968687 568134249806 -0.01 │ 1049264 1049936 -0.06 │
│ rocq-metarocq-erasure │ 479.33 478.30 0.22 │ 3273026521074 3273083471599 -0.00 │ 1894100 1892500 0.08 │
│ coq-fiat-core │ 55.25 55.12 0.24 │ 336312530025 336306151141 0.00 │ 480340 482532 -0.45 │
│ rocq-mathcomp-field │ 187.73 187.27 0.25 │ 1433298506149 1433471000973 -0.01 │ 2736932 2736536 0.01 │
│ coq-verdi-raft │ 494.97 493.34 0.33 │ 3406705213504 3406575398914 0.00 │ 817056 817028 0.00 │
│ coq-color │ 230.90 230.06 0.37 │ 1460586618280 1460598123148 -0.00 │ 1148380 1147624 0.07 │
│ rocq-metarocq-utils │ 24.08 23.98 0.42 │ 155405880137 155401697882 0.00 │ 596256 594000 0.38 │
│ rocq-runtime │ 74.30 73.84 0.62 │ 537922434811 537785135880 0.03 │ 498952 495896 0.62 │
│ rocq-stdlib │ 449.69 446.73 0.66 │ 1547995078269 1547938818146 0.00 │ 627736 630216 -0.39 │
│ rocq-mathcomp-ssreflect │ 1.20 1.18 1.69 │ 8314771941 8315537140 -0.01 │ 863156 862732 0.05 │
│ rocq-core │ 6.88 6.76 1.78 │ 40944022741 40907251613 0.09 │ 437352 437820 -0.11 │
│ rocq-equations │ 8.70 8.49 2.47 │ 59875291442 59905008773 -0.05 │ 398896 397832 0.27 │
│ coq-core │ 2.76 2.69 2.60 │ 18308484682 18316555063 -0.04 │ 88856 88936 -0.09 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
🐢 Top 25 slow downs:
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 96.2 97.6 1.3503 1.40% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 11.5 12.2 0.7100 6.18% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 1.23 1.79 0.5610 45.55% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 27.2 27.7 0.5125 1.89% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 46.6 47.1 0.4216 0.90% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 11.8 12.2 0.4121 3.50% 324 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 0.248 0.626 0.3772 151.88% 34 rocq-stdlib/theories/Logic/SetoidChoice.v.html │ │ 24.6 25.0 0.3699 1.50% 12 coq-fourcolor/theories/proof/job319to322.v.html │ │ 11.7 12.0 0.3535 3.03% 388 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 46.6 46.9 0.3311 0.71% 115 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 4.02 4.32 0.2996 7.45% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 29.8 30.1 0.2947 0.99% 12 coq-fourcolor/theories/proof/job001to106.v.html │ │ 18.0 18.3 0.2856 1.59% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 29.0 29.3 0.2793 0.96% 145 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 0.346 0.622 0.2765 79.92% 586 rocq-stdlib/theories/Strings/Byte.v.html │ │ 29.3 29.6 0.2648 0.90% 12 coq-fourcolor/theories/proof/job589to610.v.html │ │ 0.326 0.590 0.2636 80.85% 1 rocq-stdlib/theories/ZArith/ZNsatz.v.html │ │ 0.261 0.518 0.2577 98.89% 19 rocq-stdlib/theories/FSets/FSetFacts.v.html │ │ 6.79 7.03 0.2473 3.64% 842 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 28.7 28.9 0.2387 0.83% 12 coq-fourcolor/theories/proof/job563to588.v.html │ │ 7.61 7.85 0.2369 3.11% 633 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 0.274 0.506 0.2320 84.74% 13 rocq-stdlib/theories/ZArith/Zmin.v.html │ │ 0.306 0.530 0.2234 72.91% 11 rocq-stdlib/theories/setoid_ring/Rings_Q.v.html │ │ 120 120 0.2229 0.19% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 20.8 21.0 0.2226 1.07% 479 rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups:
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 67.6 62.7 -4.9549 -7.33% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 67.6 64.7 -2.8590 -4.23% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 203 201 -2.4097 -1.19% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 40.5 38.8 -1.6610 -4.10% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 44.7 43.4 -1.3687 -3.06% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 31.5 30.5 -0.9931 -3.15% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 30.6 -0.9813 -3.11% 157 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 32.8 31.8 -0.9752 -2.97% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.7 30.8 -0.9578 -3.02% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 30.8 -0.8258 -2.61% 180 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.5 30.7 -0.8212 -2.61% 166 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.4 30.6 -0.8041 -2.56% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 30.8 -0.8021 -2.54% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 42.4 41.6 -0.7493 -1.77% 246 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 65.5 64.8 -0.6869 -1.05% 716 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 18.2 17.6 -0.5770 -3.17% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 33.3 32.7 -0.5540 -1.67% 12 coq-fourcolor/theories/proof/job439to465.v.html │ │ 45.7 45.2 -0.5427 -1.19% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 33.789 33.278 -0.5110 -1.51% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 31.4 30.9 -0.5030 -1.60% 258 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 26.6 26.2 -0.4529 -1.70% 62 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html │ │ 48.4 48.0 -0.4374 -0.90% 260 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 1.44 1.01 -0.4291 -29.81% 690 rocq-stdlib/theories/setoid_ring/Field_theory.v.html │ │ 31.7 31.2 -0.4261 -1.35% 334 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 34.2 33.8 -0.4210 -1.23% 960 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
Loading