OCaml Performance Numbers - coq/coq GitHub Wiki
This page is meant to collect some miscellaneous benchmarks, best fit uses "overhead=200":
4.07.1 vs 4.11.1:
βββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββ β β user time [s] β CPU cycles β CPU instructions β max resident mem [KB] β mem faults β β β β β β β β β package_name β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-fourcolor β 2219.53 2521.57 -11.98 % β 6188352401580 7018881497705 -11.83 % β 12570826950155 11446962364839 +9.82 % β 819672 774980 +5.77 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-rewriter-perf-SuperFast β 1007.96 1057.93 -4.72 % β 2804145845820 2941994213577 -4.69 % β 4626204295813 4629296786612 -0.07 % β 1070104 1070760 -0.06 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-engine-bench-lite β 367.42 382.39 -3.91 % β 1032929756316 1075374563874 -3.95 % β 1760988596378 1837850703519 -4.18 % β 3294368 3508672 -6.11 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-rewriter β 593.12 611.01 -2.93 % β 1646095524284 1695075682115 -2.89 % β 2597286055082 2583778137837 +0.52 % β 1049640 1036416 +1.28 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-fiat-parsers β 630.43 644.30 -2.15 % β 1764748168865 1806067063580 -2.29 % β 2908550025100 2718213247620 +7.00 % β 3373196 2997960 +12.52 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-unimath β 3919.63 3989.04 -1.74 % β 10898395420607 11099620651127 -1.81 % β 21093424472985 21162644041489 -0.33 % β 1026212 1113256 -7.82 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-bedrock2 β 217.20 220.11 -1.32 % β 601861572804 608365035725 -1.07 % β 1013857394019 1003205178221 +1.06 % β 1087880 1087500 +0.03 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-coqutil β 58.82 59.57 -1.26 % β 162808378553 165334755466 -1.53 % β 211647767225 204977885884 +3.25 % β 509512 528856 -3.66 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-fiat-crypto β 4894.45 4953.55 -1.19 % β 13595520117501 13747186151354 -1.10 % β 24526173681941 23634361532446 +3.77 % β 2147396 2325156 -7.65 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-performance-tests-lite β 538.64 545.08 -1.18 % β 1506723766518 1523763571503 -1.12 % β 2679843639051 2794946296622 -4.12 % β 691160 747372 -7.52 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-odd-order β 1062.18 1071.17 -0.84 % β 2958394905201 2983994850900 -0.86 % β 4768819205838 4750383014522 +0.39 % β 1051004 995372 +5.59 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-verdi-raft β 1254.39 1263.46 -0.72 % β 3492868234006 3517381749092 -0.70 % β 4960765830528 4897357937114 +1.29 % β 927808 934576 -0.72 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-field β 289.07 291.06 -0.68 % β 804868064537 810595834280 -0.71 % β 1252412058517 1249550256940 +0.23 % β 834736 827656 +0.86 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-hott β 315.38 316.95 -0.50 % β 854928579097 857698454914 -0.32 % β 1398285756188 1376082294104 +1.61 % β 608732 635908 -4.27 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-character β 161.14 160.48 +0.41 % β 448019105121 445943831113 +0.47 % β 631960923427 619054071468 +2.08 % β 749340 735360 +1.90 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-geocoq β 1483.24 1474.56 +0.59 % β 4135126562389 4107465640498 +0.67 % β 6397763675247 6222387074122 +2.82 % β 1182616 1164380 +1.57 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-flocq β 161.80 160.28 +0.95 % β 448324438753 445543638301 +0.62 % β 570944112262 553096576990 +3.23 % β 833232 822056 +1.36 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-coqprime β 81.93 80.60 +1.65 % β 224639297465 222180114513 +1.11 % β 328100100367 310424105697 +5.69 % β 782568 768524 +1.83 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-bignums β 59.78 58.72 +1.81 % β 165901498444 161734022002 +2.58 % β 229964583586 215328903715 +6.80 % β 471316 472088 -0.16 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-corn β 1793.86 1761.80 +1.82 % β 4996195675938 4906886376306 +1.82 % β 7830505518407 7512945384964 +4.23 % β 859932 855748 +0.49 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-solvable β 175.76 172.59 +1.84 % β 489179286418 480510685593 +1.80 % β 702143836157 677602444160 +3.62 % β 705904 691792 +2.04 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-lambda-rust β 1291.28 1263.65 +2.19 % β 3593132019711 3517748788483 +2.14 % β 5145701602052 4950184399389 +3.95 % β 1238984 1174724 +5.47 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-algebra β 143.19 140.04 +2.25 % β 398316964221 390407936233 +2.03 % β 527671353637 503677892197 +4.76 % β 572976 565056 +1.40 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-verdi β 124.84 121.47 +2.77 % β 343435639901 335773985565 +2.28 % β 433051775261 413624326565 +4.70 % β 570712 574152 -0.60 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-fingroup β 49.70 48.16 +3.20 % β 137393049422 133302011858 +3.07 % β 193756629526 183798025741 +5.42 % β 495060 486332 +1.79 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-mathcomp-ssreflect β 52.56 50.65 +3.77 % β 143746267854 138368567687 +3.89 % β 189078340757 176319199609 +7.24 % β 532388 520776 +2.23 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-math-classes β 198.47 191.09 +3.86 % β 554361501369 532163857417 +4.17 % β 755487792735 700314983260 +7.88 % β 508836 505068 +0.75 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-compcert β 699.29 664.91 +5.17 % β 1948548051819 1854076888671 +5.10 % β 2786337702812 2556013202303 +9.01 % β 1128004 1131220 -0.28 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq β 573.61 543.64 +5.51 % β 1604572527057 1518215487986 +5.69 % β 2237429635889 2073882823396 +7.89 % β 604468 592392 +2.04 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-fiat-core β 112.51 106.18 +5.96 % β 319253112246 302260752861 +5.62 % β 437435530782 401496545163 +8.95 % β 485268 487352 -0.43 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-color β 656.62 618.91 +6.09 % β 1830626663379 1726226996352 +6.05 % β 2416311450164 2190563233295 +10.31 % β 1593232 1455000 +9.50 % β 0 0 +nan % β βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€ β coq-coquelicot β 75.48 69.50 +8.60 % β 206859130050 191017016431 +8.29 % β 276977963077 245324147911 +12.90 % β 590580 587328 +0.55 % β 0 0 +nan % β βββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
4.07.1+flambda vs 4.11.1+flambda
βββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββ
β β user time [s] β CPU cycles β CPU instructions β max resident mem [KB] β mem faults β
β β β β β β β
β package_name β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fourcolor β 2172.69 2470.79 -12.06 % β 6061341210998 6888709975479 -12.01 % β 12402383426379 11287819140928 +9.87 % β 869216 788728 +10.20 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-engine-bench-lite β 347.21 361.40 -3.93 % β 976745485772 1016444055313 -3.91 % β 1644187565147 1716646663352 -4.22 % β 3507676 3016152 +16.30 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter-perf-SuperFast β 919.14 954.31 -3.69 % β 2560583470132 2655293334965 -3.57 % β 4115076283441 4099855753867 +0.37 % β 1123692 1218252 -7.76 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-parsers β 583.85 597.80 -2.33 % β 1638050041183 1674420289473 -2.17 % β 2662877450413 2472909026975 +7.68 % β 3393448 3291140 +3.11 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter β 538.50 548.95 -1.90 % β 1493416260820 1523284470286 -1.96 % β 2299874568862 2279513085454 +0.89 % β 1076564 1015164 +6.05 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-field β 255.63 259.43 -1.46 % β 711190400552 722650556761 -1.59 % β 1098439459967 1095942307297 +0.23 % β 857636 859464 -0.21 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqutil β 53.09 53.69 -1.12 % β 147768702298 149237552668 -0.98 % β 186590955375 180115452639 +3.60 % β 548888 576608 -4.81 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-unimath β 3489.70 3526.20 -1.04 % β 9706127177846 9810912690460 -1.07 % β 18837068150843 18879101752334 -0.22 % β 1137628 1159956 -1.92 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-crypto β 4570.77 4610.20 -0.86 % β 12691362042182 12802015193368 -0.86 % β 22594779738523 21725871874261 +4.00 % β 2876500 2472132 +16.36 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-hott β 290.69 291.76 -0.37 % β 787484584412 786546849889 +0.12 % β 1266474310523 1245261048905 +1.70 % β 667548 715548 -6.71 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-performance-tests-lite β 466.44 467.74 -0.28 % β 1303209988923 1307731054428 -0.35 % β 2203726441345 2326501838070 -5.28 % β 864396 824960 +4.78 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-odd-order β 954.15 955.21 -0.11 % β 2659333440267 2657968526311 +0.05 % β 4174794741419 4148834444544 +0.63 % β 1026840 1011056 +1.56 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-character β 144.79 144.65 +0.10 % β 402727088860 402013478980 +0.18 % β 560855199026 545803217654 +2.76 % β 767612 772220 -0.60 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi-raft β 1109.71 1107.66 +0.19 % β 3090649452737 3084565638170 +0.20 % β 4279036230680 4207519323294 +1.70 % β 967980 964264 +0.39 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bedrock2 β 193.67 193.22 +0.23 % β 536182897768 534293642972 +0.35 % β 878384058716 864892111295 +1.56 % β 1139500 1165248 -2.21 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-algebra β 131.12 129.31 +1.40 % β 364812873077 358366270970 +1.80 % β 471572869514 446378993329 +5.64 % β 612536 604112 +1.39 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-flocq β 144.55 141.88 +1.88 % β 401510392532 393854883309 +1.94 % β 492974009754 474256960108 +3.95 % β 880276 912956 -3.58 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-geocoq β 1316.38 1292.04 +1.88 % β 3670945758064 3602333993694 +1.90 % β 5589346496254 5404402012895 +3.42 % β 1177360 1182936 -0.47 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqprime β 75.65 74.04 +2.17 % β 207162686636 203309095756 +1.90 % β 296861032673 278772720923 +6.49 % β 828552 818012 +1.29 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-solvable β 159.14 155.30 +2.47 % β 443079421804 432000160065 +2.56 % β 625659620523 596703103219 +4.85 % β 733344 728036 +0.73 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq β 1020.96 993.59 +2.75 % β 2843503120291 2768213861344 +2.72 % β 3937968761753 3757222677125 +4.81 % β 650836 706616 -7.89 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-corn β 1621.45 1571.71 +3.16 % β 4513393848598 4376504980709 +3.13 % β 6923329363035 6596195406268 +4.96 % β 813348 836040 -2.71 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi β 114.97 111.44 +3.17 % β 316763320171 306925627120 +3.21 % β 387829410950 365953589574 +5.98 % β 598456 601932 -0.58 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-lambda-rust β 1134.96 1097.26 +3.44 % β 3159759583217 3056276853849 +3.39 % β 4474268530223 4259900902370 +5.03 % β 1190672 1170844 +1.69 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-fingroup β 45.33 43.66 +3.83 % β 125813030667 121619787834 +3.45 % β 175119745692 165130893337 +6.05 % β 530928 531868 -0.18 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-ssreflect β 49.36 47.49 +3.94 % β 134918485537 129861307196 +3.89 % β 174352514531 161542540190 +7.93 % β 570272 570368 -0.02 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-math-classes β 177.55 170.37 +4.21 % β 495975882954 475045422169 +4.41 % β 644285699048 598139114550 +7.72 % β 546168 547716 -0.28 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bignums β 53.77 51.30 +4.81 % β 148947406950 141546711171 +5.23 % β 203120741165 189020497773 +7.46 % β 500700 513128 -2.42 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-core β 107.53 102.16 +5.26 % β 306284297375 289918082456 +5.65 % β 407396635475 374420622422 +8.81 % β 525772 534444 -1.62 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-compcert β 640.87 600.34 +6.75 % β 1786882282162 1672543403818 +6.84 % β 2478545132024 2239153830576 +10.69 % β 1168660 1186696 -1.52 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-color β 594.21 554.88 +7.09 % β 1656268360652 1549355376464 +6.90 % β 2111129264905 1894984169802 +11.41 % β 1606460 1507776 +6.55 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coquelicot β 70.37 64.37 +9.32 % β 192961897845 176872122264 +9.10 % β 252791002794 220540720885 +14.62 % β 634152 644728 -1.64 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
4.11.1 vs 4.11.1+flambda (https://gitlab.com/coq/coq/-/jobs/748909781)
βββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββ
β β user time [s] β CPU cycles β CPU instructions β max resident mem [KB] β mem faults β
β β β β β β β
β package_name β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-performance-tests-lite β 472.87 545.64 -13.34 % β 1322732099296 1524450014152 -13.23 % β 2203152205994 2678293479457 -17.74 % β 864356 691116 +25.07 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-lambda-rust β 1135.10 1296.26 -12.43 % β 3157824438256 3608696275653 -12.49 % β 4472155241698 5145063716562 -13.08 % β 1194816 1114264 +7.23 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi-raft β 1109.22 1263.66 -12.22 % β 3090634812733 3517623958105 -12.14 % β 4278781399231 4960477607664 -13.74 % β 960924 930368 +3.28 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-unimath β 3477.01 3949.46 -11.96 % β 9668031521164 10990066158751 -12.03 % β 18844121596146 21092496625365 -10.66 % β 1137128 1026112 +10.82 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-field β 255.36 290.01 -11.95 % β 710662039980 807785981545 -12.02 % β 1098235892038 1251956429028 -12.28 % β 856428 835340 +2.52 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-geocoq β 1321.33 1496.96 -11.73 % β 3680632949850 4170245224177 -11.74 % β 5589972184326 6398756511042 -12.64 % β 1185424 1167516 +1.53 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bedrock2 β 193.58 219.27 -11.72 % β 535713883848 606881122165 -11.73 % β 878370444224 1013536929098 -13.34 % β 1125800 1087504 +3.52 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-flocq β 144.06 162.82 -11.52 % β 400181244902 451733046922 -11.41 % β 492993658703 571503088586 -13.74 % β 880192 833044 +5.66 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-odd-order β 953.13 1072.82 -11.16 % β 2655900939966 2988193533870 -11.12 % β 4174386765131 4768660348658 -12.46 % β 1077040 1006556 +7.00 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-math-classes β 178.15 200.51 -11.15 % β 496367068903 559901309534 -11.35 % β 644123061067 755476328927 -14.74 % β 545260 509244 +7.07 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bignums β 53.57 60.22 -11.04 % β 148337829397 166501804368 -10.91 % β 203211040967 229839617244 -11.59 % β 500420 471508 +6.13 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-corn β 1410.76 1582.36 -10.84 % β 3932246569883 4405412622010 -10.74 % β 6068723885927 6838398039761 -11.26 % β 813068 834792 -2.60 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-character β 144.49 161.84 -10.72 % β 402102614659 449714209447 -10.59 % β 560528048545 631306705116 -11.21 % β 765388 751464 +1.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter β 537.58 601.04 -10.56 % β 1491288383776 1667086480122 -10.55 % β 2299241907052 2596971656154 -11.46 % β 1068964 1049580 +1.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-solvable β 159.17 176.88 -10.01 % β 442390810430 491855486026 -10.06 % β 626741120874 701905754300 -10.71 % β 748644 706156 +6.02 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqutil β 53.14 58.94 -9.84 % β 147993750909 163770793848 -9.63 % β 186558455705 211654892334 -11.86 % β 547920 508060 +7.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-color β 594.46 658.90 -9.78 % β 1658391946008 1840212244712 -9.88 % β 2111583212277 2416626937290 -12.62 % β 1606296 1592708 +0.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter-perf-SuperFast β 923.30 1020.22 -9.50 % β 2570564755758 2838290435233 -9.43 % β 4113482231482 4625118229704 -11.06 % β 1120100 1069936 +4.69 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-compcert β 641.27 704.48 -8.97 % β 1785643830643 1962234189217 -9.00 % β 2475530003084 2785334066792 -11.12 % β 1167904 1127472 +3.59 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-algebra β 130.88 143.70 -8.92 % β 363611526988 399789727681 -9.05 % β 471245755960 527729296294 -10.70 % β 612332 572328 +6.99 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-fingroup β 45.32 49.47 -8.39 % β 125619772140 137386462805 -8.56 % β 175084693429 193435071001 -9.49 % β 530600 494900 +7.21 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-hott β 290.54 317.12 -8.38 % β 788194635136 859733870787 -8.32 % β 1266452514490 1396060588636 -9.28 % β 669644 604344 +10.81 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi β 114.40 124.68 -8.25 % β 316100145625 344700463756 -8.30 % β 387914881493 433036517006 -10.42 % β 598500 594740 +0.63 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqprime β 75.26 81.55 -7.71 % β 206537995461 224936631974 -8.18 % β 296577559646 328219391367 -9.64 % β 828336 782468 +5.86 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-parsers β 583.87 632.13 -7.63 % β 1636430934269 1770518267294 -7.57 % β 2663564402228 2907592648811 -8.39 % β 3276076 3373356 -2.88 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-crypto β 4578.38 4920.66 -6.96 % β 12717892949866 13664260232521 -6.93 % β 22606375544279 24533628614853 -7.86 % β 2876532 2141212 +34.34 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coquelicot β 70.70 75.69 -6.59 % β 193610947150 207955770350 -6.90 % β 252810274590 276879593196 -8.69 % β 633764 590260 +7.37 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-ssreflect β 49.09 52.35 -6.23 % β 134903516535 143966212553 -6.30 % β 174938089991 189398009030 -7.63 % β 570228 531472 +7.29 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-engine-bench-lite β 349.13 368.58 -5.28 % β 982030343643 1037852634993 -5.38 % β 1641074787413 1762282414893 -6.88 % β 3507820 3494580 +0.38 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-core β 107.06 111.81 -4.25 % β 306028793641 320009415699 -4.37 % β 407361267564 437305959035 -6.85 % β 525888 484384 +8.57 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fourcolor β 2162.92 2211.50 -2.20 % β 6024730080500 6160280075591 -2.20 % β 12402576854690 12567265137273 -1.31 % β 868824 819696 +5.99 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq β 1020.00 576.65 +76.88 % β 2842349755889 1611578371294 +76.37 % β 3936033487502 2236879126659 +75.96 % β 667292 592764 +12.57 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
4,11.1 vs 4.11.1 + best_fit (https://gitlab.com/coq/coq/-/jobs/746857605) pending:
βββββββββββββββββββββββββββββββ¬ββββββββββββββββββββββββββ¬ββββββββββββββββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββ
β β user time [s] β CPU cycles β CPU instructions β max resident mem [KB] β mem faults β
β β β β β β β
β package_name β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coquelicot β 70.50 75.87 -7.08 % β 193729618766 207671485050 -6.71 % β 254993873219 277051483411 -7.96 % β 599036 590428 +1.46 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-color β 630.95 659.21 -4.29 % β 1760370031245 1838451662548 -4.25 % β 2291785108765 2415601444120 -5.13 % β 1640204 1592792 +2.98 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bignums β 57.68 60.26 -4.28 % β 159885622372 167062181403 -4.30 % β 219345536489 229938285743 -4.61 % β 474920 471420 +0.74 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-math-classes β 192.14 200.21 -4.03 % β 536371837913 559253430708 -4.09 % β 719666953262 755377151165 -4.73 % β 498956 508992 -1.97 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-compcert β 675.62 703.30 -3.94 % β 1881905913862 1959230763524 -3.95 % β 2649357683369 2784388721613 -4.85 % β 1124192 1127900 -0.33 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-fingroup β 48.07 49.75 -3.38 % β 132838356381 137902558026 -3.67 % β 186122534571 193837403266 -3.98 % β 493708 494904 -0.24 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqprime β 79.92 82.42 -3.03 % β 219681155813 225724215550 -2.68 % β 319027421168 328242084177 -2.81 % β 782032 782184 -0.02 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-corn β 1536.69 1582.44 -2.89 % β 4273874355026 4403659832587 -2.95 % β 6628601262966 6836713060808 -3.04 % β 950688 834580 +13.91 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-ssreflect β 51.19 52.71 -2.88 % β 139681639382 144342819179 -3.23 % β 182313572317 189424566559 -3.75 % β 531892 531336 +0.10 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-core β 109.46 112.48 -2.68 % β 311332180721 320365184857 -2.82 % β 427542273489 437430705779 -2.26 % β 484920 484268 +0.13 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq β 563.21 576.96 -2.38 % β 1576308819076 1610245205465 -2.11 % β 2187544058282 2236810220429 -2.20 % β 588512 593052 -0.77 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-parsers β 618.86 633.39 -2.29 % β 1731265852835 1773448494310 -2.38 % β 2837844349251 2907499643517 -2.40 % β 3185016 3292800 -3.27 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-algebra β 140.42 143.61 -2.22 % β 390604794512 399565389731 -2.24 % β 512879774055 527841955613 -2.83 % β 576352 572288 +0.71 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-geocoq β 1461.12 1493.98 -2.20 % β 4075268960726 4166243815994 -2.18 % β 6236381796162 6398556401954 -2.53 % β 1221920 1191516 +2.55 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-solvable β 173.03 176.90 -2.19 % β 481144093191 492429762180 -2.29 % β 686128455787 702752912769 -2.37 % β 680280 706156 -3.66 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-lambda-rust β 1271.18 1297.36 -2.02 % β 3538746227038 3610610704151 -1.99 % β 5018531663035 5148591281629 -2.53 % β 1243264 1240428 +0.23 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-flocq β 158.82 162.01 -1.97 % β 440997225748 450394534027 -2.09 % β 555344854721 571593317994 -2.84 % β 872752 833092 +4.76 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi β 122.99 125.12 -1.70 % β 337997031382 344917237326 -2.01 % β 421104566739 433019971219 -2.75 % β 574116 574096 +0.00 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqutil β 58.01 58.98 -1.64 % β 161030503409 164083407046 -1.86 % β 208079402963 211691925677 -1.71 % β 531724 514240 +3.40 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi-raft β 1244.16 1263.08 -1.50 % β 3462934018058 3518212047686 -1.57 % β 4874874038819 4960714126158 -1.73 % β 941672 930088 +1.25 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-character β 159.78 161.84 -1.27 % β 443960589531 449540801004 -1.24 % β 623282276969 631466635522 -1.30 % β 791620 752584 +5.19 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bedrock2 β 217.23 219.42 -1.00 % β 601859855713 607877387382 -0.99 % β 1001604661928 1013525757593 -1.18 % β 1148996 1087608 +5.64 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-field β 287.36 289.79 -0.84 % β 800412664016 807119830866 -0.83 % β 1238362139593 1251971647883 -1.09 % β 873596 835420 +4.57 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter β 595.64 600.59 -0.82 % β 1652364467440 1667197877731 -0.89 % β 2575236402885 2596875935952 -0.83 % β 1046812 1038728 +0.78 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-performance-tests-lite β 541.80 546.12 -0.79 % β 1512194522848 1525722340376 -0.89 % β 2649980012493 2678635591138 -1.07 % β 756412 691164 +9.44 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-odd-order β 1067.62 1072.76 -0.48 % β 2971447338179 2988380872167 -0.57 % β 4725684317412 4769156590256 -0.91 % β 1003436 1006520 -0.31 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-crypto β 4901.88 4921.50 -0.40 % β 13618416019125 13671238004379 -0.39 % β 24254031646040 24526638041381 -1.11 % β 2151052 2147644 +0.16 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-engine-bench-lite β 369.29 370.08 -0.21 % β 1039543257940 1041264191280 -0.17 % β 1736565527762 1766066617798 -1.67 % β 4028992 3494580 +15.29 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter-perf-SuperFast β 1022.17 1022.82 -0.06 % β 2842725985388 2845896155919 -0.11 % β 4585416965244 4625096605447 -0.86 % β 1300264 1070088 +21.51 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-unimath β 3945.17 3941.19 +0.10 % β 10970777090175 10966299554603 +0.04 % β 21055731354020 21094885852005 -0.19 % β 1197992 1026192 +16.74 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-hott β 316.49 315.38 +0.35 % β 857746303708 856941986913 +0.09 % β 1398028494237 1395944773155 +0.15 % β 601572 604456 -0.48 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fourcolor β 2222.27 2210.66 +0.53 % β 6198510775582 6165506233851 +0.54 % β 12481702909540 12567128965262 -0.68 % β 853260 819564 +4.11 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββ΄ββββββββββββββββββββββββββ΄ββββββββββββββββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
4.07.1 vs 4.11.1 + best_fit (https://gitlab.com/coq/coq/-/jobs/741853859)
βββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββ¬ββββββββββββββββββββ
β β user time [s] β CPU cycles β CPU instructions β max resident mem [KB] β mem faults β
β β β β β β β
β package_name β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β NEW OLD PDIFF β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fourcolor β 2208.20 2515.67 -12.22 % β 6159422285184 7013825265291 -12.18 % β 12479144575450 11447327440831 +9.01 % β 853156 775076 +10.07 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-parsers β 619.50 646.15 -4.12 % β 1735126031141 1808696168932 -4.07 % β 2838550717211 2718308274041 +4.42 % β 3185216 2997820 +6.25 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter-perf-SuperFast β 1030.98 1062.95 -3.01 % β 2867748850504 2957929888632 -3.05 % β 4585672381839 4629792501126 -0.95 % β 1300288 1070648 +21.45 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-engine-bench-lite β 374.03 382.28 -2.16 % β 1051103034220 1075893896203 -2.30 % β 1737296645168 1836802613305 -5.42 % β 4070992 3508608 +16.03 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-rewriter β 598.61 610.92 -2.01 % β 1661211393708 1697511318644 -2.14 % β 2574577998925 2583861631743 -0.36 % β 1047460 1036884 +1.02 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqutil β 58.26 59.18 -1.55 % β 161580392326 164369606377 -1.70 % β 208089699381 204982955620 +1.52 % β 531876 528920 +0.56 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coqprime β 80.06 81.10 -1.28 % β 219965606364 222148875778 -0.98 % β 319079856819 310407543066 +2.79 % β 782048 768480 +1.77 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-unimath β 3962.45 4003.12 -1.02 % β 11024288561939 11138423121186 -1.02 % β 21051121077382 21169051946498 -0.56 % β 1214140 1113564 +9.03 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-flocq β 159.30 160.55 -0.78 % β 442141054386 444858019255 -0.61 % β 555367689174 553082669644 +0.41 % β 873748 822152 +6.28 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-crypto β 4919.52 4955.62 -0.73 % β 13651691890501 13765111101646 -0.82 % β 24269169435898 23635281614825 +2.68 % β 2156812 2339816 -7.82 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi-raft β 1252.41 1261.15 -0.69 % β 3488554192335 3509951514886 -0.61 % β 4875375109872 4897289511440 -0.45 % β 947468 934672 +1.37 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-field β 289.33 291.03 -0.58 % β 805174394380 810577501518 -0.67 % β 1238371870909 1249551428572 -0.89 % β 873180 825976 +5.71 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bedrock2 β 218.48 219.42 -0.43 % β 604883094095 608617199014 -0.61 % β 1001695193394 1003268567223 -0.16 % β 1149148 1087364 +5.68 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-geocoq β 1472.14 1474.00 -0.13 % β 4102229640371 4112364285360 -0.25 % β 6236354838250 6222306192639 +0.23 % β 1231056 1147624 +7.27 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-performance-tests-lite β 545.55 546.06 -0.09 % β 1523706134075 1525018234346 -0.09 % β 2650504876062 2794681720014 -5.16 % β 756544 747360 +1.23 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-fingroup β 48.11 48.06 +0.10 % β 133142460404 133348436384 -0.15 % β 186097692665 183850811227 +1.22 % β 493724 486340 +1.52 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-bignums β 58.32 58.11 +0.36 % β 160860843862 160627147837 +0.15 % β 219322383504 215331314434 +1.85 % β 474828 472144 +0.57 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-odd-order β 1074.52 1068.44 +0.57 % β 2992236515501 2978079039587 +0.48 % β 4725839951155 4750344215863 -0.52 % β 1004716 994032 +1.07 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-corn β 1771.62 1761.20 +0.59 % β 4934590397008 4901326716356 +0.68 % β 7611974748873 7512882355561 +1.32 % β 950988 855988 +11.10 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-character β 160.98 159.90 +0.68 % β 447187125934 445380591886 +0.41 % β 623765722069 619098431123 +0.75 % β 790548 736704 +7.31 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-lambda-rust β 1274.17 1263.20 +0.87 % β 3545991125663 3516340102274 +0.84 % β 5016270117803 4947745242286 +1.38 % β 1222968 1174820 +4.10 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-solvable β 174.01 172.51 +0.87 % β 484446784090 480253546322 +0.87 % β 686104243810 677668026916 +1.24 % β 679492 691948 -1.80 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-hott β 318.06 315.05 +0.96 % β 861854398522 856708496892 +0.60 % β 1398975739207 1376024905209 +1.67 % β 579712 635964 -8.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-verdi β 122.79 121.62 +0.96 % β 338703843788 335957978534 +0.82 % β 421118943256 413673407150 +1.80 % β 570748 574240 -0.61 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-ssreflect β 51.17 50.66 +1.01 % β 139831170592 138430324263 +1.01 % β 182268137034 176280676935 +3.40 % β 532584 520832 +2.26 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-mathcomp-algebra β 141.93 140.34 +1.13 % β 393248098935 390141024521 +0.80 % β 513136676800 503715278515 +1.87 % β 574280 565036 +1.64 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-coquelicot β 70.84 69.87 +1.39 % β 194607296865 191135104045 +1.82 % β 254996589554 245303622507 +3.95 % β 599300 587168 +2.07 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-compcert β 678.71 665.87 +1.93 % β 1889485385741 1856340836411 +1.79 % β 2649341650215 2555954385433 +3.65 % β 1124164 1131392 -0.64 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-math-classes β 193.92 190.08 +2.02 % β 540195760748 530267944670 +1.87 % β 719549432958 700334701606 +2.74 % β 498856 504748 -1.17 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-color β 633.18 617.46 +2.55 % β 1766537049254 1724694289532 +2.43 % β 2292326187434 2190545821844 +4.65 % β 1638820 1455240 +12.62 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq-fiat-core β 110.22 105.95 +4.03 % β 312971015270 301974056873 +3.64 % β 426957676501 401523424965 +6.33 % β 484804 487364 -0.53 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββββββββΌββββββββββββββββββββββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββΌββββββββββββββββββββ€
β coq β 566.12 542.99 +4.26 % β 1580218181016 1517998084424 +4.10 % β 2187950201891 2073653504771 +5.51 % β 597436 592388 +0.85 % β 0 0 +nan % β
βββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββ΄ββββββββββββββββββββ
To the extent possible under law, the contributors of βCocorico!, the Coq wikiβ have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.