Experiment: unboxed ints in ltac2 runtime

[SkySkimmer]

No description provided.

[SkySkimmer]

@coqbot bench

[SkySkimmer]

cc @Janno @gmalecha-at-skylabs if you have some private bench you want to try this on
(I'm not expecting much though)

[Janno]

+0.07%, possibly noise. (SkyLabsAI#13 (comment))

[SkySkimmer]

Ltac2 does not use many ints I guess

[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-elpi │   16.32    16.47  -0.91 │   116422581158    116425032609  -0.00 │  448948   452760  -0.84 │
│             rocq-mathcomp-ssreflect │    1.17     1.18  -0.85 │     7669001079      7670798584  -0.02 │  591760   591664   0.02 │
│                        coq-coqprime │   56.28    56.76  -0.85 │   390860417500    390837303896   0.01 │  822004   822188  -0.02 │
│                         rocq-stdlib │  419.09   421.01  -0.46 │  1508094735362   1508033911186   0.00 │  632432   628268   0.66 │
│                 rocq-metarocq-utils │   24.33    24.44  -0.45 │   159092849746    159093915832  -0.00 │  589040   588152   0.15 │
│                         coq-coqutil │   46.84    47.04  -0.43 │   290897844207    290912654418  -0.01 │  567828   564148   0.65 │
│          rocq-metarocq-translations │   15.25    15.31  -0.39 │   108768939768    108770506083  -0.00 │  782012   784456  -0.31 │
│              rocq-metarocq-template │   81.47    81.77  -0.37 │   560000966097    560017799635  -0.00 │ 1084392  1084740  -0.03 │
│                  rocq-mathcomp-boot │   39.39    39.50  -0.28 │   232513731528    232509259774   0.00 │  654260   656244  -0.30 │
│                           coq-verdi │   43.11    43.20  -0.21 │   288105673345    288090434375   0.01 │  520700   519772   0.18 │
│                        coq-compcert │  301.13   301.63  -0.17 │  1977201866021   1977184410561   0.00 │ 1226392  1225560   0.07 │
│                        coq-bedrock2 │  356.27   356.75  -0.13 │  2967549375811   2967687328731  -0.00 │  810992   807776   0.40 │
│                rocq-metarocq-common │   41.22    41.25  -0.07 │   267945785506    267924022185   0.01 │  904740   902364   0.26 │
│                        rocq-runtime │   75.88    75.93  -0.07 │   551195237098    551031941138   0.03 │  494420   495012  -0.12 │
│                      coq-verdi-raft │  489.72   490.00  -0.06 │  3391849632492   3391797340274   0.00 │  812760   814764  -0.25 │
│        coq-fiat-crypto-with-bedrock │ 7200.31  7203.70  -0.05 │ 59433785715020  59430414430237   0.01 │ 2874460  2861300   0.46 │
│                        coq-rewriter │  329.43   329.50  -0.02 │  2454198040334   2454106091882   0.00 │ 1444524  1434148   0.72 │
│         coq-rewriter-perf-SuperFast │  465.19   465.28  -0.02 │  3654310088825   3650373231317   0.11 │ 1252312  1251464   0.07 │
│                 rocq-mathcomp-order │   81.47    81.48  -0.01 │   600934937578    600944400757  -0.00 │ 1608540  1608972  -0.03 │
│               coq-engine-bench-lite │  127.73   127.73  -0.00 │   948105132816    947955294750   0.02 │ 1103476  1105744  -0.21 │
│                            coq-core │    2.69     2.69   0.00 │    18577317976     18576835812   0.00 │   91300    90956   0.38 │
│                           coq-color │  229.94   229.90   0.02 │  1456280572819   1456187109280   0.01 │ 1151612  1152164  -0.05 │
│                       coq-fiat-core │   55.59    55.57   0.04 │   336052080675    336071625508  -0.01 │  484908   484064   0.17 │
│                 coq-category-theory │  640.21   639.77   0.07 │  4781246596318   4781443978559  -0.00 │ 6749000  6751212  -0.03 │
│                         coq-unimath │ 1819.93  1818.56   0.08 │ 15179781205998  15178715535660   0.01 │ 1085316  1085876  -0.05 │
│ coq-neural-net-interp-computed-lite │  236.55   236.37   0.08 │  2264516162745   2264561813956  -0.00 │  879992   880460  -0.05 │
│          coq-performance-tests-lite │  882.18   881.22   0.11 │  7091360499867   7087433879118   0.06 │ 1302240  1299032   0.25 │
│                             coq-vst │  832.23   831.23   0.12 │  6320530533391   6320848802972  -0.01 │ 2174148  2176032  -0.09 │
│                 rocq-metarocq-pcuic │  601.83   601.10   0.12 │  3882860190536   3882729328570   0.00 │ 1693864  1692620   0.07 │
│                            coq-corn │  635.83   635.04   0.12 │  4324967604756   4325084119574  -0.00 │  619336   617484   0.30 │
│                            coq-hott │  157.14   156.93   0.13 │  1058587119530   1058584524892   0.00 │  475976   477260  -0.27 │
│                    coq-math-classes │   82.12    81.97   0.18 │   499304437048    499241956105   0.01 │  513584   515016  -0.28 │
│                      coq-coquelicot │   38.85    38.77   0.21 │   235039897803    235073255447  -0.01 │  828772   829364  -0.07 │
│               rocq-metarocq-erasure │  440.72   439.69   0.23 │  2998494340187   2998601390358  -0.00 │ 1809908  1809036   0.05 │
│                   coq-iris-examples │  365.68   364.82   0.24 │  2387778154847   2387834595314  -0.00 │ 1065816  1069916  -0.38 │
│           rocq-metarocq-safechecker │  318.91   317.89   0.32 │  2380324284151   2380098058238   0.01 │ 1729864  1725700   0.24 │
│                      rocq-equations │    8.56     8.53   0.35 │    58527868642     58510482283   0.03 │  400572   400128   0.11 │
│          rocq-mathcomp-finite-group │   26.55    26.45   0.38 │   172615384814    172613231325   0.00 │  570400   572116  -0.30 │
│                    coq-fiat-parsers │  272.88   271.46   0.52 │  2090042025953   2090041525366   0.00 │ 2032972  2033264  -0.01 │
│                        rocq-bignums │   24.98    24.82   0.64 │   158020214333    158022332014  -0.00 │  459048   460148  -0.24 │
│                           rocq-core │    6.95     6.79   2.36 │    41339874440     41335175585   0.01 │  445468   446072  -0.14 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-algebra (in NEW)

rocq-mathcomp-solvable (dependency rocq-mathcomp-algebra failed)
rocq-mathcomp-field (dependency rocq-mathcomp-algebra failed)
rocq-mathcomp-group-representation (dependency rocq-mathcomp-algebra failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-algebra failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-algebra failed)
coq-fourcolor (dependency rocq-mathcomp-algebra failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SLOW DOWNS                                                             │
│                                                                                                                                           │
│  OLD     NEW     DIFF    %DIFF   Ln                      FILE                                                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   17.9    18.7  0.8576    4.79%   32  coq-performance-tests-lite/src/pattern.v.html                                                       │
│   21.7    22.4  0.6409    2.95%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                             │
│   34.6    35.2  0.5998    1.74%  194  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                       │
│   80.2    80.8  0.5763    0.72%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                             │
│  0.274   0.782  0.5082  185.66%  682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                                    │
│   3.73    4.23  0.4914   13.16%  196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                       │
│   53.8    54.3  0.4724    0.88%  296  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                  │
│    201     201  0.4619    0.23%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html       │
│   55.4    55.8  0.4252    0.77%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                            │
│   58.2    58.7  0.4181    0.72%  659  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                               │
│ 34.286  34.691  0.4050    1.18%   97  coq-vst/veric/binop_lemmas5.v.html                                                                  │
│   80.4    80.8  0.3769    0.47%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                         │
│   40.6    41.0  0.3507    0.86%  539  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                          │
│  0.225   0.564  0.3399  151.31%   18  rocq-stdlib/theories/ZArith/Zeven.v.html                                                            │
│   28.8    29.1  0.3102    1.08%  145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                        │
│  0.308   0.613  0.3047   98.80%   19  rocq-stdlib/theories/ZArith/Int.v.html                                                              │
│   18.8    19.1  0.2941    1.56%   23  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html                                       │
│   11.1    11.4  0.2894    2.60%  194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                            │
│   20.3    20.6  0.2790    1.38%    6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │
│   11.1    11.4  0.2578    2.31%  159  coq-fiat-crypto-with-bedrock/src/Bedrock/P256.v.html                                                │
│  0.262   0.518  0.2563   97.90%   14  rocq-stdlib/theories/ZArith/auxiliary.v.html                                                        │
│ 11.496  11.751  0.2550    2.22%  126  coq-vst/veric/binop_lemmas6.v.html                                                                  │
│   24.9    25.1  0.2500    1.00%  788  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                │
│   15.2    15.4  0.2446    1.61%  898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                │
│  0.149   0.386  0.2371  159.24%  820  rocq-stdlib/theories/micromega/EnvRing.v.html                                                       │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SPEED UPS                                                          │
│                                                                                                                                    │
│  OLD    NEW    DIFF     %DIFF   Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  66.1   62.9  -3.1529   -4.77%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│  63.8   62.9  -0.8913   -1.40%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│  47.2   46.4  -0.8693   -1.84%  115  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html  │
│  31.1   30.4  -0.6803   -2.19%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html          │
│  2.12   1.58  -0.5403  -25.54%   42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                      │
│  31.1   30.5  -0.5281   -1.70%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html          │
│  46.6   46.1  -0.5062   -1.09%  277  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  55.2   54.7  -0.4495   -0.81%  512  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│  37.1   36.7  -0.4220   -1.14%  244  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                  │
│  45.2   44.8  -0.4157   -0.92%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html              │
│  31.2   30.8  -0.3842   -1.23%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html          │
│  21.6   21.2  -0.3812   -1.77%  651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│  13.3   12.9  -0.3697   -2.78%  286  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│ 0.722  0.366  -0.3566  -49.36%  596  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│  23.9   23.6  -0.3116   -1.30%  782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│ 0.645  0.341  -0.3043  -47.17%   14  rocq-stdlib/theories/MSets/MSetToFiniteSet.v.html                                             │
│  31.5   31.2  -0.3030   -0.96%  331  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                    │
│  31.0   30.7  -0.3028   -0.98%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html          │
│ 0.588  0.294  -0.2944  -50.04%   18  rocq-stdlib/theories/micromega/VarMap.v.html                                                  │
│ 0.587  0.297  -0.2900  -49.41%   16  rocq-stdlib/theories/extraction/ExtrOcamlIntConv.v.html                                       │
│  20.0   19.7  -0.2891   -1.45%  225  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                  │
│ 0.514  0.234  -0.2803  -54.50%   11  rocq-stdlib/theories/ZArith/Wf_Z.v.html                                                       │
│  23.1   22.8  -0.2741   -1.19%   85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                        │
│  31.2   31.0  -0.2732   -0.87%  255  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                    │
│ 0.764  0.491  -0.2729  -35.71%  207  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                            │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

as expected doesn't really do anything