Bench: print size diff in vosize.log

[SkySkimmer]

No description provided.

[SkySkimmer]

rebased on #19014 for testing

[coqbot-app]

🏁 Bench results:

┌──────────────┬───────────────────────┬─────────────────────────────────────┬─────────────────────────────────────┬───────────────────────┐
│              │     user time [s]     │             CPU cycles              │          CPU instructions           │ max resident mem [KB] │
│              │                       │                                     │                                     │                       │
│ package_name │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │      NEW            OLD       PDIFF │  NEW     OLD    PDIFF │
├──────────────┼───────────────────────┼─────────────────────────────────────┼─────────────────────────────────────┼───────────────────────┤
│     coq-hott │ 159.84  160.46  -0.39 │  714474297160   716888070481  -0.34 │ 1131579476386  1139449555627  -0.69 │ 478868  478632   0.05 │
│   coq-stdlib │ 350.39  349.03   0.39 │ 1487198890954  1478891335100   0.56 │ 1259301391240  1258613079424   0.05 │ 715144  715688  -0.08 │
│     coq-core │ 128.37  127.69   0.53 │  502562106711   503283847469  -0.14 │  531927987133   531788768169   0.03 │ 458276  457656   0.14 │
└──────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────────────────┴───────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────┐
│                                   TOP 25 SLOW DOWNS                                    │
│                                                                                        │
│  OLD     NEW     DIFF    %DIFF   Ln           FILE                                     │
├────────────────────────────────────────────────────────────────────────────────────────┤
│ 2.3990  3.2550  0.8560   35.68%  487  coq-stdlib/Numbers/HexadecimalFacts.v.html       │
│ 1.0030  1.4420  0.4390   43.77%  854  coq-stdlib/FSets/FMapAVL.v.html                  │
│ 0.3920  0.6010  0.2090   53.32%  870  coq-stdlib/MSets/MSetRBT.v.html                  │
│ 0.5920  0.7750  0.1830   30.91%  160  coq-stdlib/Numbers/HexadecimalNat.v.html         │
│ 0.9730  1.1540  0.1810   18.60%  384  coq-stdlib/MSets/MSetAVL.v.html                  │
│ 0.1140  0.2740  0.1600  140.35%  240  coq-stdlib/Numbers/HexadecimalString.v.html      │
│ 0.2950  0.4460  0.1510   51.19%  313  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html │
│ 0.2260  0.3700  0.1440   63.72%   11  coq-stdlib/Floats/FloatOps.v.html                │
│ 0.3200  0.4430  0.1230   38.44%  705  coq-stdlib/Numbers/HexadecimalFacts.v.html       │
│ 0.1790  0.3020  0.1230   68.72%    1  coq-stdlib/micromega/ZifySint63.v.html           │
│ 0.5610  0.6830  0.1220   21.75%  422  coq-stdlib/MSets/MSetList.v.html                 │
│ 0.4500  0.5720  0.1220   27.11%   82  coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html    │
│ 0.1620  0.2750  0.1130   69.75%   13  coq-stdlib/extraction/ExtrOCamlInt63.v.html      │
│ 0.5970  0.7070  0.1100   18.43%  170  coq-stdlib/Numbers/HexadecimalNat.v.html         │
│ 0.2000  0.3090  0.1090   54.50%   14  coq-stdlib/Numbers/Cyclic/Int63/Ring63.v.html    │
│ 0.2160  0.3190  0.1030   47.69%   16  coq-stdlib/Numbers/HexadecimalNat.v.html         │
│ 0.5090  0.6120  0.1030   20.24%   14  coq-stdlib/MSets/MSetToFiniteSet.v.html          │
│ 0.2950  0.3910  0.0960   32.54%  861  coq-stdlib/FSets/FMapAVL.v.html                  │
│ 0.2130  0.3030  0.0900   42.25%   11  coq-stdlib/QArith/Qpower.v.html                  │
│ 0.3940  0.4810  0.0870   22.08%  637  coq-stdlib/MSets/MSetRBT.v.html                  │
│ 0.5530  0.6380  0.0850   15.37%  816  coq-stdlib/MSets/MSetRBT.v.html                  │
│ 0.0000  0.0840  0.0840     inf%  284  coq-stdlib/Numbers/DecimalPos.v.html             │
│ 0.1960  0.2790  0.0830   42.35%   11  coq-stdlib/Reals/AltSeries.v.html                │
│ 0.2880  0.3600  0.0720   25.00%  877  coq-stdlib/FSets/FMapAVL.v.html                  │
│ 0.1510  0.2210  0.0700   46.36%   11  coq-stdlib/QArith/QArith_base.v.html             │
└────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                          TOP 25 SPEED UPS                                           │
│                                                                                                     │
│  OLD     NEW     DIFF     %DIFF     Ln             FILE                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 0.6040  0.3240  -0.2800   -46.36%   868  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 1.0270  0.8270  -0.2000   -19.47%   467  coq-stdlib/Numbers/DecimalFacts.v.html                     │
│ 0.4120  0.2730  -0.1390   -33.74%   387  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.2660  0.1490  -0.1170   -43.98%  1846  coq-stdlib/FSets/FMapAVL.v.html                            │
│ 0.3240  0.2080  -0.1160   -35.80%   338  coq-hott/theories/Homotopy/CayleyDickson.v.html            │
│ 1.5120  1.3990  -0.1130    -7.47%   691  coq-hott/theories/Pointed/Core.v.html                      │
│ 0.1480  0.0390  -0.1090   -73.65%   353  coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html           │
│ 0.3840  0.2890  -0.0950   -24.74%   719  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.1290  0.0370  -0.0920   -71.32%   345  coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html           │
│ 0.3190  0.2290  -0.0900   -28.21%   301  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.3800  0.2910  -0.0890   -23.42%   596  coq-stdlib/Strings/Byte.v.html                             │
│ 0.1320  0.0500  -0.0820   -62.12%   356  coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html           │
│ 0.0810  0.0000  -0.0810  -100.00%   285  coq-stdlib/Numbers/DecimalPos.v.html                       │
│ 0.2330  0.1540  -0.0790   -33.91%   391  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.2880  0.2100  -0.0780   -27.08%    11  coq-stdlib/Reals/Alembert.v.html                           │
│ 0.2040  0.1270  -0.0770   -37.75%  1603  coq-stdlib/micromega/Tauto.v.html                          │
│ 0.1500  0.0750  -0.0750   -50.00%  1636  coq-stdlib/micromega/Tauto.v.html                          │
│ 0.1820  0.1080  -0.0740   -40.66%    25  coq-stdlib/Logic/WKL.v.html                                │
│ 0.2610  0.1880  -0.0730   -27.97%    12  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html     │
│ 0.2440  0.1770  -0.0670   -27.46%   351  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │
│ 0.3980  0.3320  -0.0660   -16.58%   474  coq-stdlib/MSets/MSetWeakList.v.html                       │
│ 0.2030  0.1370  -0.0660   -32.51%    11  coq-stdlib/ZArith/Zcomplements.v.html                      │
│ 0.7840  0.7190  -0.0650    -8.29%   597  coq-stdlib/Strings/Byte.v.html                             │
│ 0.4430  0.3780  -0.0650   -14.67%   205  coq-hott/theories/Spaces/Spheres.v.html                    │
│ 0.2680  0.2070  -0.0610   -22.76%  1045  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

It works

[ppedrot]

I'm not really convinced this is useful in practice since we still have to sort the resulting file, but since it cannot hurt either...

[ppedrot]

@coqbot merge now