Stream: Coq devs & plugin devs

Topic: Interlacing of bench results


view this post on Zulip 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.

view this post on Zulip 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....

view this post on Zulip Ali Caglayan (Mar 01 2022 at 22:10):

It seems like something that happens during copy time (I am guessing)

view this post on Zulip Gaëtan Gilbert (Mar 01 2022 at 23:02):

It doesn't happen for me
maybe because I have copy events disabled

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 10 2022 at 20:35):

I am using firefox and I have no issue copying the table.

view this post on Zulip Pierre-Marie Pédrot (Mar 10 2022 at 20:47):

Ideally coqbot should do that alone.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 10 2022 at 20:52):

I think that should be easy enough to do


Last updated: Feb 06 2023 at 00:03 UTC