Closed JasonGross closed 2 years ago
https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/815/consoleText :
┌────────────────────────┬──────────────────────────┬────────────────────────────────────────────┬────────────────────────────────────────────┬───────────────────────────────┬───────────────────────┐ │ │ 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-mathcomp-ssreflect │ 43.05 43.33 -0.65 % │ 117889867748 118039211900 -0.13 % │ 153326738210 153262882755 +0.04 % │ 547632 547816 -0.03 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-performance-tests │ 65.64 65.96 -0.49 % │ 182581903759 183322492417 -0.40 % │ 194913529053 194816031006 +0.05 % │ 424592 424672 -0.02 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-solvable │ 192.92 193.37 -0.23 % │ 537120061079 538485006595 -0.25 % │ 762703147181 763400853980 -0.09 % │ 806580 806336 +0.03 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-field │ 225.99 226.23 -0.11 % │ 630335930549 630774664489 -0.07 % │ 942476276532 942512159337 -0.00 % │ 764568 764752 -0.02 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-character │ 189.51 189.68 -0.09 % │ 527635562619 527700589096 -0.01 % │ 738945772950 738804869413 +0.02 % │ 1041412 1041140 +0.03 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-odd-order │ 1345.02 1345.83 -0.06 % │ 3750155972180 3751462922126 -0.03 % │ 6448013642349 6448257936900 -0.00 % │ 1276272 1276212 +0.00 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-geocoq │ 1598.20 1597.98 +0.01 % │ 4454928490295 4455014341098 -0.00 % │ 6815415810469 6815580931692 -0.00 % │ 1400204 1399892 +0.02 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-hott │ 394.46 394.12 +0.09 % │ 1077909340354 1077495127679 +0.04 % │ 1732812733326 1732834138087 -0.00 % │ 563500 564668 -0.21 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-algebra │ 166.71 166.46 +0.15 % │ 464034463730 463799058286 +0.05 % │ 604975553370 604941978300 +0.01 % │ 643112 642908 +0.03 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-mathcomp-fingroup │ 53.82 53.66 +0.30 % │ 149032410263 149154905874 -0.08 % │ 207168253911 207278499832 -0.05 % │ 587024 586884 +0.02 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-rewriter │ 623.96 621.74 +0.36 % │ 1732040384880 1724761748330 +0.42 % │ 2653607834481 2642269741286 +0.43 % │ 1182556 1166876 +1.34 % │ 698 535 +30.47 % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-compcert │ 789.90 776.30 +1.75 % │ 2200662115442 2163268302981 +1.73 % │ 3166565321743 3118590469060 +1.54 % │ 1301696 1288132 +1.05 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-coqutil │ 64.07 59.60 +7.50 % │ 178071250053 165872740518 +7.35 % │ 226233523839 210734232710 +7.35 % │ 569032 546500 +4.12 % │ 0 0 +nan % │ ├────────────────────────┼──────────────────────────┼────────────────────────────────────────────┼────────────────────────────────────────────┼───────────────────────────────┼───────────────────────┤ │ coq-flocq │ 641.52 538.21 +19.20 % │ 1785546645181 1497310960127 +19.25 % │ 2688145966073 2287452729883 +17.52 % │ 1732512 1731084 +0.08 % │ 0 0 +nan % │ └────────────────────────┴──────────────────────────┴────────────────────────────────────────────┴────────────────────────────────────────────┴───────────────────────────────┴───────────────────────┘
https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/813/consoleText
┌────────────────────────┬─────────────────────────┬───────────────────────────────────────────┬───────────────────────────────────────────┬───────────────────────────────┬─────────────────────┐ │ │ 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-hott │ 361.92 363.86 -0.53 % │ 989384804073 991412603305 -0.20 % │ 1592205165912 1592237358960 -0.00 % │ 608496 608324 +0.03 % │ 8 7 +14.29 % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-performance-tests │ 11.50 11.53 -0.26 % │ 31520147102 31697493098 -0.56 % │ 54373619448 54404663515 -0.06 % │ 424292 424336 -0.01 % │ 15 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-solvable │ 178.76 179.22 -0.26 % │ 498152805640 498755578452 -0.12 % │ 705116333787 705121053403 -0.00 % │ 788596 788668 -0.01 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-field │ 214.67 215.22 -0.26 % │ 598513337461 598712153987 -0.03 % │ 896452606960 896511773393 -0.01 % │ 753192 753296 -0.01 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-math-classes │ 553.61 554.91 -0.23 % │ 1544476551134 1549406943350 -0.32 % │ 2145061361633 2146600528683 -0.07 % │ 636856 637240 -0.06 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-character │ 167.00 167.34 -0.20 % │ 464730024490 465193054134 -0.10 % │ 647370005341 647334141719 +0.01 % │ 854644 854396 +0.03 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-corn │ 1485.62 1487.91 -0.15 % │ 4144907464728 4148783172813 -0.09 % │ 6359687137536 6359657843595 +0.00 % │ 855672 855548 +0.01 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-algebra │ 154.18 154.37 -0.12 % │ 429312644941 428829561609 +0.11 % │ 557415239874 557422725324 -0.00 % │ 614176 609924 +0.70 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-color │ 2859.90 2862.21 -0.08 % │ 7973435002136 7981711174726 -0.10 % │ 9614801740341 9615495663829 -0.01 % │ 1553896 1554024 -0.01 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-fingroup │ 48.87 48.90 -0.06 % │ 135213618948 135183643870 +0.02 % │ 186654141450 186572964699 +0.04 % │ 560028 560076 -0.01 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-bedrock2 │ 488.63 488.91 -0.06 % │ 1359558733706 1360016351824 -0.03 % │ 2370796692406 2370575817782 +0.01 % │ 3168112 3168144 -0.00 % │ 4 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-coqutil │ 59.24 59.27 -0.05 % │ 164685445220 164625424558 +0.04 % │ 209623598492 209581246041 +0.02 % │ 545536 545856 -0.06 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-compcert │ 730.93 730.85 +0.01 % │ 2036600861548 2035210266974 +0.07 % │ 2914452546091 2914372144311 +0.00 % │ 1068284 1067736 +0.05 % │ 1 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-odd-order │ 1375.82 1374.70 +0.08 % │ 3835614001695 3833218102459 +0.06 % │ 6806282113618 6806251572331 +0.00 % │ 1285624 1285644 -0.00 % │ 2 15 -86.67 % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-flocq │ 244.78 244.50 +0.11 % │ 681626984789 679921678556 +0.25 % │ 913497086703 913528385583 -0.00 % │ 1017616 1017752 -0.01 % │ 27 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-coqprime │ 181.12 180.82 +0.17 % │ 501538627489 501645162975 -0.02 % │ 916069360947 916060831792 +0.00 % │ 807948 808372 -0.05 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-bignums │ 64.04 63.85 +0.30 % │ 177369874704 177205490551 +0.09 % │ 248818985630 248755086514 +0.03 % │ 494968 494908 +0.01 % │ 24 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-rewriter │ 582.46 578.20 +0.74 % │ 1617676389490 1607127324201 +0.66 % │ 2475187614357 2474301473763 +0.04 % │ 991000 1008336 -1.72 % │ 0 0 +nan % │ ├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤ │ coq-mathcomp-ssreflect │ 40.78 40.40 +0.94 % │ 110695586389 110431508668 +0.24 % │ 142744974801 142779471929 -0.02 % │ 524504 524724 -0.04 % │ 2 0 +nan % │ └────────────────────────┴─────────────────────────┴───────────────────────────────────────────┴───────────────────────────────────────────┴───────────────────────────────┴─────────────────────┘
We dropped this column in coq/coq#16628
https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/815/consoleText :
https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/813/consoleText