Skip to content

[experiment] Convert stack in the right order except for application nodes.#21996

Draft
ppedrot wants to merge 2 commits into
rocq-prover:masterfrom
ppedrot:conversion-right-order-except-application
Draft

[experiment] Convert stack in the right order except for application nodes.#21996
ppedrot wants to merge 2 commits into
rocq-prover:masterfrom
ppedrot:conversion-right-order-except-application

Conversation

@ppedrot
Copy link
Copy Markdown
Member

@ppedrot ppedrot commented May 4, 2026

Variant of #19038 that was itself a revival of another endless stream of attempts at making the kernel conversion saner.

@ppedrot ppedrot added request: full CI Use this label when you want your next push to trigger a full CI. kind: experiment labels May 4, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 4, 2026
@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 4, 2026

@coqbot bench

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented May 4, 2026

hott is going mad on this command https://github.com/HoTT/Coq-HoTT/blob/0fa55b36710d8a6933ea4f965f7adc5fc0377318/theories/Homotopy/ExactSequence.v#L471-L475

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 4, 2026

🏁 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.74     6.85    -1.61 │    41464613701     41464690316    -0.00 │  446116   447464  -0.30 │
│                        coq-coqprime │   53.38    53.91    -0.98 │   364388189367    366041717389    -0.45 │  826188   824096   0.25 │
│                 rocq-metarocq-utils │   24.62    24.80    -0.73 │   159119552012    159186458007    -0.04 │  593008   593000   0.00 │
│          rocq-metarocq-translations │   16.65    16.75    -0.60 │   118783014648    118719344751     0.05 │  783788   785472  -0.21 │
│                      coq-verdi-raft │  499.59   502.30    -0.54 │  3448006447369   3445793811706     0.06 │  822248   834556  -1.47 │
│                    coq-math-classes │   83.53    83.96    -0.51 │   508762802721    508747559191     0.00 │  513760   518516  -0.92 │
│          coq-performance-tests-lite │  903.29   906.34    -0.34 │  7247776786906   7243281850455     0.06 │ 1271064  1269940   0.09 │
│                rocq-metarocq-common │   41.37    41.47    -0.24 │   266198331665    266377496089    -0.07 │  925300   925316  -0.00 │
│ coq-neural-net-interp-computed-lite │  238.69   239.17    -0.20 │  2266597969729   2267135462043    -0.02 │  894700   897428  -0.30 │
│                 coq-category-theory │  554.15   554.98    -0.15 │  4053239012573   4050394244930     0.07 │  891832   887772   0.46 │
│                       coq-fiat-core │   56.48    56.56    -0.14 │   343853053179    343476211817     0.11 │  481864   482972  -0.23 │
│         coq-rewriter-perf-SuperFast │  477.59   477.97    -0.08 │  3730093365268   3733112782496    -0.08 │ 1246420  1246448  -0.00 │
│                         rocq-stdlib │  436.78   437.07    -0.07 │  1559127350749   1563909751058    -0.31 │  646524   648740  -0.34 │
│                           coq-color │  234.25   234.34    -0.04 │  1485768016294   1485557644171     0.01 │ 1169748  1172968  -0.27 │
│                        coq-rewriter │  334.57   334.52     0.01 │  2480242987937   2479588732284     0.03 │ 1536428  1542620  -0.40 │
│                   coq-iris-examples │  371.11   370.87     0.06 │  2421612019156   2421830988599    -0.01 │ 1118888  1119284  -0.04 │
│                 rocq-mathcomp-field │  195.40   195.09     0.16 │  1476011471370   1451517351967     1.69 │ 2300976  2097472   9.70 │
│                  rocq-mathcomp-boot │   39.28    39.21     0.18 │   231285394081    230561705373     0.31 │  640516   641052  -0.08 │
│              rocq-mathcomp-fingroup │   26.72    26.66     0.23 │   172772097458    172240626314     0.31 │  573976   571900   0.36 │
│                        coq-bedrock2 │  362.13   361.24     0.25 │  2997503897831   2999966877282    -0.08 │  880220   879320   0.10 │
│                           coq-verdi │   44.12    44.00     0.27 │   292783199676    292803283952    -0.01 │  526864   530800  -0.74 │
│               coq-engine-bench-lite │  128.97   128.60     0.29 │   959673155631    958698854323     0.10 │ 1005672  1005208   0.05 │
│                            coq-corn │  672.86   670.66     0.33 │  4507214537928   4500076159682     0.16 │  716848   754476  -4.99 │
│                         coq-coqutil │   47.56    47.40     0.34 │   294662280210    294332164047     0.11 │  569600   572292  -0.47 │
│                 rocq-metarocq-pcuic │  656.50   654.29     0.34 │  4178654474847   4167493742034     0.27 │ 2305704  2328520  -0.98 │
│              rocq-metarocq-template │   85.19    84.89     0.35 │   582753540582    582407330485     0.06 │ 1110516  1110932  -0.04 │
│           rocq-metarocq-safechecker │  345.64   344.36     0.37 │  2525088774238   2522830806114     0.09 │ 1862520  1863916  -0.07 │
│             rocq-mathcomp-character │  103.25   102.79     0.45 │   725175165723    721666360454     0.49 │ 1707380  1705328   0.12 │
│                        rocq-runtime │   75.85    75.50     0.46 │   548826776346    548771046846     0.01 │  503696   505076  -0.27 │
│                           rocq-elpi │   16.27    16.19     0.49 │   115973438303    115971572863     0.00 │  466848   467172  -0.07 │
│                      rocq-equations │    8.49     8.44     0.59 │    59180180182     59166034540     0.02 │  401500   399900   0.40 │
│                        rocq-bignums │   25.81    25.57     0.94 │   163761776216    163754290796     0.00 │  462892   458900   0.87 │
│                    coq-fiat-parsers │  283.25   280.60     0.94 │  2162788061220   2141111782122     1.01 │ 2298292  2320996  -0.98 │
│             rocq-mathcomp-ssreflect │    1.04     1.02     1.96 │     6790961400      6789535592     0.02 │  589812   589588   0.04 │
│                      coq-coquelicot │   40.88    40.02     2.15 │   252269666276    242940015613     3.84 │  827556   835796  -0.99 │
│                            coq-core │    2.72     2.66     2.26 │    18309561167     18311537895    -0.01 │   90564    90164   0.44 │
│                         coq-unimath │ 1895.92  1853.28     2.30 │ 15646955592541  15246757267657     2.62 │ 1070876  1059820   1.04 │
│                 rocq-mathcomp-order │   85.43    82.24     3.88 │   639247338078    598498305616     6.81 │ 1648104  1578284   4.42 │
│              rocq-mathcomp-solvable │  103.43    99.06     4.41 │   712601271929    670673416021     6.25 │ 1119144  1121372  -0.20 │
│              coq-mathcomp-odd-order │  676.91   612.81    10.46 │  4951067990586   4323402638572    14.52 │ 2715224  2719756  -0.17 │
│                       coq-fourcolor │ 1498.41  1355.04    10.58 │ 13863628609584  12435829718508    11.48 │ 1030480  1013912   1.63 │
│               coq-mathcomp-analysis │ 1472.94  1151.30    27.94 │ 11897518029564   8464377738580    40.56 │ 1951588  1951672  -0.00 │
│               rocq-mathcomp-algebra │  496.85   331.54    49.86 │  4058653426551   2425669003703    67.32 │ 1363548  1278372   6.66 │
│                            coq-hott │ 7254.45   158.16  4486.78 │ 69954484929916   1065654884573  6464.46 │  462420   460028   0.52 │
└─────────────────────────────────────┴───────────────────────────┴─────────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-compcert (dependency install failed in NEW)
rocq-metarocq-erasure (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)

coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                            TOP 25 SLOW DOWNS                                            │
│                                                                                                         │
│   OLD     NEW     DIFF        %DIFF       Ln             FILE                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.0559  7096  7095.7910  12703039.87%   471  coq-hott/theories/Homotopy/ExactSequence.v.html          │
│  0.00598  44.8    44.7997    749408.87%  4836  rocq-mathcomp-algebra/algebra/matrix.v.html              │
│  0.00650  44.6    44.6110    686640.63%  4866  rocq-mathcomp-algebra/algebra/matrix.v.html              │
│  0.00658  36.1    36.0531    547918.81%  4832  rocq-mathcomp-algebra/algebra/matrix.v.html              │
│  0.00167  35.9    35.8640   2150119.60%   397  coq-fourcolor/theories/proof/gridmap.v.html              │
│  0.00724  35.7    35.7077    493336.52%  4863  rocq-mathcomp-algebra/algebra/matrix.v.html              │
│  0.00152  27.2    27.1844   1783755.31%   461  coq-fourcolor/theories/proof/walkup.v.html               │
│  0.00553  27.0    26.9583    487227.74%   452  coq-fourcolor/theories/proof/walkup.v.html               │
│  0.00618  26.9    26.8490    434238.96%   451  coq-fourcolor/theories/proof/walkup.v.html               │
│     1.15  24.5    23.3722      2033.55%  1588  coq-mathcomp-analysis/theories/ftc.v.html                │
│ 0.000501  11.5    11.5452   2304421.76%   753  coq-unimath/UniMath/AlgebraicTheories/Combinators.v.html │
│    0.828  12.3    11.4670      1384.08%   105  coq-mathcomp-analysis/theories/gauss_integral.v.html     │
│    0.283  7.59     7.3089      2586.47%  1061  coq-mathcomp-odd-order/theories/PFsection13.v.html       │
│    0.183  7.44     7.2601      3977.13%   778  coq-mathcomp-analysis/theories/hoelder.v.html            │
│    0.336  6.58     6.2433      1860.22%  1263  coq-mathcomp-analysis/theories/ftc.v.html                │
│  0.00190  6.17     6.1638    324242.14%   240  coq-fourcolor/theories/proof/birkhoff.v.html             │
│    0.311  6.42     6.1074      1963.80%  1538  coq-mathcomp-analysis/theories/ftc.v.html                │
│  0.00233  6.04     6.0364    259519.00%   220  coq-fourcolor/theories/proof/birkhoff.v.html             │
│   0.0159  5.82     5.8037     36425.37%   139  coq-mathcomp-analysis/theories/derive.v.html             │
│    0.593  6.33     5.7411       967.75%  1153  coq-mathcomp-analysis/theories/ftc.v.html                │
│    0.450  5.81     5.3617      1191.45%   361  coq-mathcomp-analysis/theories/gauss_integral.v.html     │
│    0.519  5.31     4.7874       922.76%  1170  coq-mathcomp-analysis/theories/ftc.v.html                │
│    0.519  5.30     4.7810       921.52%  1161  coq-mathcomp-analysis/theories/ftc.v.html                │
│    0.420  5.02     4.6039      1094.98%  1665  coq-mathcomp-analysis/theories/ftc.v.html                │
│    0.407  4.91     4.5026      1106.17%   622  coq-mathcomp-analysis/theories/ftc.v.html                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD     NEW     DIFF     %DIFF   Ln                     FILE                                                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  8.92   0.0325  -8.8911  -99.64%  126  coq-mathcomp-odd-order/theories/BGappendixAB.v.html                                              │
│  2.84    0.426  -2.4184  -85.01%  404  coq-mathcomp-odd-order/theories/BGappendixC.v.html                                               │
│  2.09    0.643  -1.4458  -69.23%  459  coq-unimath/UniMath/ModelCategories/Examples.v.html                                              │
│  94.6     93.3  -1.2486   -1.32%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  1.38    0.163  -1.2149  -88.15%  150  coq-mathcomp-odd-order/theories/BGappendixAB.v.html                                              │
│  1.43    0.263  -1.1695  -81.65%  395  coq-mathcomp-odd-order/theories/BGappendixC.v.html                                               │
│  1.48    0.315  -1.1687  -78.77%  396  coq-mathcomp-odd-order/theories/BGappendixC.v.html                                               │
│  94.5     93.3  -1.1536   -1.22%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  1.48    0.347  -1.1332  -76.56%  368  coq-unimath/UniMath/ModelCategories/Examples.v.html                                              │
│  1.42    0.329  -1.0959  -76.91%  918  coq-mathcomp-odd-order/theories/PFsection12.v.html                                               │
│  1.46    0.470  -0.9868  -67.72%  158  coq-mathcomp-analysis/theories/realfun.v.html                                                    │
│  1.11    0.128  -0.9849  -88.46%  659  coq-mathcomp-analysis/theories/independence.v.html                                               │
│ 0.711  0.00296  -0.7079  -99.58%  524  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │
│ 0.710    0.127  -0.5828  -82.07%  642  coq-mathcomp-analysis/theories/probability_theory/random_variable.v.html                         │
│ 0.624   0.0459  -0.5782  -92.65%  624  coq-mathcomp-odd-order/theories/BGsection13.v.html                                               │
│   203      203  -0.5699   -0.28%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html    │
│ 0.571  0.00196  -0.5690  -99.66%  160  coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedAssociator.v.html               │
│ 0.636    0.122  -0.5135  -80.74%  593  coq-mathcomp-analysis/theories/ftc.v.html                                                        │
│ 0.638    0.125  -0.5132  -80.41%  570  coq-mathcomp-analysis/theories/ftc.v.html                                                        │
│ 0.550   0.0456  -0.5047  -91.71%  592  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v.html          │
│ 0.552   0.0656  -0.4861  -88.11%  313  coq-fourcolor/theories/proof/revsnip.v.html                                                      │
│  1.36    0.887  -0.4725  -34.75%  408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                        │
│  1.27    0.799  -0.4724  -37.15%  151  coq-mathcomp-odd-order/theories/BGappendixAB.v.html                                              │
│  46.4     46.0  -0.4689   -1.01%  115  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                       │
│ 0.517   0.0593  -0.4578  -88.53%  526  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label May 5, 2026
ppedrot added 2 commits May 5, 2026 10:37
@ppedrot
Convert stack in the right order except for application nodes.
1fe71f6 
Variant of rocq-prover#19038 that was itself a revival of another endless stream of
attempts at making the kernel conversion saner.
@ppedrot
Guard the LTR ordering of conversion with the typing flag.
111c890
@ppedrot ppedrot force-pushed the conversion-right-order-except-application branch from 43a03c3 to 111c890 Compare May 5, 2026 08:38
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 5, 2026
@ppedrot
Copy link
Copy Markdown
Member Author

ppedrot commented May 5, 2026

Let's retry with the correct ordering in the kernel only, similarly to what I did in #19038. @coqbot bench

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 5, 2026

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                      coq-coquelicot │   39.70    40.27  -1.42 │   242552154049    243347314194  -0.33 │  829448   834348  -0.59 │
│                        rocq-runtime │   75.16    75.84  -0.90 │   549053904491    548905337455   0.03 │  506024   500836   1.04 │
│                         coq-unimath │ 1855.89  1866.63  -0.58 │ 15309076904255  15248562577133   0.40 │ 1069616  1059936   0.91 │
│                 rocq-metarocq-utils │   24.57    24.68  -0.45 │   158949580792    159181467747  -0.15 │  594812   593192   0.27 │
│              rocq-metarocq-template │   84.91    85.24  -0.39 │   582128560120    582378393211  -0.04 │ 1113064  1111124   0.17 │
│                         rocq-stdlib │  440.18   441.54  -0.31 │  1564235694924   1564219541220   0.00 │  648740   646184   0.40 │
│          rocq-metarocq-translations │   16.68    16.71  -0.18 │   118634650756    118771337883  -0.12 │  784852   786088  -0.16 │
│                           rocq-core │    6.78     6.79  -0.15 │    41484628406     41471958029   0.03 │  449028   449196  -0.04 │
│                      rocq-equations │    8.58     8.59  -0.12 │    58663827057     59130648937  -0.79 │  399044   400376  -0.33 │
│                        coq-coqprime │   53.65    53.70  -0.09 │   365716571161    366082111278  -0.10 │  823864   821860   0.24 │
│              coq-mathcomp-odd-order │  610.33   610.83  -0.08 │  4323101456740   4321133122365   0.05 │ 2724840  2721432   0.13 │
│                           rocq-elpi │   16.33    16.34  -0.06 │   116026976655    116018665541   0.01 │  448240   448064   0.04 │
│               coq-engine-bench-lite │  129.62   129.59   0.02 │   960344344858    961142250262  -0.08 │ 1005052  1009992  -0.49 │
│               rocq-metarocq-erasure │  482.72   482.55   0.04 │  3302011111807   3303608950558  -0.05 │ 1801080  1819868  -1.03 │
│                   coq-iris-examples │  370.95   370.76   0.05 │  2421120776170   2422018299542  -0.04 │ 1125576  1121448   0.37 │
│                 rocq-mathcomp-field │  193.05   192.91   0.07 │  1450761675902   1451414929894  -0.05 │ 2294916  2098592   9.36 │
│                       coq-fiat-core │   56.20    56.14   0.11 │   343266175395    343688065354  -0.12 │  482900   480772   0.44 │
│              rocq-mathcomp-fingroup │   26.69    26.66   0.11 │   172268145275    172245771081   0.01 │  573632   573636  -0.00 │
│                           coq-verdi │   44.03    43.98   0.11 │   292488487517    292891901860  -0.14 │  527704   527736  -0.01 │
│               rocq-mathcomp-algebra │  330.25   329.87   0.12 │  2425921158188   2425718850640   0.01 │ 1274464  1276932  -0.19 │
│                           coq-color │  234.08   233.81   0.12 │  1484981829492   1485723560214  -0.05 │ 1175068  1170180   0.42 │
│          coq-performance-tests-lite │  904.99   903.74   0.14 │  7240715837350   7244461715987  -0.05 │ 1269868  1219696   4.11 │
│                        coq-bedrock2 │  364.89   364.32   0.16 │  2995560408832   2999897546404  -0.14 │  881488   885668  -0.47 │
│                 rocq-metarocq-pcuic │  655.32   653.77   0.24 │  4168100391203   4167549516874   0.01 │ 2300124  2327732  -1.19 │
│                    coq-fiat-parsers │  280.16   279.46   0.25 │  2140721528201   2141743462469  -0.05 │ 2319272  2319036   0.01 │
│                         coq-coqutil │   47.76    47.64   0.25 │   294117703094    294590430940  -0.16 │  570292   569340   0.17 │
│               coq-mathcomp-analysis │ 1151.90  1148.38   0.31 │  8466739678027   8464557928075   0.03 │ 1954948  1954772   0.01 │
│                            coq-corn │  673.56   670.97   0.39 │  4499079745259   4500325432368  -0.03 │  754708   754428   0.04 │
│             rocq-mathcomp-character │  102.80   102.40   0.39 │   722620068975    722395475946   0.03 │ 1707052  1705372   0.10 │
│         coq-rewriter-perf-SuperFast │  477.21   475.12   0.44 │  3730973642653   3731515909232  -0.01 │ 1234256  1240264  -0.48 │
│           rocq-metarocq-safechecker │  345.46   343.91   0.45 │  2522305461917   2522782210258  -0.02 │ 1875752  1864696   0.59 │
│              rocq-mathcomp-solvable │   99.24    98.77   0.48 │   671861927308    671030998771   0.12 │ 1115020  1124192  -0.82 │
│                 rocq-mathcomp-order │   81.15    80.75   0.50 │   598824181922    598793027003   0.01 │ 1650652  1617372   2.06 │
│                  rocq-mathcomp-boot │   39.21    39.01   0.51 │   230560512924    230555039239   0.00 │  637940   639684  -0.27 │
│                        coq-rewriter │  335.13   333.32   0.54 │  2479185225739   2479994015479  -0.03 │ 1538412  1546780  -0.54 │
│                    coq-math-classes │   84.21    83.69   0.62 │   508744736301    508792069866  -0.01 │  514100   514020   0.02 │
│ coq-neural-net-interp-computed-lite │  237.86   236.39   0.62 │  2266378990197   2267144097997  -0.03 │  895192   895264  -0.01 │
│                 coq-category-theory │  555.29   551.82   0.63 │  4049823497955   4050833991790  -0.02 │  895448   889972   0.62 │
│                        rocq-bignums │   25.81    25.64   0.66 │   163714486278    163711601056   0.00 │  460248   463100  -0.62 │
│                            coq-hott │  158.74   157.66   0.69 │  1065824971002   1065618595081   0.02 │  462364   462320   0.01 │
│                      coq-verdi-raft │  501.39   497.70   0.74 │  3443685760543   3446297563046  -0.08 │  824228   836048  -1.41 │
│                rocq-metarocq-common │   41.50    41.13   0.90 │   266319551334    266299208233   0.01 │  922468   920776   0.18 │
│             rocq-mathcomp-ssreflect │    1.05     1.03   1.94 │     6791364204      6789025362   0.03 │  589800   591828  -0.34 │
│                            coq-core │    2.83     2.76   2.54 │    18526127651     18523670504   0.01 │   90524    90368   0.17 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-compcert (dependency install failed in NEW)
coq-fiat-crypto-with-bedrock (in NEW)
coq-fourcolor (dependency install failed in NEW)

coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SLOW DOWNS                                                                │
│                                                                                                                                                 │
│   OLD      NEW    DIFF     %DIFF     Ln                      FILE                                                                               │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    0.163   4.48  4.3124   2651.41%   536  coq-unimath/UniMath/CategoryTheory/LocallyCartesianClosed/Preservation.v.html                         │
│   0.0398   2.18  2.1368   5368.04%   452  coq-unimath/UniMath/CategoryTheory/LocallyCartesianClosed/Preservation.v.html                         │
│      200    202  1.6524      0.82%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html         │
│     94.6   95.3  0.6548      0.69%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│     3.73   4.27  0.5403     14.49%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                  │
│    0.159  0.629  0.4693    294.49%   301  coq-unimath/UniMath/CategoryTheory/LocallyCartesianClosed/Preservation.v.html                         │
│   0.0351  0.466  0.4313   1227.14%   373  coq-unimath/UniMath/CategoryTheory/LocallyCartesianClosed/Preservation.v.html                         │
│     2.28   2.69  0.4149     18.23%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                    │
│     36.3   36.7  0.4012      1.10%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                          │
│    0.632   1.01  0.3821     60.50%   200  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                                    │
│ 0.000749  0.382  0.3813  50906.54%   146  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v.html │
│     94.7   95.0  0.3491      0.37%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│     38.2   38.5  0.3485      0.91%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                        │
│   0.0164  0.362  0.3457   2104.13%   251  coq-unimath/UniMath/CategoryTheory/Inductives/Lists.v.html                                            │
│    0.204  0.541  0.3366    164.67%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                        │
│    0.408  0.738  0.3297     80.80%  1161  rocq-stdlib/theories/Strings/Byte.v.html                                                              │
│     38.8   39.1  0.3215      0.83%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                            │
│    0.351  0.641  0.2905     82.85%   596  rocq-stdlib/theories/Strings/Byte.v.html                                                              │
│     2.80   3.08  0.2831     10.11%   597  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html             │
│     18.7   19.0  0.2697      1.44%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                     │
│     7.51   7.78  0.2659      3.54%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html        │
│    0.228  0.490  0.2613    114.40%     4  rocq-stdlib/theories/extraction/ExtrHaskellZInteger.v.html                                            │
│    0.491  0.742  0.2512     51.19%    59  rocq-stdlib/theories/ZArith/Zeuclid.v.html                                                            │
│    0.255  0.499  0.2444     95.97%     1  rocq-stdlib/theories/micromega/ZifyPow.v.html                                                         │
│    0.728  0.967  0.2395     32.91%    41  rocq-stdlib/theories/ZArith/Zdiv_facts.v.html                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SPEED UPS                                                         │
│                                                                                                                                  │
│  OLD     NEW     DIFF     %DIFF    Ln                   FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  2.11    0.642  -1.4683  -69.59%   459  coq-unimath/UniMath/ModelCategories/Examples.v.html                                      │
│  13.1     12.1  -1.0518   -8.01%   388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  13.5     12.6  -0.9426   -6.97%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  13.1     12.2  -0.9250   -7.07%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  9.18     8.44  -0.7406   -8.06%   648  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  8.53     7.83  -0.6949   -8.15%   633  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  7.91     7.32  -0.5946   -7.52%   663  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  9.41     8.84  -0.5649   -6.00%   950  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  10.1     9.66  -0.4577   -4.53%   435  coq-mathcomp-odd-order/theories/PFsection12.v.html                                       │
│  4.38     3.95  -0.4287   -9.80%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                            │
│  7.17     6.75  -0.4180   -5.83%   831  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  19.8     19.4  -0.4068   -2.06%   559  coq-mathcomp-odd-order/theories/PFsection9.v.html                                        │
│ 0.891    0.493  -0.3974  -44.62%   586  rocq-stdlib/theories/Strings/Byte.v.html                                                 │
│  5.03     4.65  -0.3820   -7.60%   646  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│ 0.642    0.268  -0.3738  -58.23%    12  rocq-stdlib/theories/MSets/MSets.v.html                                                  │
│ 0.342  0.00134  -0.3409  -99.61%   265  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v.html  │
│ 0.700    0.423  -0.2766  -39.54%   682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                         │
│  3.56     3.29  -0.2719   -7.64%   751  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│ 0.405    0.136  -0.2692  -66.52%  1177  rocq-stdlib/theories/Reals/Abstract/ConstructiveReals.v.html                             │
│  4.05     3.79  -0.2605   -6.43%   909  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  4.08     3.83  -0.2543   -6.23%   895  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  3.28     3.03  -0.2518   -7.67%   668  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  3.50     3.25  -0.2504   -7.15%   610  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  10.2     9.95  -0.2470   -2.42%   673  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                             │
│  21.0     20.8  -0.2442   -1.16%   479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

kind: experiment

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ppedrot @SkySkimmer