Fix the relevance generated by the set / pose tactics.

[ppedrot]

No description provided.

[ppedrot]

Bench: https://gitlab.com/coq/coq/-/jobs/1729371231

[Alizter]

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬───────────────────┐
│                             │      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-coqprime │  187.70   191.15  -1.80 │   822175728547    836910736103  -1.76 │  1561615692436   1561276310348   0.02 │  831956   855008  -2.70 │   0    0      nan │
│                    coq-core │  102.45   103.29  -0.81 │   379669688980    379088175600   0.15 │   435099754136    435038025610   0.01 │  247916   248364  -0.18 │   1    0      nan │
│               coq-fourcolor │ 1511.31  1523.41  -0.79 │  6611040049186   6664312546888  -0.80 │ 12104717998745  12104501920582   0.00 │  729952   730236  -0.04 │   0    0      nan │
│                   coq-flocq │   77.16    77.76  -0.77 │   336248633367    338866380108  -0.77 │   448090745261    448160134290  -0.02 │  992088   994048  -0.20 │   8    0      nan │
│ coq-rewriter-perf-SuperFast │  923.79   929.61  -0.63 │  4036505218698   4062857027204  -0.65 │  6973398480121   6974337107960  -0.01 │ 1151264  1147168   0.36 │  17   16     6.25 │
│                 coq-bignums │   29.15    29.28  -0.44 │   127749501571    127736352323   0.01 │   176743388658    176757245305  -0.01 │  468852   468940  -0.02 │   0    0      nan │
│                 coq-unimath │ 2787.94  2798.83  -0.39 │ 12202866629315  12250360062638  -0.39 │ 24345318076007  24346445220603  -0.00 │ 3834164  3834164   0.00 │   5    9   -44.44 │
│      coq-mathcomp-odd-order │  594.94   597.15  -0.37 │  2607870270657   2617786019469  -0.38 │  4475783791066   4475770372554   0.00 │  937316   937132   0.02 │   0    0      nan │
│                coq-rewriter │  388.89   390.15  -0.32 │  1697378833632   1702384725676  -0.29 │  2792007533471   2790151841590   0.07 │ 1063308  1063548  -0.02 │   0    0      nan │
│                    coq-hott │  159.55   159.98  -0.27 │   693400738031    691987137207   0.20 │  1091125228805   1091205832106  -0.01 │  663440   659508   0.60 │   0    0      nan │
│            coq-math-classes │   95.22    95.44  -0.23 │   415284686327    415510790518  -0.05 │   590128336452    590097794708   0.01 │  495900   494892   0.20 │   0    0      nan │
│      coq-mathcomp-character │   80.20    80.36  -0.20 │   351225183157    352020494120  -0.23 │   540293675356    540344016482  -0.01 │  740016   741300  -0.17 │   0    0      nan │
│       coq-mathcomp-fingroup │   24.27    24.31  -0.16 │   106301685233    106407404180  -0.10 │   156963355466    156957457974   0.00 │  483448   481436   0.42 │   0    0      nan │
│        coq-mathcomp-algebra │   65.99    66.08  -0.14 │   288976698316    288904582009   0.02 │   404271253817    404357502376  -0.02 │  561756   561052   0.13 │   0    0      nan │
│  coq-performance-tests-lite │  811.44   812.49  -0.13 │  3532143898825   3536762555531  -0.13 │  6014772293518   6016832197756  -0.03 │ 2062468  2066040  -0.17 │   4    0      nan │
│           coq-iris-examples │  471.42   471.41   0.00 │  2058193367571   2059201393758  -0.05 │  3131810691160   3131884165631  -0.00 │ 1183864  1183636   0.02 │  20    0      nan │
│          coq-mathcomp-field │  120.61   120.57   0.03 │   528296176156    528358867971  -0.01 │   873163898480    873186178207  -0.00 │  663492   663760  -0.04 │   0    0      nan │
│                   coq-verdi │   50.09    50.07   0.04 │   217524322132    217603064472  -0.04 │   325980008415    325964477394   0.00 │  830392   830096   0.04 │   3    3     0.00 │
│             coq-fiat-crypto │ 2874.97  2872.37   0.09 │ 12551343645333  12538605267419   0.10 │ 23163794553102  23164662902229  -0.00 │ 2268460  2258252   0.45 │   1   13   -92.31 │
│               coq-perennial │ 3948.03  3943.16   0.12 │ 17270975556327  17248551669474   0.13 │ 28837519531036  28843207208955  -0.02 │ 2714824  2715332  -0.02 │   1    1     0.00 │
│              coq-verdi-raft │  599.52   598.70   0.14 │  2618386675546   2617329767584   0.04 │  4038003363390   4037999331394   0.00 │ 1219576  1218284   0.11 │   0    0      nan │
│                    coq-corn │  823.08   821.74   0.16 │  3598302156710   3591835439347   0.18 │  5605842930684   5605576797663   0.00 │  830608   828372   0.27 │   0    0      nan │
│            coq-fiat-parsers │  340.47   339.44   0.30 │  1472635423072   1467901151941   0.32 │  2432859349692   2432848980833   0.00 │ 2799028  2798572   0.02 │   0    0      nan │
│                   coq-color │  270.19   269.18   0.38 │  1175199541361   1170011615143   0.44 │  1592477048182   1592296338892   0.01 │ 1241424  1243168  -0.14 │   0    0      nan │
│                  coq-geocoq │  742.12   739.07   0.41 │  3240948312697   3228223534378   0.39 │  5153220224929   5152814242430   0.01 │ 1044792  1045040  -0.02 │   0    0      nan │
│       coq-mathcomp-solvable │   93.06    92.67   0.42 │   407402307890    405676276692   0.43 │   630294918612    630332646453  -0.01 │  663652   662944   0.11 │   0    0      nan │
│               coq-fiat-core │   55.32    55.06   0.47 │   232849782492    230678903766   0.94 │   323686548794    323594886145   0.03 │  474356   474456  -0.02 │   0    0      nan │
│      coq-mathcomp-ssreflect │   26.57    26.43   0.53 │   115435711695    115037513465   0.35 │   146700138683    146718068862  -0.01 │  536956   542212  -0.97 │   0    0      nan │
│                 coq-coqutil │   33.08    32.88   0.61 │   142712252698    141630138156   0.76 │   188289902960    188284414368   0.00 │  601460   601088   0.06 │   0    0      nan │
│       coq-engine-bench-lite │  181.16   179.99   0.65 │   761233344810    755444693303   0.77 │  1477020750063   1476731434391   0.02 │ 1293820  1294080  -0.02 │   0    0      nan │
│              coq-coquelicot │   36.14    35.76   1.06 │   155543552223    154123510964   0.92 │   203868993976    203814392627   0.03 │  749432   748348   0.14 │  46    2  2200.00 │
│                coq-bedrock2 │  178.70   175.10   2.06 │   781313247951    765915535520   2.01 │  1431919735898   1431349829962   0.04 │  790424   790492  -0.01 │   0    0      nan │
│                  coq-stdlib │  430.14   418.91   2.68 │  1530199067701   1506305574630   1.59 │  1447047683852   1446969842259   0.01 │  593216   593368  -0.03 │   0    0      nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘

[Alizter]

That seems like a big increase in the stdlib.

[ppedrot]

coq-stlidb has a strong tendency to be noisy, I am more concerned by bedrock2 which does appear in the per-line diff.

[SkySkimmer]

I'm not sure it's that noisy, at least when I looked at some past benches stdlib didn't seem to create outliers.

[ppedrot]

Let's get another bench: https://gitlab.com/coq/coq/-/jobs/1744108867

[ppedrot]

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬──────────────────┐
│                             │      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 │ 1515.41  1523.99  -0.56 │  6631815735000   6668017436421  -0.54 │ 12105043247558  12104666038228   0.00 │  732108   729896   0.30 │   0    0     nan │
│       coq-engine-bench-lite │  180.49   180.64  -0.08 │   758204931752    759786276693  -0.21 │  1474653836390   1482191322726  -0.51 │ 1294124  1293956   0.01 │   0    0     nan │
│                  coq-stdlib │  418.36   418.52  -0.04 │  1514314900785   1516448747029  -0.14 │  1447120540229   1446931402964   0.01 │  591908   592000  -0.02 │   0    0     nan │
│                    coq-core │  102.34   102.25   0.09 │   384646426421    379265888982   1.42 │   435525196984    435208574656   0.07 │  247340   248776  -0.58 │   0    0     nan │
│              coq-verdi-raft │  598.90   598.00   0.15 │  2616260742483   2612402840508   0.15 │  4038142778517   4038096254634   0.00 │ 1219300  1216344   0.24 │   0    0     nan │
│                coq-rewriter │  390.05   389.18   0.22 │  1702066087458   1697755707292   0.25 │  2790300249014   2790357894630  -0.00 │ 1067004  1063484   0.33 │   0    0     nan │
│ coq-rewriter-perf-SuperFast │  930.04   927.30   0.30 │  4064467460510   4051854727126   0.31 │  6976333624721   6975261647901   0.02 │ 1147096  1147856  -0.07 │  15   16   -6.25 │
│      coq-mathcomp-character │   80.58    80.30   0.35 │   352895588582    351843023671   0.30 │   540316961744    540261249544   0.01 │  741564   739024   0.34 │   0    0     nan │
│                   coq-flocq │   77.26    76.94   0.42 │   336764879192    334970219896   0.54 │   448165476418    447957096745   0.05 │  993212   990876   0.24 │  26    0     nan │
│                 coq-unimath │ 2795.14  2783.25   0.43 │ 12234685486099  12183799927849   0.42 │ 24346135476240  24346394575974  -0.00 │ 3834260  3834480  -0.01 │  13    2  550.00 │
│               coq-perennial │ 3950.04  3932.28   0.45 │ 17277855433796  17199025574300   0.46 │ 28848521820483  28848365209279   0.00 │ 2712608  2713624  -0.04 │   1    1    0.00 │
│        coq-mathcomp-algebra │   66.18    65.86   0.49 │   289459273009    287714841201   0.61 │   404259512669    404240020420   0.00 │  560232   560152   0.01 │   0    0     nan │
│                 coq-bignums │   29.45    29.30   0.51 │   128386048390    128010750546   0.29 │   176774319873    176788538892  -0.01 │  466040   471252  -1.11 │   0    0     nan │
│          coq-mathcomp-field │  120.26   119.63   0.53 │   526929962687    524326491224   0.50 │   873368366347    873345700229   0.00 │  662756   662400   0.05 │   0    0     nan │
│                    coq-corn │  823.77   819.12   0.57 │  3600872065890   3579485844690   0.60 │  5606411075466   5606201449802   0.00 │  828632   828452   0.02 │   0    0     nan │
│             coq-fiat-crypto │ 2881.80  2864.36   0.61 │ 12581379569877  12504797303284   0.61 │ 23153215212441  23150932491357   0.01 │ 2265904  2250640   0.68 │   1   18  -94.44 │
│      coq-mathcomp-ssreflect │   26.62    26.44   0.68 │   115748248367    115261990554   0.42 │   146678085133    146738696098  -0.04 │  536848   536900  -0.01 │   0    0     nan │
│            coq-math-classes │   95.83    95.11   0.76 │   416642342671    413468639518   0.77 │   590142001517    590123226156   0.00 │  496404   496468  -0.01 │   0    0     nan │
│                  coq-geocoq │  742.67   737.07   0.76 │  3242948437614   3219463517329   0.73 │  5153137985242   5152695166783   0.01 │ 1047124  1046868   0.02 │   0    0     nan │
│                coq-bedrock2 │  175.87   174.43   0.83 │   768564866722    763283856617   0.69 │  1431835338764   1431921044747  -0.01 │  790252   790724  -0.06 │   0    0     nan │
│            coq-fiat-parsers │  342.51   339.64   0.85 │  1480048100729   1469019506856   0.75 │  2433030202638   2433116795007  -0.00 │ 2798408  2799012  -0.02 │   0    0     nan │
│           coq-iris-examples │  473.88   469.70   0.89 │  2069766949466   2051546579075   0.89 │  3132316668699   3132267491058   0.00 │ 1183828  1183508   0.03 │  14    0     nan │
│                    coq-hott │  160.35   158.91   0.91 │   696767736722    690091271089   0.97 │  1091295243930   1091315579304  -0.00 │  659952   659424   0.08 │   0    0     nan │
│                   coq-verdi │   50.52    50.05   0.94 │   219557655225    217263370453   1.06 │   326003430477    325999315890   0.00 │  831128   830608   0.06 │   3    3    0.00 │
│                   coq-color │  269.36   266.73   0.99 │  1171014436837   1160642313371   0.89 │  1592585968884   1592379132040   0.01 │ 1242476  1243948  -0.12 │   0    0     nan │
│       coq-mathcomp-fingroup │   24.41    24.17   0.99 │   106832171374    105343627389   1.41 │   156983872683    156939164016   0.03 │  479936   481028  -0.23 │   0    0     nan │
│              coq-coquelicot │   35.96    35.59   1.04 │   155535006006    153784721495   1.14 │   203780377002    203794678288  -0.01 │  750960   749132   0.24 │  32    0     nan │
│                coq-coqprime │  187.48   185.23   1.21 │   820354389458    811143440513   1.14 │  1561472841225   1562125303116  -0.04 │  856472   856096   0.04 │   0    0     nan │
│       coq-mathcomp-solvable │   93.33    92.12   1.31 │   408540939271    403375317758   1.28 │   630267400157    630240044782   0.00 │  663664   664396  -0.11 │   0    0     nan │
│      coq-mathcomp-odd-order │  599.45   590.90   1.45 │  2628404601821   2590010625692   1.48 │  4475788689375   4475679722487   0.00 │  936968   937460  -0.05 │   0    0     nan │
│  coq-performance-tests-lite │  818.82   806.89   1.48 │  3563694664879   3511452546198   1.49 │  6016517644702   6016385537616   0.00 │ 2062452  2064636  -0.11 │   2    0     nan │
│                 coq-coqutil │   33.27    32.72   1.68 │   143680763870    140956640564   1.93 │   188295624362    188264559635   0.02 │  601264   599996   0.21 │   0    0     nan │
│               coq-fiat-core │   55.81    54.57   2.27 │   233620431288    229670614000   1.72 │   323717434148    323585165197   0.04 │  475152   474740   0.09 │   0    0     nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴──────────────────┘

Hmm, was it noise in the end? Bedrock does not appear any more in the per-line diff. 🐙

[herbelin]

Hmm, was it noise in the end? Bedrock does not appear any more in the per-line diff. 🐙

By the way, should we trust more the time or the CPU instructions?

[ppedrot]

Cycles, even more than instructions.

[herbelin]

I said instructions because they seem more stable from one run to the other, while cycles seem more in line with times. So, should I conclude from your answer that running several times and computing an average time is eventually more faithful to the reality than counting the instructions?

[ppedrot]

Averaging is always better, but I think that despite the PR that removed the noise from opam resolution, the new machines are still quite noisy. I don't know why but pendulum was clearly around a 1% noise threshold, whereas we get move movement now.

[ppedrot]

What do we do with this PR? The code change is definitely sound and desired by anybody using SProp (I can testify personally) but I am still a bit concerned this might be a bit slower in practice. Should we run another bench, or one with several runs? cc @SkySkimmer

[SkySkimmer]

Using relevance_of_term c instead of relevance_of_type t may be faster.

[ppedrot]

I am not sure about that. Since we already compute the type, the latter should be more compact in general than the term so that the relevance is going to require less term crawling.

Relatedly, I had a look at relevance_of_term and it's broken because it claims that the relevance of a product is given by its codomain, but that's a type so always relevant.

[SkySkimmer]

relevance_of_type needs reduction, relevance_of_term doesn't

Relatedly, I had a look at relevance_of_term and it's broken because it claims that the relevance of a product is given by its codomain, but that's a type so always relevant.

PR when?

[herbelin]

The code change is definitely sound and desired by anybody using SProp

This is my opinion too.

I did not look at details, so this is a bit speculative, but can't the computation of relevance be only in the Some case, assuming that typ_of would compute the relevance itself?

From a practical point of view, I'm more actually also worried about SProp not being a subtype a Prop. To address the efficiency problem, couldn't we have in the longer term explicit coercions which would avoid recomputing the relevance?

[ppedrot]

To address the efficiency problem, couldn't we have in the longer term explicit coercions which would avoid recomputing the relevance?

Rather, typing and friends should return not only the type but also the sort it lives in.

[herbelin]

Rather, typing and friends should return not only the type but also the sort it lives in.

Already, right. Maybe not too complicated to do actually??

[ppedrot]

Bench with relevance_of_term: https://gitlab.com/coq/coq/-/jobs/1776762641

[ppedrot]

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬───────────────────┐
│                             │      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-core │   98.77   101.31  -2.51 │   389406007208    386137870083   0.85 │   434416328563    434343053959   0.02 │  249408   249472  -0.03 │   0    0      nan │
│                  coq-stdlib │  415.16   417.82  -0.64 │  1516049848189   1524101875326  -0.53 │  1446185116996   1446389670989  -0.01 │  598260   599292  -0.17 │   0    0      nan │
│      coq-mathcomp-character │   79.86    80.09  -0.29 │   349859246293    351152473900  -0.37 │   538496296760    538497676106  -0.00 │  731944   732292  -0.05 │   0    0      nan │
│          coq-mathcomp-field │  120.32   120.54  -0.18 │   527031723585    528055770329  -0.19 │   869350370692    869345278064   0.00 │  661988   662448  -0.07 │   0    0      nan │
│               coq-fourcolor │ 1506.93  1509.50  -0.17 │  6594107121282   6604812776889  -0.16 │ 12098571500101  12098978203954  -0.00 │  730424   730792  -0.05 │   0    0      nan │
│       coq-mathcomp-fingroup │   24.32    24.35  -0.12 │   106171913775    106329703719  -0.15 │   156552001388    156546834590   0.00 │  481408   481416  -0.00 │   0    0      nan │
│       coq-engine-bench-lite │  182.89   183.11  -0.12 │   770130498722    770414009868  -0.04 │  1489508335222   1488170657671   0.09 │ 1293904  1295896  -0.15 │   0    0      nan │
│                    coq-hott │  158.79   158.95  -0.10 │   691030312594    690868008800   0.02 │  1083830365676   1083853770801  -0.00 │  660776   660292   0.07 │   0    0      nan │
│               coq-fiat-core │   55.40    55.45  -0.09 │   232603592111    232853262522  -0.11 │   321143299840    321058678619   0.03 │  474736   474628   0.02 │   0    0      nan │
│             coq-fiat-crypto │ 2889.51  2891.84  -0.08 │ 12616343130553  12625733991586  -0.07 │ 23262056277930  23252668866353   0.04 │ 2261816  2259420   0.11 │   1    6   -83.33 │
│           coq-iris-examples │  476.89   477.27  -0.08 │  2083088888007   2085264015533  -0.10 │  3150414865091   3150526332710  -0.00 │ 1184764  1186628  -0.16 │   4    0      nan │
│ coq-rewriter-perf-SuperFast │  965.89   966.39  -0.05 │  4222959053507   4225356947613  -0.06 │  7314192173494   7315600351801  -0.02 │ 1146520  1149752  -0.28 │  26   16    62.50 │
│                 coq-unimath │ 2983.86  2985.34  -0.05 │ 13064810372839  13070268476182  -0.04 │ 26008536217220  26008113761601   0.00 │ 3858012  3867820  -0.25 │   7    8   -12.50 │
│                coq-rewriter │  388.95   389.10  -0.04 │  1696746424461   1698549011669  -0.11 │  2785481002071   2785647514939  -0.01 │ 1067160  1063328   0.36 │   0    0      nan │
│      coq-mathcomp-ssreflect │   26.51    26.52  -0.04 │   115552294899    115524931758   0.02 │   146302783630    146318811114  -0.01 │  534740   534932  -0.04 │   0    0      nan │
│      coq-mathcomp-odd-order │  590.61   590.75  -0.02 │  2589342304709   2589937469366  -0.02 │  4437029466644   4436925650592   0.00 │  944028   944628  -0.06 │   0    0      nan │
│                 coq-bignums │   29.44    29.41   0.10 │   128046807115    128192156081  -0.11 │   176617307544    176617751415  -0.00 │  466520   465764   0.16 │   1    0      nan │
│            coq-fiat-parsers │  340.85   340.41   0.13 │  1473731058354   1472874672672   0.06 │  2428917805386   2428586696100   0.01 │ 2799468  2798396   0.04 │   0    0      nan │
│                  coq-geocoq │  744.11   742.98   0.15 │  3247691233897   3244606568344   0.10 │  5157938850535   5158100093149  -0.00 │ 1083272  1079968   0.31 │   0    0      nan │
│                    coq-corn │  827.72   826.26   0.18 │  3616787972176   3610259861511   0.18 │  5609050821574   5609221197960  -0.00 │  828424   828400   0.00 │   0    0      nan │
│              coq-verdi-raft │  600.67   599.56   0.19 │  2624425442780   2619361632624   0.19 │  4046408945800   4046468947229  -0.00 │ 1223184  1221384   0.15 │   0    0      nan │
│                   coq-flocq │   76.69    76.51   0.24 │   333718305684    332822510505   0.27 │   442982135810    443029765391  -0.01 │  987064   987748  -0.07 │   8    0      nan │
│                coq-bedrock2 │  177.82   177.39   0.24 │   777909775398    776423014853   0.19 │  1453693664867   1453841054431  -0.01 │  791416   791692  -0.03 │   2    0      nan │
│       coq-mathcomp-solvable │   92.34    92.08   0.28 │   404634284996    403376642118   0.31 │   626703080841    626845709643  -0.02 │  662492   662304   0.03 │   0    0      nan │
│               coq-perennial │ 4004.22  3991.70   0.31 │ 17517275247010  17463299799692   0.31 │ 29085393845858  29083218048171   0.01 │ 2707764  2710012  -0.08 │   1    1     0.00 │
│                 coq-coqutil │   33.03    32.92   0.33 │   142395137411    141845999142   0.39 │   187191068830    187149526157   0.02 │  601136   600944   0.03 │   0    0      nan │
│  coq-performance-tests-lite │  813.41   810.57   0.35 │  3540909625734   3529238350504   0.33 │  6024078469991   6022122583182   0.03 │ 1832740  1832808  -0.00 │   2    0      nan │
│                   coq-verdi │   50.45    50.23   0.44 │   219194151215    218227888550   0.44 │   326109537167    326094118752   0.00 │  829152   830344  -0.14 │   3    3     0.00 │
│        coq-mathcomp-algebra │   66.48    66.18   0.45 │   290425637041    289403511000   0.35 │   403004295290    403005464327  -0.00 │  563524   560924   0.46 │   0    0      nan │
│              coq-coquelicot │   35.89    35.63   0.73 │   154836575859    154261978538   0.37 │   202745921807    202660034176   0.04 │  753304   748808   0.60 │  58    2  2800.00 │
│                coq-coqprime │  187.23   185.74   0.80 │   818793119187    813094839040   0.70 │  1560838373057   1560905356513  -0.00 │  856088   831992   2.90 │   0    0      nan │
│            coq-math-classes │   96.99    96.10   0.93 │   422046340234    418722416668   0.79 │   591211810643    591180513166   0.01 │  496368   496460  -0.02 │   0    0      nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘

Nothing out of the ordinary.

[SkySkimmer]

@coqbot merge now