Bench automatic overlay system

[SkySkimmer]

No description provided.

[SkySkimmer]

first running a test bench with no overlays applying

[SkySkimmer]

and another bench with an overlay on elpi

[coqbot-app]

🏁 Bench results:

┌──────────────┬───────────────────────┬─────────────────────────────────────┬───────────────────────┐
│              │     user time [s]     │          CPU instructions           │ max resident mem [KB] │
│              │                       │                                     │                       │
│ package_name │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │  NEW     OLD    PDIFF │
├──────────────┼───────────────────────┼─────────────────────────────────────┼───────────────────────┤
│    rocq-core │   6.79    6.95  -2.30 │   41655734179    41664396503  -0.02 │ 443500  443808  -0.07 │
│  rocq-stdlib │ 436.11  439.59  -0.79 │ 1555583160060  1555559432920   0.00 │ 632444  629932   0.40 │
│ rocq-runtime │  76.39   76.38   0.01 │  550756429122   550686979674   0.01 │ 493876  494912  -0.21 │
│     coq-core │   2.90    2.69   7.81 │   18568602180    18567038309   0.01 │  91260   90856   0.44 │
└──────────────┴───────────────────────┴─────────────────────────────────────┴───────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                         TOP 25 SLOW DOWNS                                          │
│                                                                                                    │
│  OLD     NEW    DIFF    %DIFF    Ln              FILE                                              │
├────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   1.63   1.99  0.3574   21.88%   313  rocq-stdlib/theories/Strings/Byte.v.html                     │
│  0.164  0.434  0.2705  165.24%   592  rocq-stdlib/theories/MSets/MSetAVL.v.html                    │
│  0.132  0.380  0.2472  186.82%   658  rocq-stdlib/theories/Numbers/DecimalFacts.v.html             │
│  0.174  0.420  0.2461  141.55%   586  rocq-stdlib/theories/Strings/Byte.v.html                     │
│   1.09   1.33  0.2399   21.93%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                    │
│   1.08   1.31  0.2343   21.70%   702  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html         │
│  0.260  0.491  0.2308   88.74%    10  rocq-stdlib/theories/extraction/ExtrHaskellZNum.v.html       │
│  0.327  0.558  0.2305   70.40%   719  rocq-stdlib/theories/MSets/MSetRBT.v.html                    │
│  0.335  0.547  0.2122   63.37%    12  rocq-stdlib/theories/ZArith/Znumtheory.v.html                │
│  0.457  0.640  0.1825   39.90%   170  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html           │
│  0.278  0.458  0.1810   65.20%    15  rocq-stdlib/theories/micromega/ZifyInst.v.html               │
│  0.281  0.456  0.1742   61.91%   207  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html           │
│  0.376  0.547  0.1710   45.51%   637  rocq-stdlib/theories/MSets/MSetRBT.v.html                    │
│  0.348  0.515  0.1671   48.08%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                  │
│  0.465  0.630  0.1650   35.47%    83  rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html      │
│ 0.0651  0.228  0.1632  250.59%   580  rocq-stdlib/theories/MSets/MSetAVL.v.html                    │
│  0.138  0.294  0.1557  112.70%    11  rocq-stdlib/theories/Structures/EqualitiesFacts.v.html       │
│  0.337  0.492  0.1555   46.17%  1161  rocq-stdlib/theories/Strings/Byte.v.html                     │
│  0.317  0.468  0.1508   47.59%    73  rocq-stdlib/theories/Reals/Abstract/ConstructiveReals.v.html │
│  0.141  0.291  0.1497  106.18%    16  rocq-stdlib/theories/MSets/MSetWeakList.v.html               │
│  0.218  0.364  0.1455   66.61%   698  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html         │
│  0.146  0.290  0.1434   98.20%  1187  rocq-stdlib/theories/Strings/Byte.v.html                     │
│  0.183  0.326  0.1433   78.44%  1637  rocq-stdlib/theories/micromega/Tauto.v.html                  │
│  0.152  0.288  0.1359   89.25%    11  rocq-stdlib/theories/ZArith/Zmisc.v.html                     │
│  0.128  0.264  0.1359  105.76%   726  rocq-stdlib/theories/MSets/MSetList.v.html                   │
└────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────┐
│                                       TOP 25 SPEED UPS                                       │
│                                                                                              │
│  OLD    NEW    DIFF     %DIFF    Ln             FILE                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────┤
│ 0.909  0.434  -0.4748  -52.25%  2109  rocq-stdlib/theories/FSets/FMapFacts.v.html            │
│  1.73   1.26  -0.4683  -27.08%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html              │
│  22.1   21.8  -0.3395   -1.54%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html              │
│ 0.616  0.286  -0.3304  -53.63%    18  rocq-stdlib/theories/ZArith/Zeven.v.html               │
│ 0.725  0.424  -0.3008  -41.49%   141  rocq-stdlib/theories/Strings/Ascii.v.html              │
│ 0.598  0.306  -0.2915  -48.78%   484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html   │
│  1.27  0.996  -0.2769  -21.75%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html              │
│ 0.488  0.216  -0.2726  -55.81%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html         │
│ 0.620  0.363  -0.2567  -41.40%    19  rocq-stdlib/theories/ZArith/Zcompare.v.html            │
│ 0.505  0.273  -0.2319  -45.91%    11  rocq-stdlib/theories/ZArith/Wf_Z.v.html                │
│ 0.439  0.208  -0.2306  -52.58%   639  rocq-stdlib/theories/MSets/MSetAVL.v.html              │
│ 0.565  0.335  -0.2302  -40.73%    11  rocq-stdlib/theories/micromega/Zify.v.html             │
│ 0.513  0.286  -0.2263  -44.14%    17  rocq-stdlib/theories/micromega/QMicromega.v.html       │
│ 0.760  0.534  -0.2262  -29.77%   160  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html     │
│ 0.538  0.322  -0.2156  -40.08%    11  rocq-stdlib/theories/Sorting/PermutEq.v.html           │
│ 0.529  0.344  -0.1853  -35.00%     1  rocq-stdlib/theories/ZArith/ZNsatz.v.html              │
│ 0.359  0.179  -0.1797  -50.09%  1982  rocq-stdlib/theories/FSets/FMapFacts.v.html            │
│ 0.271  0.100  -0.1704  -62.91%   152  rocq-stdlib/theories/FSets/FSetProperties.v.html       │
│ 0.354  0.184  -0.1698  -47.93%   143  rocq-stdlib/theories/Strings/Ascii.v.html              │
│ 0.318  0.152  -0.1660  -52.17%   558  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html   │
│ 0.314  0.149  -0.1651  -52.51%   133  rocq-stdlib/theories/Strings/Ascii.v.html              │
│ 0.466  0.302  -0.1636  -35.13%    11  rocq-stdlib/theories/setoid_ring/Rings_Q.v.html        │
│ 0.497  0.338  -0.1584  -31.88%    10  rocq-stdlib/theories/micromega/ZArith_hints.v.html     │
│ 0.439  0.281  -0.1576  -35.93%    11  rocq-stdlib/theories/QArith/QOrderedType.v.html        │
│ 0.278  0.137  -0.1409  -50.62%   148  rocq-stdlib/theories/Structures/EqualitiesFacts.v.html │
└──────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

should work now