Ali Caglayan (Mar 01 2022 at 22:09): Ali Caglayan (Mar 01 2022 at 22:09):@Gaëtan Gilbert Here is PMP's bench results:
┌─────────────────────────────┬──────────────────────────┬────────────────────────────────────────┬────────────────────────────────────────┬─────────────────────────┬───────────────────┐
│ │ 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-character │ 70.66 79.84 -11.50 │ 309650143211 349552147854 -11.42 │ 473233306442 533356959306 -11.27 │ 831280 850960 -2.31 │ 0 0 nan │
│ coq-mathcomp-field │ 106.68 118.66 -10.10 │ 467163156882 519961709245 -10.15 │ 775203032255 861754575747 -10.04 │ 706500 709584 -0.43 │ 0 0 nan │
│ coq-mathcomp-fingroup │ 22.54 24.58 -8.30 │ 98535314247 107246272837 -8.12 │ 143801085872 157015806181 -8.42 │ 485680 491352 -1.15 │ 0 0 nan │
│ coq-mathcomp-algebra │ 61.36 66.41 -7.60 │ 268199644900 290363664637 -7.63 │ 369848487016 402702056465 -8.16 │ 599400 600408 -0.17 │ 0 0 nan │
│ coq-mathcomp-solvable │ 84.48 90.71 -6.87 │ 369918514142 397492629336 -6.94 │ 568424594180 613607761446 -7.36 │ 700848 667228 5.04 │ 0 0 nan │
│ coq-mathcomp-odd-order │ 546.40 573.90 -4.79 │ 2395036139147 2515736957530 -4.80 │ 4117735437721 4288221208083 -3.98 │ 1224284 1224284 0.00 │ 0 0 nan │
│ coq-mathcomp-ssreflect │ 25.90 27.04 -4.22 │ 113053007541 117725045087 -3.97 │ 143090532730 149262182907 -4.13 │ 534404 537308 -0.54 │ 0 0 nan │
│ coq-coquelicot │ 34.88 35.36 -1.36 │ 150878931509 152591188256 -1.12 │ 199842237416 202567560429 -1.35 │ 757436 754196 0.43 │ 177 0 nan │
│ coq-engine-bench-lite │ 180.63 182.64 -1.10 │ 759173512577 768249860098 -1.18 │ 1490196503446 1495589332446 -0.36 │ 1234680 1234436 0.02 │ 0 0 nan │
│ coq-compcert │ 288.97 291.21 -0.77 │ 1257903989737 1265518491253 -0.60 │ 1889669407409 1889678479758 -0.00 │ 1105852 1105100 0.07 │ 0 6 -100.00 │
│ coq-verdi │ 48.88 49.17 -0.59 │ 212360230374 213520305444 -0.54 │ 319798399313 321426729576 -0.51 │ 836384 836608 -0.03 │ 1 0 nan │
│ coq-rewriter-perf-SuperFast │ 953.66 959.31 -0.59 │ 4168714161781 4192534801310 -0.57 │ 7266525408654 7270019904327 -0.05 │ 1145112 1144460 0.06 │ 8 0 nan │
│ coq-fourcolor │ 1500.12 1506.50 -0.42 │ 6564836317472 6591337665547 -0.40 │ 12083532700773 12114931531060 -0.26 │ 757396 757388 0.00 │ 0 0 nan │
│ coq-corn │ 778.18 780.71 -0.32 │ 3397555868865 3408838854393 -0.33 │ 5278194890403 5278236725940 -0.00 │ 881448 878596 0.32 │ 0 0 nan │
│ coq-color │ 214.81 215.49 -0.32 │ 933178790584 934140207519 -0.10 │ 1326478266315 1325985542500 0.04 │ 1152040 1150944 0.10 │ 0 0 nan │
│ coq-stdlib │ 415.08 416.29 -0.29 │ 1484707025816 1491334563352 -0.44 │ 1417913147985 1427353970740 -0.66 │ 609260 607200 0.34 │ 0 0 nan │
│ coq-rewriter │ 384.69 385.58 -0.23 │ 1677551004497 1681815171041 -0.25 │ 2771599851732 2771964625861 -0.01 │ 1060240 1060184 0.01 │ 3 6 -50.00 │
│ coq-category-theory │ 1683.53 1687.26 -0.22 │ 7375677771687 739[1567](https://gitlab.com/coq/coq/-/jobs/2144162601#L1567)768913 -0.21 │ 15422034794400 15423704526601 -0.01 │ 1468512 1469252 -0.05 │ 0 0 nan │
│ coq-performance-tests-lite │ 799.58 801.28 -0.21 │ 3479858350582 3486969092197 -0.20 │ 5944992126627 5960180848965 -0.25 │ 1824428 1824532 -0.01 │ 2 0 nan │
│ coq-fiat-crypto │ 2897.46 2901.96 -0.16 │ 12641871053812 12663475979006 -0.17 │ 23224367429208 23218965992429 0.02 │ 3849312 3849336 -0.00 │ 95 98 -3.06 │
│ coq-verdi-raft │ 575.84 576.25 -0.07 │ 2516690216963 2518271739781 -0.06 │ 3924715937249 3923565304365 0.03 │ 1256904 1232808 1.95 │ 0 0 nan │
│ coq-vst │ 1088.65 1089.10 -0.04 │ 4754945208563 4758534982720 -0.08 │ 7709936264228 7707931364641 0.03 │ 2111496 2112656 -0.05 │ 3 0 nan │
│ coq-bedrock2 │ 222.45 222.45 0.00 │ 971898865141 972406809060 -0.05 │ 1768413232048 1768220377581 0.01 │ 2052096 2052144 -0.00 │ 61 8 662.50 │
│ coq-unimath │ 4433.03 4430.66 0.05 │ 19412384844907 19402187215352 0.05 │ 38982227224963 38968115896564 0.04 │ 3258216 3258384 -0.01 │ 8 3 166.67 │
│ coq-geocoq │ 721.74 721.08 0.09 │ 3150292248945 3147525918525 0.09 │ 4988859378713 4995258501103 -0.13 │ 1076316 1076024 0.03 │ 9 26 -65.38 │
│ coq-bignums │ 28.74 28.71 0.10 │ 125505733393 125563273148 -0.05 │ 172267106579 172228509742 0.02 │ 468964 469292 -0.07 │ 0 0 nan │
│ coq-hott │ 166.54 166.35 0.11 │ 723803010755 723806574252 -0.00 │ 1150986843450 1151000210755 -0.00 │ 617464 617084 0.06 │ 0 0 nan │
│ coq-fiat-core │ 56.97 56.88 0.16 │ 235336883601 234790729296 0.23 │ 331403263157 331017480568 0.12 │ 481396 479688 0.36 │ 1 0 nan │
│ coq-flocq3 │ 78.92 78.77 0.19 │ 343531680884 343325856989 0.06 │ 454741898608 454816682441 -0.02 │ 988232 991480 -0.33 │ 73 0 nan │
│ coq-coqprime │ 43.61 43.51 0.23 │ 189234013293 189100244810 0.07 │ 280260701151 280099666827 0.06 │ 763512 763868 -0.05 │ 0 0 nan │
│ coq-fiat-parsers │ 344.35 343.44 0.26 │ 1485128528115 1481617512802 0.24 │ 2451047799679 2450737202831 0.01 │ 2694788 2694892 -0.00 │ 0 7 -100.00 │
│ coq-math-classes │ 93.46 93.21 0.27 │ 405268779476 405018802563 0.06 │ 571525199879 571521262818 0.00 │ 502472 503012 -0.11 │ 0 0 nan │
│ coq-core │ 107.85 107.26 0.55 │ 389869796349 388164587348 0.44 │ 44[1586](https://gitlab.com/coq/coq/-/jobs/2144162601#L1586)936808 441922569214 -0.08 │ 277748 277940 -0.07 │ 1 0 nan │
│ coq-coqutil │ 36.09 35.67 1.18 │ 155196604810 153941864632 0.82 │ 208856125037 208662337830 0.09 │ 608704 608764 -0.01 │ 4 4 0.00 │
└─────────────────────────────┴──────────────────────────┴────────────────────────────────────────┴────────────────────────────────────────┴─────────────────────────┴───────────────────┘
It seems to me gitlab picked up 1586 in the number for example and linked it as a line number.
Ali Caglayan (Mar 01 2022 at 22:10):What is weird is that it didn't do this everywhere, nor can it be seen in the log....
Ali Caglayan (Mar 01 2022 at 22:10):It seems like something that happens during copy time (I am guessing)
Gaëtan Gilbert (Mar 01 2022 at 23:02):It doesn't happen for me
maybe because I have copy events disabled
Ali Caglayan (Mar 10 2022 at 20:31):@Pierre-Marie Pédrot I think I've worked out what is going on. When you select the bench results the log line numbers are also links, so it seems you are inadvertently copying those as well.
Ali Caglayan (Mar 10 2022 at 20:35):Since i am working on the bench summary stuff at the moment, I will also dump the table into a file so you can browse artifacts and copy the table no problem.
Ali Caglayan (Mar 10 2022 at 20:35):I am using firefox and I have no issue copying the table.
Pierre-Marie Pédrot (Mar 10 2022 at 20:47):Ideally coqbot should do that alone.
Pierre-Marie Pédrot (Mar 10 2022 at 20:47):like, writing @coqbot bench should run a bench and when it finishes coqbot pastes stuff back in that comment
Ali Caglayan (Mar 10 2022 at 20:52):I think that should be easy enough to do
Last updated: Dec 07 2023 at 04:02 UTC