Add a PUSHACCMANY opcode.

[silene]

Especially for symbols defined inside sections, callee functions might be invoked with the exact same arguments as caller functions. A similar situation happens with recursive functions that share most of their arguments across calls. This new opcode replaces a sequence of repeated PUSH; ACC opcodes with constant indices.

[silene]

@coqbot run full ci

[silene]

@coqbot bench

[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-core │  127.97   129.49  -1.17 │   503273406849    497433979138   1.17 │   530195150907    530109271892   0.02 │  456808   456532   0.06 │
│                          coq-stdlib │  360.44   360.75  -0.09 │  1529115862156   1533990694316  -0.32 │  1286663054683   1286469110691   0.02 │  720724   720596   0.02 │
│                        coq-rewriter │  386.73   386.97  -0.06 │  1758058465792   1759524938319  -0.08 │  2946424661989   2946326376353   0.00 │ 1476020  1477596  -0.11 │
│                    coq-math-classes │   85.60    85.64  -0.05 │   384387487554    384478189173  -0.02 │   534870750167    534967925151  -0.02 │  502540   503188  -0.13 │
│         coq-rewriter-perf-SuperFast │  784.91   785.19  -0.04 │  3569671169354   3568363818020   0.04 │  6184690936286   6184108601295   0.01 │ 1570516  1572700  -0.14 │
│                        coq-coqprime │   47.93    47.91   0.04 │   214858626259    215006296867  -0.07 │   330962142425    330945296178   0.01 │  785080   785012   0.01 │
│        coq-fiat-crypto-with-bedrock │ 6180.09  6176.41   0.06 │ 28156892780250  28140987209002   0.06 │ 50308713143646  50307574686353   0.00 │ 3246184  3245992   0.01 │
│                             coq-vst │  875.99   874.72   0.15 │  3983024899121   3978396655052   0.12 │  6739099263337   6738779855319   0.00 │ 2147248  2147088   0.01 │
│                        coq-compcert │  279.63   279.20   0.15 │  1266560790891   1262427963420   0.33 │  1934955926431   1934713872939   0.01 │ 1118180  1117120   0.09 │
│                        coq-bedrock2 │  360.28   359.61   0.19 │  1642392285139   1639722189741   0.16 │  3095454451137   3095576477815  -0.00 │  861440   855856   0.65 │
│                         coq-coqutil │   41.77    41.68   0.22 │   184275104265    183992625626   0.15 │   267997178012    267902401461   0.04 │  561628   561620   0.00 │
│                       coq-fiat-core │   58.68    58.55   0.22 │   244500457798    243762775137   0.30 │   363472377339    363473075620  -0.00 │  485276   485064   0.04 │
│                            coq-hott │  157.39   157.02   0.24 │   702631056327    701794108877   0.12 │  1117058698331   1117518284808  -0.04 │  548632   550948  -0.42 │
│                                 coq │  714.56   712.79   0.25 │  3008684716638   3005576629777   0.10 │  5378664895608   5382227653441  -0.07 │ 2716984  2484372   9.36 │
│                         coq-bignums │   29.42    29.34   0.27 │   133843679308    132768095255   0.81 │   192019226174    192034203082  -0.01 │  472440   474688  -0.47 │
│          coq-performance-tests-lite │  704.19   701.40   0.40 │  3178345367910   3167880106062   0.33 │  5634002524038   5633230946571   0.01 │ 2265992  2264616   0.06 │
│                      coq-verdi-raft │  582.35   579.79   0.44 │  2649966074166   2638365684038   0.44 │  4165153151262   4164996454310   0.00 │  850400   850296   0.01 │
│                   coq-iris-examples │  467.63   465.44   0.47 │  2126984403550   2114719022013   0.58 │  3270526113072   3270600797717  -0.00 │ 1111928  1112364  -0.04 │
│                         coq-unimath │ 2445.48  2433.31   0.50 │ 11139919356924  11082252197282   0.52 │ 21916076011532  21916329016847  -0.00 │ 1254392  1254292   0.01 │
│               coq-engine-bench-lite │  156.69   155.71   0.63 │   663772082236    659854254801   0.59 │  1228063585855   1225479867302   0.21 │ 1234876  1236708  -0.15 │
│                            coq-corn │  715.28   710.51   0.67 │  3250557881247   3228391550746   0.69 │  5068380071012   5068044631091   0.01 │  758344   756928   0.19 │
│                           coq-color │  250.45   248.59   0.75 │  1127110954148   1117837863443   0.83 │  1628453187940   1628331271968   0.01 │ 1205516  1205128   0.03 │
│                    coq-fiat-parsers │  310.85   307.91   0.95 │  1384999781698   1375178195891   0.71 │  2426455003130   2424148090500   0.10 │ 2395752  2393880   0.08 │
│                           coq-verdi │   48.79    48.27   1.08 │   219257702435    217894405720   0.63 │   339580292906    339561652663   0.01 │  531820   531508   0.06 │
│ coq-neural-net-interp-computed-lite │  303.74   298.27   1.83 │  1386325725412   1363293092343   1.69 │  3427452458403   3423545749638   0.11 │ 1124212  1126008  -0.16 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-equations

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-template (dependency coq-equations failed)
coq-metacoq-pcuic (dependency coq-equations failed)
coq-metacoq-safechecker (dependency coq-equations failed)
coq-metacoq-erasure (dependency coq-equations failed)
coq-metacoq-translations (dependency coq-equations failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF    %DIFF    Ln                     FILE                                                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 257.2670  262.3030  5.0360    1.96%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html    │
│ 215.7170  218.9060  3.1890    1.48%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                              │
│  62.4220   63.7430  1.3210    2.12%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html    │
│  97.8660   99.0440  1.1780    1.20%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                      │
│  94.9310   95.7570  0.8260    0.87%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  95.0650   95.8100  0.7450    0.78%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  39.2960   40.0260  0.7300    1.86%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html        │
│  21.9310   22.5630  0.6320    2.88%  2061  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  66.6740   67.1990  0.5250    0.79%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
│  50.5460   51.0690  0.5230    1.03%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  26.4290   26.9460  0.5170    1.96%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html             │
│  39.1010   39.6150  0.5140    1.31%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                      │
│  19.7000   20.2000  0.5000    2.54%   819  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                          │
│   7.0390    7.5050  0.4660    6.62%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html   │
│  48.2050   48.6540  0.4490    0.93%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│ 154.9920  155.4060  0.4140    0.27%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                    │
│  22.9170   23.3230  0.4060    1.77%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  46.1790   46.5800  0.4010    0.87%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                        │
│  38.4070   38.7860  0.3790    0.99%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                   │
│  33.0780   33.4310  0.3530    1.07%    97  coq-vst/veric/binop_lemmas5.v.html                                                               │
│  46.2160   46.5650  0.3490    0.76%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html     │
│   0.3300    0.6780  0.3480  105.45%   868  coq-stdlib/MSets/MSetRBT.v.html                                                                  │
│  73.2190   73.5490  0.3300    0.45%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                             │
│   7.8720    8.1780  0.3060    3.89%  1225  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html                      │
│  36.6950   36.9970  0.3020    0.82%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF     %DIFF   Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 184.5380  182.1100  -2.4280   -1.32%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 132.1320  130.6580  -1.4740   -1.12%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  19.5880   18.1450  -1.4430   -7.37%  820  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   3.7110    2.8700  -0.8410  -22.66%  490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│  30.8600   30.0360  -0.8240   -2.67%  194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│  12.2330   11.4850  -0.7480   -6.11%  194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  31.6550   30.9430  -0.7120   -2.25%  147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│  26.3580   25.6750  -0.6830   -2.59%   22  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  26.3460   25.6830  -0.6630   -2.52%   17  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  29.5230   28.9880  -0.5350   -1.81%   79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html       │
│  99.7340   99.2310  -0.5030   -0.50%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  15.2330   14.7470  -0.4860   -3.19%   99  coq-fiat-crypto-with-bedrock/src/Spec/Curve25519.v.html                                                 │
│  15.5580   15.0740  -0.4840   -3.11%   33  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery25519.v.html                                   │
│  20.5800   20.1190  -0.4610   -2.24%   25  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  14.0260   13.5830  -0.4430   -3.16%  850  coq-unimath/UniMath/CategoryTheory/Profunctors/Transformation.v.html                                    │
│  15.8960   15.5070  -0.3890   -2.45%   25  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery25519.v.html                                   │
│  47.8180   47.4540  -0.3640   -0.76%  558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│  35.7740   35.4300  -0.3440   -0.96%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│   1.3270    1.0060  -0.3210  -24.19%  854  coq-stdlib/FSets/FMapAVL.v.html                                                                         │
│  63.5920   63.2820  -0.3100   -0.49%  609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  13.6600   13.3880  -0.2720   -1.99%   12  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  17.6490   17.3840  -0.2650   -1.50%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                       │
│   4.4610    4.2000  -0.2610   -5.85%  199  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                             │
│   7.6610    7.4300  -0.2310   -3.02%   57  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery25519.v.html                                   │
│  10.6210   10.4090  -0.2120   -2.00%  326  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[silene]

The bench unfortunately failed to complete due to concurrent commits in the tested repositories, but it still gives an idea. As with #18964, the overall gain is minor, but specific developments nonetheless benefit heavily from it, e.g., coq-hott (18% reduction of the size of Products.vo), coq-corn (16% for ACarith.vo).

One I was not expecting is coq-verdi-raft (20% reduction for RaftState.vo), but it makes sense. Indeed, it implements the update pattern from OCaml (i.e., { record with field = value }) for a large record with lots of section arguments, hence a naturally quadratic term, since they use non-primitive (I guess?) projections.

[ppedrot]

Let's retry @coqbot bench

[SkySkimmer]

Probably should rebase before retrying

[ppedrot]

Doesn't the bench script perform an auto-merge with master?

[SkySkimmer]

no

[ppedrot]

@coqbot bench

[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-neural-net-interp-computed-lite │  297.14   301.10  -1.32 │  1355478911038   1373661571802  -1.32 │  3427916862049   3616185929296  -5.21 │ 1126268  1126284  -0.00 │
│                      coq-coquelicot │   39.29    39.72  -1.08 │   175168343359    175625035623  -0.26 │   248616906142    248634109450  -0.01 │  851700   855044  -0.39 │
│          coq-performance-tests-lite │  714.33   718.04  -0.52 │  3193267237738   3212391251224  -0.60 │  5635881939009   5684160686282  -0.85 │ 2264864  2265780  -0.04 │
│             coq-metacoq-safechecker │  421.81   423.84  -0.48 │  1922511204277   1930470656829  -0.41 │  3197754969402   3198315573449  -0.02 │ 2064712  2068548  -0.19 │
│                    coq-fiat-parsers │  313.16   314.51  -0.43 │  1385814886140   1389778466360  -0.29 │  2433444241161   2469669717714  -1.47 │ 2396008  2399948  -0.16 │
│                      coq-verdi-raft │  582.33   584.44  -0.36 │  2642112126788   2648949941013  -0.26 │  4159840642216   4159862941264  -0.00 │  840296   840096   0.02 │
│                   coq-iris-examples │  467.11   468.67  -0.33 │  2115465142727   2120300796295  -0.23 │  3276427498493   3276512997907  -0.00 │ 1111676  1113928  -0.20 │
│                   coq-metacoq-pcuic │  989.37   992.49  -0.31 │  4413292480441   4423986453159  -0.24 │  6475322685641   6476523603388  -0.02 │ 2682164  2683544  -0.05 │
│        coq-fiat-crypto-with-bedrock │ 6221.68  6237.47  -0.25 │ 28171352622042  28245039252124  -0.26 │ 50403990596794  51217808255610  -1.59 │ 3245960  3245996  -0.00 │
│                 coq-metacoq-erasure │  504.72   505.93  -0.24 │  2284027088833   2290218914823  -0.27 │  3586882595017   3586889915303  -0.00 │ 2161176  2155956   0.24 │
│                             coq-vst │  880.03   882.10  -0.23 │  3974958708501   3984751980285  -0.25 │  6746378555745   6746257124722   0.00 │ 2147344  2148412  -0.05 │
│                         coq-coqutil │   42.75    42.85  -0.23 │   187763986220    187765620900  -0.00 │   270403670681    270464918720  -0.02 │  561744   560848   0.16 │
│            coq-metacoq-translations │   17.12    17.15  -0.17 │    75385651627     75359351756   0.03 │   124794854106    124792026414   0.00 │  848084   846344   0.21 │
│                    coq-math-classes │   86.11    86.26  -0.17 │   384817508557    384797007845   0.01 │   535997604266    535969080919   0.01 │  504140   503688   0.09 │
│                           coq-verdi │   49.21    49.29  -0.16 │   220214139656    220439786328  -0.10 │   340650605962    340753875302  -0.03 │  532012   532084  -0.01 │
│         coq-rewriter-perf-SuperFast │  794.68   795.77  -0.14 │  3549919719363   3551348329046  -0.04 │  6200746892528   6254500629087  -0.86 │ 1572740  1570060   0.17 │
│                         coq-bignums │   29.52    29.55  -0.10 │   133425652549    133455125221  -0.02 │   192021186077    192009352019   0.01 │  472008   472212  -0.04 │
│                        coq-coqprime │   48.19    48.22  -0.06 │   215774624417    215538832535   0.11 │   332234707788    334063002261  -0.55 │  784536   782944   0.20 │
│                        coq-rewriter │  391.53   391.66  -0.03 │  1764046712516   1764775601079  -0.04 │  2949810832830   2990291726532  -1.35 │ 1477880  1473736   0.28 │
│                       coq-fiat-core │   60.07    60.05   0.03 │   248368639559    248661973805  -0.12 │   367892361858    367873830397   0.01 │  476292   473820   0.52 │
│                        coq-bedrock2 │  361.71   361.43   0.08 │  1632784089280   1630703193073   0.13 │  3099005273994   3102524421288  -0.11 │  857540   857568  -0.00 │
│                            coq-core │  132.38   132.27   0.08 │   493329665602    492743326192   0.12 │   531563228009    531576974510  -0.00 │  457744   457056   0.15 │
│                        coq-compcert │  281.80   281.49   0.11 │  1264874130428   1263994422034   0.07 │  1934231940628   1942369201606  -0.42 │ 1116668  1117688  -0.09 │
│                       coq-fourcolor │ 1369.74  1366.71   0.22 │  6228578523543   6214995855489   0.22 │ 12189924602116  12916793195426  -5.63 │ 2128800  2128848  -0.00 │
│                         coq-unimath │ 2471.46  2465.10   0.26 │ 11201323616343  11172279666874   0.26 │ 22197164802501  22197615963795  -0.00 │ 1255924  1254212   0.14 │
│                       coq-equations │    7.70     7.68   0.26 │    31232732801     31061081570   0.55 │    50795503435     50802935971  -0.01 │  386224   388176  -0.50 │
│               coq-engine-bench-lite │  157.78   157.37   0.26 │   661709759365    660627941181   0.16 │  1226051664650   1226403046711  -0.03 │ 1234872  1235056  -0.01 │
│                            coq-corn │  716.68   714.64   0.29 │  3240918260865   3230590015234   0.32 │  5070792756706   5071974975494  -0.02 │  764872   765484  -0.08 │
│                coq-metacoq-template │  151.87   151.39   0.32 │   667878184834    666509203420   0.21 │  1045740331178   1045673948138   0.01 │ 1480932  1485568  -0.31 │
│                          coq-stdlib │  366.21   364.84   0.38 │  1515601518253   1512147605432   0.23 │  1286677747117   1286714897052  -0.00 │  717424   714764   0.37 │
│                 coq-category-theory │  694.77   691.66   0.45 │  3146676001007   3129586102763   0.55 │  5255375132717   5257618081303  -0.04 │  956680   955732   0.10 │
│                            coq-hott │  161.77   161.03   0.46 │   716102408313    712875077541   0.45 │  1141279401888   1141249152510   0.00 │  478456   480944  -0.52 │
│                      coq-test-suite │  705.51   702.11   0.48 │  2997674211138   2977734693418   0.67 │  5351127068168   5383089031174  -0.59 │ 2461072  2461444  -0.02 │
│               coq-mathcomp-solvable │  118.72   118.03   0.58 │   540395690267    537675375803   0.51 │   859177329342    859343472728  -0.02 │  879512   881352  -0.21 │
│              coq-mathcomp-character │  109.65   108.95   0.64 │   498197949721    495357987941   0.57 │   793252119122    793236380994   0.00 │ 1154832  1152664   0.19 │
│                  coq-mathcomp-field │  144.29   143.29   0.70 │   651151998751    645941182476   0.81 │  1077202846572   1077241433570  -0.00 │ 1449424  1448364   0.07 │
│                           coq-color │  253.95   252.06   0.75 │  1129908478124   1123797558877   0.54 │  1634087072227   1634150741144  -0.00 │ 1206548  1205356   0.10 │
│              coq-mathcomp-odd-order │  800.55   793.90   0.84 │  3654251448633   3622375669635   0.88 │  6096384048460   6096553132920  -0.00 │ 1638664  1640692  -0.12 │
│                coq-mathcomp-algebra │  262.83   260.52   0.89 │  1186961180458   1176859556463   0.86 │  2003848906268   2003844485152   0.00 │ 1293148  1294256  -0.09 │
│              coq-mathcomp-ssreflect │  223.88   221.67   1.00 │  1008970965543    999545833989   0.94 │  1673769937142   1673643209681   0.01 │ 1743384  1737004   0.37 │
│               coq-mathcomp-fingroup │   30.93    30.60   1.08 │   139988029265    138319350090   1.21 │   208136197585    208084853588   0.02 │  563880   565840  -0.35 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  83.6910   85.7480  2.0570   2.46%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│  69.6480   71.6450  1.9970   2.87%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│  47.5950   49.2650  1.6700   3.51%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  48.0360   49.2130  1.1770   2.45%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                   │
│  96.4730   97.3780  0.9050   0.94%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│  37.3300   38.1210  0.7910   2.12%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                  │
│  81.4210   82.1590  0.7380   0.91%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│   1.6360    2.2610  0.6250  38.20%   196  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                          │
│  46.6410   47.2310  0.5900   1.26%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                         │
│  17.0160   17.5630  0.5470   3.21%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                 │
│  33.5840   33.9440  0.3600   1.07%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│  28.6430   28.9980  0.3550   1.24%    12  coq-fourcolor/theories/job323to383.v.html                                                         │
│  26.0090   26.3590  0.3500   1.35%    12  coq-fourcolor/theories/job531to534.v.html                                                         │
│  25.1310   25.4460  0.3150   1.25%    12  coq-fourcolor/theories/job466to485.v.html                                                         │
│  25.9040   26.2050  0.3010   1.16%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                             │
│   0.3670    0.6670  0.3000  81.74%  2108  coq-stdlib/FSets/FMapFacts.v.html                                                                 │
│  25.2210   25.5180  0.2970   1.18%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                │
│   0.5890    0.8820  0.2930  49.75%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                            │
│  36.7420   37.0340  0.2920   0.79%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│  19.6860   19.9740  0.2880   1.46%  2061  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│ 101.5340  101.8180  0.2840   0.28%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│   1.3090    1.5850  0.2760  21.08%   596  coq-stdlib/Strings/Byte.v.html                                                                    │
│  29.3500   29.6120  0.2620   0.89%    12  coq-fourcolor/theories/job001to106.v.html                                                         │
│  21.7530   21.9970  0.2440   1.12%    12  coq-fourcolor/theories/job384to398.v.html                                                         │
│  15.2210   15.4620  0.2410   1.58%  1382  coq-rewriter-perf-SuperFast/src/Rewriter/Language/Wf.v.html                                       │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 243.0660  235.9220  -7.1440   -2.94%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│ 259.5740  255.4060  -4.1680   -1.61%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│ 138.5250  134.8720  -3.6530   -2.64%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│ 258.2840  255.7030  -2.5810   -1.00%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                         │
│ 182.7430  181.1630  -1.5800   -0.86%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  41.0060   39.6710  -1.3350   -3.26%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html               │
│  63.2610   61.9290  -1.3320   -2.11%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  39.9660   38.6800  -1.2860   -3.22%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                          │
│  27.0290   25.8800  -1.1490   -4.25%    17  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  27.0150   25.8760  -1.1390   -4.22%    22  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  40.9240   39.8220  -1.1020   -2.69%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                              │
│  96.4030   95.3500  -1.0530   -1.09%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│ 155.2520  154.2390  -1.0130   -0.65%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  42.3620   41.4040  -0.9580   -2.26%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  96.2690   95.3660  -0.9030   -0.94%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  21.1630   20.2770  -0.8860   -4.19%    25  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│   3.7380    2.8690  -0.8690  -23.25%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│  27.1670   26.4040  -0.7630   -2.81%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  12.4590   11.7200  -0.7390   -5.93%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  28.8410   28.1400  -0.7010   -2.43%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  15.5190   14.8370  -0.6820   -4.39%    99  coq-fiat-crypto-with-bedrock/src/Spec/Curve25519.v.html                                                 │
│   3.0560    2.4010  -0.6550  -21.43%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                              │
│ 219.5410  218.9330  -0.6080   -0.28%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│  14.0390   13.4580  -0.5810   -4.14%    12  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  15.7550   15.1830  -0.5720   -3.63%    33  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery25519.v.html                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[silene]

After the merge of #18968, the benefits of this pull request increase notably, at least for coq-hott. For example, the size reduction of Products.vo now reaches 32% (instead of 18%), while it is 20% for DisplayedEquiv.vo (instead of 13%).

The .vo size reduction over the whole test-suite is 0.5%, with coq-hott, coq-unimath, and coq-corn being the biggest winners. Most developments do not see a single byte of difference.

@coqbot run full ci

[silene]

@coqbot run full ci

[ppedrot]

@silene could you rebase on master? I'd like to see the effects of this PR after the merge of #19014.

[silene]

@coqbot bench

[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-equations │   11.86    12.12  -2.15 │    50132660845     50439166101  -0.61 │    79531454213     79618484526  -0.11 │  424740   425576  -0.20 │
│               coq-mathcomp-fingroup │   30.21    30.63  -1.37 │   137463474701    138613996978  -0.83 │   207639324042    207657132990  -0.01 │  568228   568628  -0.07 │
│              coq-mathcomp-character │  108.68   110.19  -1.37 │   494066056541    501194013532  -1.42 │   790177533828    790174256944   0.00 │ 1128696  1128732  -0.00 │
│ coq-neural-net-interp-computed-lite │  259.10   262.58  -1.33 │  1180575927283   1196589564731  -1.34 │  3039547372618   3208059216564  -5.25 │ 1113076  1112880   0.02 │
│              coq-mathcomp-odd-order │  784.98   793.82  -1.11 │  3582845387319   3624024751267  -1.14 │  6077683009387   6077874447463  -0.00 │ 1665428  1663036   0.14 │
│                  coq-mathcomp-field │  143.02   144.09  -0.74 │   645083959477    650363678458  -0.81 │  1073450039088   1073448159011   0.00 │ 1438276  1434644   0.25 │
│            coq-metacoq-translations │   16.92    17.03  -0.65 │    74673315425     74924695813  -0.34 │   124438088210    124439083576  -0.00 │  843156   843924  -0.09 │
│                   coq-metacoq-pcuic │  988.82   994.81  -0.60 │  4411310293017   4435202779024  -0.54 │  6465531174938   6467029825751  -0.02 │ 2679556  2678924   0.02 │
│                           coq-color │  250.95   252.42  -0.58 │  1121592767618   1126230020824  -0.41 │  1632324633884   1632480408375  -0.01 │ 1170496  1165044   0.47 │
│                            coq-corn │  714.96   718.90  -0.55 │  3233278070326   3252330130667  -0.59 │  5074811678887   5075852440411  -0.02 │  785604   789068  -0.44 │
│                       coq-fourcolor │ 1400.88  1408.31  -0.53 │  6372519425446   6408687275659  -0.56 │ 12751018385994  13505982826121  -5.59 │ 2137812  2137796   0.00 │
│                      coq-coquelicot │   39.75    39.93  -0.45 │   175956842225    176354157117  -0.23 │   249028317604    248969393428   0.02 │  857008   852260   0.56 │
│              coq-mathcomp-ssreflect │  222.74   223.73  -0.44 │  1004199874678   1008344285602  -0.41 │  1676143141307   1676169232990  -0.00 │ 1714772  1720660  -0.34 │
│                   coq-iris-examples │  468.08   470.06  -0.42 │  2119520250908   2126869490223  -0.35 │  3277482883205   3277647109595  -0.01 │ 1116024  1115776   0.02 │
│                coq-mathcomp-algebra │  260.45   261.46  -0.39 │  1177640623796   1182024886278  -0.37 │  1999229196905   1999241092609  -0.00 │ 1337212  1337736  -0.04 │
│                        coq-rewriter │  389.07   390.55  -0.38 │  1754070681636   1762843398124  -0.50 │  2934920454327   2975136312031  -1.35 │ 1479968  1477528   0.17 │
│          coq-performance-tests-lite │  711.57   714.26  -0.38 │  3185117550505   3197414548081  -0.38 │  5637954220678   5687140120106  -0.86 │ 2275680  2274988   0.03 │
│                        coq-compcert │  281.46   282.49  -0.36 │  1263004823664   1267116165188  -0.32 │  1931757441032   1939648914840  -0.41 │ 1137024  1137380  -0.03 │
│                      coq-verdi-raft │  581.59   583.66  -0.35 │  2639560267510   2649528775264  -0.38 │  4161062467200   4161119581048  -0.00 │  848140   848132   0.00 │
│                 coq-metacoq-erasure │  539.66   541.26  -0.30 │  2443827783666   2451049304941  -0.29 │  3834048264855   3834190238324  -0.00 │ 2144772  2145372  -0.03 │
│        coq-fiat-crypto-with-bedrock │ 5965.46  5982.48  -0.28 │ 27003007496479  27075687571366  -0.27 │ 48049761244263  48701888224173  -1.34 │ 3245948  3245872   0.00 │
│               coq-mathcomp-solvable │  118.26   118.55  -0.24 │   538068669455    540345272840  -0.42 │   856079519077    856246607524  -0.02 │  883904   882932   0.11 │
│                            coq-hott │  162.03   162.42  -0.24 │   715961363222    717345857240  -0.19 │  1142974666533   1142748705258   0.02 │  471928   474192  -0.48 │
│                    coq-fiat-parsers │  308.07   308.79  -0.23 │  1363989191312   1368940419734  -0.36 │  2398927047716   2434312585952  -1.45 │ 2464012  2461236   0.11 │
│                        coq-coqprime │   48.36    48.46  -0.21 │   215795108230    216089624553  -0.14 │   332892328791    334653940949  -0.53 │  784492   782624   0.24 │
│                         coq-coqutil │   42.43    42.49  -0.14 │   186297507091    186300996005  -0.00 │   270864122616    270983810188  -0.04 │  561148   561508  -0.06 │
│                         coq-unimath │ 2585.00  2587.78  -0.11 │ 11711590325969  11712825902574  -0.01 │ 23090310046702  23090260587367   0.00 │ 1273560  1274824  -0.10 │
│                          coq-stdlib │  352.04   352.41  -0.10 │  1474224407224   1473615014913   0.04 │  1257448755764   1257481091987  -0.00 │  714336   715236  -0.13 │
│                coq-metacoq-template │  151.52   151.52   0.00 │   665484769105    666563396997  -0.16 │  1045148754639   1045172638798  -0.00 │ 1510312  1504852   0.36 │
│               coq-engine-bench-lite │  158.06   157.91   0.09 │   662366499647    662501125184  -0.02 │  1228545810870   1223214343784   0.44 │ 1228304  1228104   0.02 │
│                             coq-vst │  881.20   880.27   0.11 │  3985271426670   3982115044309   0.08 │  6737272119182   6737374413799  -0.00 │ 2210724  2211668  -0.04 │
│         coq-rewriter-perf-SuperFast │  794.92   794.05   0.11 │  3552285919167   3550839404193   0.04 │  6171974451366   6225565472853  -0.86 │ 1578620  1578820  -0.01 │
│                        coq-bedrock2 │  364.03   363.42   0.17 │  1641768218459   1640723082510   0.06 │  3105949314696   3109546890591  -0.12 │  862020   862344  -0.04 │
│             coq-metacoq-safechecker │  421.83   420.91   0.22 │  1923330790667   1918767366893   0.24 │  3171843256989   3172580645014  -0.02 │ 2023852  2023956  -0.01 │
│                            coq-core │  130.31   129.84   0.36 │   501394239367    499890832657   0.30 │   532005638576    531770274428   0.04 │  458252   458184   0.01 │
│                       coq-fiat-core │   59.62    59.38   0.40 │   245408629460    245452253332  -0.02 │   368787759971    368815819842  -0.01 │  485104   484248   0.18 │
│                           coq-verdi │   49.21    48.98   0.47 │   220272026016    219107178286   0.53 │   340708198707    340669389999   0.01 │  529276   527960   0.25 │
│                    coq-math-classes │   86.24    85.77   0.55 │   384746525634    383784066300   0.25 │   536749223571    536779716356  -0.01 │  504768   504084   0.14 │
│                         coq-bignums │   29.82    29.63   0.64 │   134579509606    133398270136   0.89 │   192216775670    192229562617  -0.01 │  472580   470352   0.47 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-category-theory

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF    %DIFF    Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  62.6290   64.0820  1.4530    2.32%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│ 154.8970  156.2060  1.3090    0.85%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  81.5800   82.4580  0.8780    1.08%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  11.8630   12.5870  0.7240    6.10%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  49.0720   49.7950  0.7230    1.47%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│  65.5030   66.2170  0.7140    1.09%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  17.4650   18.1480  0.6830    3.91%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
│ 180.6150  181.2360  0.6210    0.34%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   6.9670    7.5610  0.5940    8.53%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html      │
│   2.3900    2.9280  0.5380   22.51%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                              │
│  62.1620   62.6360  0.4740    0.76%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│   5.5290    5.9650  0.4360    7.89%    19  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html                              │
│   0.3160    0.6370  0.3210  101.58%   870  coq-stdlib/MSets/MSetRBT.v.html                                                                         │
│  16.8450   17.1430  0.2980    1.77%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html                                        │
│  34.3380   34.6130  0.2750    0.80%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│   4.3560    4.6120  0.2560    5.88%   199  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                             │
│  49.0640   49.3200  0.2560    0.52%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│  33.8740   34.1270  0.2530    0.75%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  44.7060   44.9580  0.2520    0.56%   827  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│   0.6620    0.8990  0.2370   35.80%   813  coq-stdlib/MSets/MSetRBT.v.html                                                                         │
│   7.2390    7.4720  0.2330    3.22%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html          │
│  29.0270   29.2520  0.2250    0.78%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                      │
│   0.5280    0.7500  0.2220   42.05%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                                                │
│   8.2310    8.4420  0.2110    2.56%   900  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                            │
│  29.0320   29.2260  0.1940    0.67%    79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                             │
│                                                                                                                                          │
│   OLD       NEW      DIFF    %DIFF    Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 242.1150  236.0070  -6.1080  -2.52%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│ 220.9590  217.1980  -3.7610  -1.70%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  83.6860   80.4870  -3.1990  -3.82%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                             │
│ 138.8370  135.7170  -3.1200  -2.25%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│ 221.3040  218.3740  -2.9300  -1.32%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                           │
│  69.2010   66.8900  -2.3110  -3.34%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                             │
│ 259.2140  257.1350  -2.0790  -0.80%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                               │
│  40.9340   39.6640  -1.2700  -3.10%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html     │
│  40.7890   39.6940  -1.0950  -2.68%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│  39.8590   39.2150  -0.6440  -1.62%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                │
│  17.3180   16.7010  -0.6170  -3.56%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│  37.3200   36.7450  -0.5750  -1.54%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│  96.8010   96.2600  -0.5410  -0.56%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  33.7840   33.2590  -0.5250  -1.55%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│  29.3790   28.8770  -0.5020  -1.71%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html          │
│  25.2880   24.7860  -0.5020  -1.99%    12  coq-fourcolor/theories/job503to506.v.html                                                     │
│  11.5040   11.0280  -0.4760  -4.14%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                        │
│  29.9730   29.5700  -0.4030  -1.34%    12  coq-fourcolor/theories/job323to383.v.html                                                     │
│  17.4840   17.0900  -0.3940  -2.25%   474  coq-metacoq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html                │
│   3.6970    3.3710  -0.3260  -8.82%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                    │
│  25.5770   25.2560  -0.3210  -1.26%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│  47.2190   46.8990  -0.3200  -0.68%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                     │
│  29.2370   28.9180  -0.3190  -1.09%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
│  26.3120   25.9940  -0.3180  -1.21%    12  coq-fourcolor/theories/job466to485.v.html                                                     │
│  27.6300   27.3140  -0.3160  -1.14%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

Doesn't seem to be very useful now. Leaderboard:

coq-metacoq-pcuic/./pcuic/theories/PCUICParallelReductionConfluence.vo 3371169 3334915 36254 (-1%)
coq-hott/./theories/Colimits/GraphQuotient.vo 595317 555941 39376 (-7%)
coq-corn/./reals/faster/ARArith.vo 503787 460949 42838 (-9%)
coq-metacoq-safechecker/./safechecker/theories/PCUICSafeRetyping.vo 3493744 3445252 48492 (-1%)
coq-hott/./theories/WildCat/DisplayedEquiv.vo 991217 937465 53752 (-5%)
coq-fiat-crypto-with-bedrock/./src/Util/FsatzAutoLemmas.vo 975316 886357 88959 (-9%)
coq-hott/./theories/WildCat/Monoidal.vo 1860169 1764618 95551 (-5%)
coq-hott/./theories/WildCat/Products.vo 4393617 4262042 131575 (-3%)
coq-metacoq-safechecker/./safechecker/theories/PCUICSafeConversion.vo 8255051 8069677 185374 (-2%)
coq-metacoq-safechecker/./safechecker/theories/PCUICSafeReduce.vo 7838949 7546806 292143 (-4%)
TOTAL 1378182007 1375499992 -2682015 (-0%)

[Janno]

Doesn't seem to be very useful now.

Maybe your comment is only about vo sizes but I just wanted to make sure the performance improvements don't get lost. At the usual going rate of 6 billion instructions per second this change yields an estimated ~5 minute overall improvement in the bench.

[proux01]

We can see a 5% decrease in CPU instructions for fourcolor (heavy VM user) but apparently doesn't really translates in time.

[Janno]

It's possible that the usual exchange rate between instructions and time does not apply because this is only about the vm. However, even the time measurements attest about a minute of time saved across the bench. Given that the change does not seem super complex (at least in terms of lines of code) it almost seems like free (as in "the work is already done") performance to me.

[ppedrot]

We can also merge, it's basically zero-cost in terms of maintenance.

[ppedrot]

FWIW.

[ppedrot]

Alea jacta est, @coqbot merge now