Evarconv: save keys

[Tragicus]

Saves the head constant of a term before delta-reducing it, to be used during canonical structure resolution and to find matching heads.
Also prevents trying to solve canonical structure problems of the form S.proj s ~ t when s reduces to an applied constructor.

Fixes / closes #????

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

• mathcomp-analysis: adapt to coq#19611 math-comp/analysis#1377
• odd-order: annotate card_vspace1 math-comp/odd-order#60
• fcsl-pcm: Adapt to coq#pr19611 imdea-software/fcsl-pcm#45

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

started a bench manually to have the mathcomp overlay

[pi8027]

FYI, I started porting lemma-overloading to recent versions of Coq and MathComp. I think this is a good stress test for this PR. (I don't think I will finish it quickly though.)

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬──────────────────────────┬────────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]       │            CPU instructions            │  max resident mem [KB]  │
│                                     │                          │                                        │                         │
│            package_name             │   NEW      OLD    PDIFF  │      NEW             OLD        PDIFF  │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼──────────────────────────┼────────────────────────────────────────┼─────────────────────────┤
│              coq-mathcomp-ssreflect │   89.55   105.71  -15.29 │   593765703433    675097586725  -12.05 │ 1708612  1601036   6.72 │
│                  coq-mathcomp-field │   86.00    89.71   -4.14 │   600885944213    624864974808   -3.84 │ 1216220  1222288  -0.50 │
│                coq-mathcomp-algebra │  140.03   145.09   -3.49 │   943208861313    974396403803   -3.20 │ 1246296  1217864   2.33 │
│                            coq-core │  131.88   133.17   -0.97 │   538775747363    537923375867    0.16 │  464636   463612   0.22 │
│                      coq-coquelicot │   36.21    36.38   -0.47 │   219058827535    219457366312   -0.18 │  806192   797560   1.08 │
│                         coq-bignums │   29.15    29.27   -0.41 │   187620597553    187670802631   -0.03 │  466892   466732   0.03 │
│                    coq-math-classes │   82.89    83.12   -0.28 │   510039285588    509907834273    0.03 │  503612   505028  -0.28 │
│            coq-metacoq-translations │   16.24    16.28   -0.25 │   116717921642    116650628876    0.06 │  774664   776028  -0.18 │
│         coq-rewriter-perf-SuperFast │  760.00   761.82   -0.24 │  5897070818265   5893652429846    0.06 │ 1417276  1405464   0.84 │
│                        coq-bedrock2 │  324.48   325.18   -0.22 │  2759798121663   2758721757276    0.04 │  854256   855004  -0.09 │
│                        coq-compcert │  296.59   296.93   -0.11 │  1969076554753   1968900609438    0.01 │ 1043524  1099004  -5.05 │
│                           coq-color │  242.15   242.38   -0.09 │  1530532602613   1530169927014    0.02 │ 1134936  1141108  -0.54 │
│                        coq-rewriter │  336.93   336.99   -0.02 │  2522840750122   2520893274970    0.08 │ 1320152  1312212   0.61 │
│                 coq-metacoq-erasure │  518.64   518.51    0.03 │  3629447415427   3617390942937    0.33 │ 1910368  1880440   1.59 │
│                coq-metacoq-template │  144.95   144.88    0.05 │   981092236486    980571017599    0.05 │ 1229632  1229996  -0.03 │
│                      coq-verdi-raft │  532.82   532.40    0.08 │  3715589182606   3713463475553    0.06 │  822568   830628  -0.97 │
│                         coq-coqutil │   42.04    42.00    0.10 │   264395161626    264198201368    0.07 │  681692   679424   0.33 │
│        coq-fiat-crypto-with-bedrock │ 5272.64  5263.86    0.17 │ 42756185125487  42735126349101    0.05 │ 3245484  3245524  -0.00 │
│                 coq-category-theory │  612.11   610.71    0.23 │  4547269133461   4531510158951    0.35 │  982504   983308  -0.08 │
│                   coq-metacoq-pcuic │  689.23   687.59    0.24 │  4500597644567   4493354574677    0.16 │ 3023924  2963848   2.03 │
│                             coq-vst │  856.79   854.64    0.25 │  6454103927081   6451604288675    0.04 │ 1670044  1686824  -0.99 │
│             coq-metacoq-safechecker │  357.04   355.93    0.31 │  2704889680353   2706916488112   -0.07 │ 1880316  1884324  -0.21 │
│                   coq-metacoq-utils │   22.44    22.36    0.36 │   147802784250    147541387752    0.18 │  582812   583552  -0.13 │
│                       coq-fiat-core │   55.28    55.06    0.40 │   335277567151    334910529400    0.11 │  470636   469568   0.23 │
│                          coq-stdlib │  349.16   347.13    0.58 │  1211878544222   1211032327532    0.07 │  641680   640348   0.21 │
│               coq-mathcomp-fingroup │   26.14    25.97    0.65 │   171920258169    172842808336   -0.53 │  566396   562276   0.73 │
│                           coq-verdi │   44.23    43.89    0.77 │   295099698361    294621171347    0.16 │  526468   520572   1.13 │
│                    coq-fiat-parsers │  275.28   273.07    0.81 │  2127610473729   2127052320493    0.03 │ 2288972  2290104  -0.05 │
│                  coq-metacoq-common │   65.89    65.26    0.97 │   428603066947    428243840959    0.08 │ 1228060  1228380  -0.03 │
│ coq-neural-net-interp-computed-lite │  234.92   232.48    1.05 │  2253470067051   2253200986106    0.01 │  846080   847384  -0.15 │
│               coq-mathcomp-solvable │   95.23    94.23    1.06 │   672666146553    654105986926    2.84 │  879408   877048   0.27 │
│               coq-engine-bench-lite │  130.58   129.12    1.13 │   971452409059    967934679775    0.36 │ 1058672  1059056  -0.04 │
│                       coq-equations │    7.12     7.02    1.42 │    47725746624     47670990230    0.11 │  384604   385920  -0.34 │
│                        coq-coqprime │   51.70    50.92    1.53 │   354921498383    354810409244    0.03 │  783148   781192   0.25 │
│                            coq-corn │  678.23   664.91    2.00 │  4724824917108   4630759298817    2.03 │  750888   723772   3.75 │
│                   coq-iris-examples │  524.52   389.09   34.81 │  3663492067555   2614036103434   40.15 │ 1075552  1147496  -6.27 │
│                       coq-fourcolor │ 1996.50  1351.68   47.71 │ 16544608430012  12512926816404   32.22 │  818408   828496  -1.22 │
└─────────────────────────────────────┴──────────────────────────┴────────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-hott
coq-performance-tests-lite
coq-mathcomp-character
coq-mathcomp-analysis (dependency install failed in NEW)
coq-unimath

coq-mathcomp-odd-order (dependency coq-mathcomp-character failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                    TOP 25 SLOW DOWNS                                                                    │
│                                                                                                                                                         │
│   OLD       NEW       DIFF      %DIFF      Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.4110  534.9490  534.5380  130057.91%   193  coq-fourcolor/theories/hypermap.v.html                                                                  │
│   0.6130   70.7650   70.1520   11444.05%   670  coq-fourcolor/theories/matte.v.html                                                                     │
│   8.0820   52.1460   44.0640     545.21%   581  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   8.0880   52.1000   44.0120     544.16%   591  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   7.9890   51.7230   43.7340     547.43%   580  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   0.4160   42.2550   41.8390   10057.45%   621  coq-fourcolor/theories/matte.v.html                                                                     │
│   0.2430    3.7030    3.4600    1423.87%  1156  coq-fourcolor/theories/cfmap.v.html                                                                     │
│  62.3500   65.1640    2.8140       4.51%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│ 198.3720  200.5560    2.1840       1.10%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│ 181.0750  182.6620    1.5870       0.88%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 120.1750  121.2370    1.0620       0.88%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  94.1270   95.0840    0.9570       1.02%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│   3.0240    3.9220    0.8980      29.70%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│   3.0920    3.9450    0.8530      27.59%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  36.9020   37.7500    0.8480       2.30%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  23.9940   24.8180    0.8240       3.43%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│   0.4760    1.2870    0.8110     170.38%   330  coq-metacoq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html                                 │
│   0.0110    0.8140    0.8030    7300.00%   165  coq-fourcolor/theories/revsnip.v.html                                                                   │
│  36.5750   37.3540    0.7790       2.13%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  35.5480   36.1710    0.6230       1.75%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  37.2650   37.8230    0.5580       1.50%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                     │
│  18.3720   18.8810    0.5090       2.77%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
│   6.3770    6.8650    0.4880       7.65%   192  coq-vst/veric/binop_lemmas5.v.html                                                                      │
│   1.6460    2.0690    0.4230      25.70%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│   1.0130    1.4200    0.4070      40.18%  1142  coq-stdlib/FSets/FMapAVL.v.html                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SPEED UPS                                                           │
│                                                                                                                                      │
│   OLD      NEW      DIFF     %DIFF    Ln                    FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 11.2360   0.2140  -11.0220  -98.10%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                    │
│  4.8790   0.4880   -4.3910  -90.00%  2089  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                    │
│ 63.6750  62.4490   -1.2260   -1.93%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                               │
│  1.1970   0.0010   -1.1960  -99.92%  3118  coq-mathcomp-algebra/mathcomp/algebra/poly.v.html                                         │
│  4.9420   3.8210   -1.1210  -22.68%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                    │
│  1.0040   0.0070   -0.9970  -99.30%   202  coq-mathcomp-field/mathcomp/field/separable.v.html                                        │
│ 25.6430  24.7880   -0.8550   -3.33%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                        │
│  0.8560   0.0080   -0.8480  -99.07%  1595  coq-mathcomp-solvable/mathcomp/solvable/maximal.v.html                                    │
│  5.0150   4.2040   -0.8110  -16.17%  1827  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                       │
│  3.2780   2.5500   -0.7280  -22.21%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                    │
│ 25.4450  24.8220   -0.6230   -2.45%    12  coq-fourcolor/theories/job279to282.v.html                                                 │
│ 25.4840  24.8890   -0.5950   -2.33%    12  coq-fourcolor/theories/job299to302.v.html                                                 │
│ 62.1100  61.5380   -0.5720   -0.92%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                  │
│  2.5080   1.9570   -0.5510  -21.97%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                               │
│  0.5310   0.0060   -0.5250  -98.87%   177  coq-mathcomp-solvable/mathcomp/solvable/alt.v.html                                        │
│ 12.4480  11.9460   -0.5020   -4.03%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                  │
│ 19.9150  19.4660   -0.4490   -2.25%    12  coq-fourcolor/theories/job507to510.v.html                                                 │
│ 39.1870  38.7410   -0.4460   -1.14%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                │
│  0.4400   0.0030   -0.4370  -99.32%   363  coq-mathcomp-solvable/mathcomp/solvable/cyclic.v.html                                     │
│  2.0160   1.5830   -0.4330  -21.48%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                               │
│ 39.1230  38.6930   -0.4300   -1.10%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│  0.4680   0.0410   -0.4270  -91.24%   464  coq-mathcomp-field/mathcomp/field/separable.v.html                                        │
│  0.4050   0.0040   -0.4010  -99.01%   170  coq-mathcomp-solvable/mathcomp/solvable/alt.v.html                                        │
│  0.3760   0.0030   -0.3730  -99.20%  1556  coq-mathcomp-solvable/mathcomp/solvable/abelian.v.html                                    │
│  0.3710   0.0020   -0.3690  -99.46%   187  coq-mathcomp-solvable/mathcomp/solvable/jordanholder.v.html                               │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[coqbot-app]

🔴 CI failures at commit d1e2548 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 241e2fa succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-hott, ci-unimath

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

performance-tests-lite timedout in the bench, in Reify/CanonicalStructures/_2_SuperFast.v AFAICT (the bench runs each package with a 3h timeout)
mathcomp-character failed producing a 3.7GiB log full of Debug [unification] messages, the end of the log says

- File "./inertia.v", line 933, characters 2-6:
- Error: The reference STOP was not found in the current environment.
- 
- Command exited with non-zero status 1
- inertia.vo (real: 3995.19, user: 3961.49, sys: 33.47, mem: 1484984 ko)

it seems the only files tried where

- mxrepresentation.vo (real: 17.75, user: 17.56, sys: 0.19, mem: 922884 ko)
- classfun.vo (real: 12.10, user: 11.92, sys: 0.17, mem: 949400 ko)
- character.vo (real: 14.61, user: 14.44, sys: 0.16, mem: 916728 ko)
- inertia.vo (real: 3995.19, user: 3961.49, sys: 33.47, mem: 1484984 ko)

[Tragicus]

Oh, sorry, fixed, and thank you. There is no need to restart the bench, there are several issues to investigate already.

[Tragicus]

This should be ready for the CI, and if everything goes well a bench.

[ppedrot]

@coqbot run full ci

[Tragicus]

It looks like my overlay is wrong. What name should I give instead of odd-order?

[ppedrot]

Did you use the script to generate the overlays or did you copy-paste this from other files? Otherwise the projects are oddorder and hott respectively.

[Tragicus]

I did not know about the script, which actually appears at least twice in the documentation, so thank you.

[gares]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                       coq-fiat-core │   55.49    56.18  -1.23 │   336470944098    336408576927   0.02 │  468236   468456  -0.05 │
│                         coq-coqutil │   41.54    41.84  -0.72 │   263581420058    263544639916   0.01 │  555004   554620   0.07 │
│                    coq-math-classes │   83.86    84.04  -0.21 │   516216257731    516253848517  -0.01 │  504560   505056  -0.10 │
│               coq-engine-bench-lite │  127.93   128.20  -0.21 │   965498238639    965692417118  -0.02 │ 1058400  1058564  -0.02 │
│                            coq-corn │  673.40   674.74  -0.20 │  4662357327308   4656448720325   0.13 │  691104   738600  -6.43 │
│                    coq-fiat-parsers │  273.79   274.25  -0.17 │  2129620274030   2129243214611   0.02 │ 2273188  2276860  -0.16 │
│                          coq-stdlib │  347.80   348.18  -0.11 │  1214703125301   1214564500899   0.01 │  625036   624444   0.09 │
│ coq-neural-net-interp-computed-lite │  233.77   233.95  -0.08 │  2251728299380   2251675158522   0.00 │  852620   851792   0.10 │
│                            coq-core │  133.34   133.42  -0.06 │   540339460167    539727016820   0.11 │  479180   480336  -0.24 │
│                             coq-vst │  855.65   855.56   0.01 │  6465110946260   6464865820756   0.00 │ 1687360  1680276   0.42 │
│                        coq-compcert │  301.01   300.97   0.01 │  1990019888399   1990565348138  -0.03 │ 1091544  1089884   0.15 │
│          coq-performance-tests-lite │  905.47   904.96   0.06 │  7310034933726   7303419246523   0.09 │ 2439296  2439140   0.01 │
│                           coq-verdi │   43.94    43.85   0.21 │   295723523267    295652893961   0.02 │  523464   524284  -0.16 │
│                           coq-color │  242.77   242.09   0.28 │  1536791883831   1537160565668  -0.02 │ 1136596  1136940  -0.03 │
│                         coq-bignums │   29.76    29.66   0.34 │   189873776339    189875375233  -0.00 │  468228   469012  -0.17 │
│                   coq-iris-examples │  395.87   394.33   0.39 │  2653758511765   2650846764347   0.11 │ 1083968  1071904   1.13 │
│                      coq-verdi-raft │  537.91   534.66   0.61 │  3746880976043   3746610588691   0.01 │  830988   830972   0.00 │
│                        coq-bedrock2 │  326.10   324.05   0.63 │  2766383093518   2766375143020   0.00 │  862696   862732  -0.00 │
│                        coq-coqprime │   51.97    51.55   0.81 │   357264460808    357282524467  -0.01 │  781044   781188  -0.02 │
│                         coq-unimath │ 1474.45  1460.32   0.97 │ 12186602565391  12106387491320   0.66 │ 1107280  1112588  -0.48 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-hott
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-equations
coq-rewriter

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-mathcomp-analysis (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-utils (dependency coq-equations failed)
coq-metacoq-common (dependency coq-equations 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-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SLOW DOWNS                                                      │
│                                                                                                                             │
│   OLD      NEW      DIFF     %DIFF     Ln                  FILE                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.0030    1.3140  1.3110  43700.00%   238  coq-unimath/UniMath/CategoryTheory/Limits/Filtered.v.html                       │
│ 62.2290   63.0790  0.8500      1.37%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                     │
│ 46.5520   47.2550  0.7030      1.51%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 36.1370   36.8060  0.6690      1.85%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                    │
│  0.0850    0.7340  0.6490    763.53%   556  coq-unimath/UniMath/AlgebraicTheories/RepresentationTheorem.v.html              │
│  0.0010    0.6100  0.6090  60900.00%   110  coq-unimath/UniMath/CategoryTheory/Limits/StandardDiagrams.v.html               │
│  0.0010    0.6090  0.6080  60800.00%   107  coq-unimath/UniMath/CategoryTheory/Limits/StandardDiagrams.v.html               │
│ 99.4830  100.0170  0.5340      0.54%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 25.0900   25.5490  0.4590      1.83%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 99.5570  100.0110  0.4540      0.46%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 25.0300   25.4820  0.4520      1.81%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 32.9050   33.3340  0.4290      1.30%   147  coq-vst/veric/expr_lemmas4.v.html                                               │
│ 46.2480   46.6700  0.4220      0.91%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                      │
│  0.1950    0.5940  0.3990    204.62%   934  coq-unimath/UniMath/AlgebraicTheories/CategoryOfRetracts.v.html                 │
│ 11.1820   11.5470  0.3650      3.26%   410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html            │
│ 31.9390   32.2650  0.3260      1.02%   194  coq-vst/veric/expr_lemmas4.v.html                                               │
│  0.2910    0.6070  0.3160    108.59%   199  coq-unimath/UniMath/CategoryTheory/Categories/StandardCategories.v.html         │
│ 16.8740   17.1840  0.3100      1.84%    32  coq-performance-tests-lite/src/pattern.v.html                                   │
│  4.5180    4.8230  0.3050      6.75%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│ 20.0080   20.2940  0.2860      1.43%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 18.5320   18.8110  0.2790      1.51%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html               │
│  0.1450    0.4120  0.2670    184.14%   290  coq-unimath/UniMath/AlgebraicTheories/Examples/EndomorphismTheory.v.html        │
│ 14.9250   15.1830  0.2580      1.73%  1505  coq-vst/floyd/VSU.v.html                                                        │
│ 17.3450   17.5890  0.2440      1.41%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                       │
│  0.3810    0.6240  0.2430     63.78%   870  coq-stdlib/MSets/MSetRBT.v.html                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                              │
│                                                                                                                                           │
│   OLD       NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  43.0820   42.1710  -0.9110    -2.11%  834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│   0.7080    0.3180  -0.3900   -55.08%  868  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.9120    0.6900  -0.2220   -24.34%  205  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                      │
│   1.9950    1.7760  -0.2190   -10.98%   25  coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html                                       │
│   5.3150    5.1080  -0.2070    -3.89%  198  coq-compcert/x86/Op.v.html                                                                    │
│   1.6970    1.5010  -0.1960   -11.55%  313  coq-stdlib/Strings/Byte.v.html                                                                │
│ 199.9390  199.7440  -0.1950    -0.10%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   0.8300    0.6700  -0.1600   -19.28%  813  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   7.9220    7.7640  -0.1580    -1.99%   31  coq-performance-tests-lite/src/pattern.v.html                                                 │
│   0.4060    0.2710  -0.1350   -33.25%  650  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.4240    0.2910  -0.1330   -31.37%  637  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   4.3540    4.2230  -0.1310    -3.01%  428  coq-compcert/lib/Heaps.v.html                                                                 │
│   0.3500    0.2190  -0.1310   -37.43%  445  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                                           │
│   4.3420    4.2180  -0.1240    -2.86%  623  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   1.2250    1.1020  -0.1230   -10.04%   21  coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html                                       │
│   0.2950    0.1770  -0.1180   -40.00%   16  coq-stdlib/Numbers/HexadecimalZ.v.html                                                        │
│   3.5620    3.4440  -0.1180    -3.31%  490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                    │
│   1.3810    1.2670  -0.1140    -8.25%  839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                 │
│   0.4380    0.3260  -0.1120   -25.57%  624  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.1080    0.0000  -0.1080  -100.00%  301  coq-vst/concurrency/conclib.v.html                                                            │
│   0.1190    0.0120  -0.1070   -89.92%   72  coq-unimath/UniMath/CategoryTheory/Categories/HSET/SliceFamEquiv.v.html                       │
│   0.1750    0.0700  -0.1050   -60.00%  230  coq-iris-examples/theories/logatom/snapshot/atomic_snapshot.v.html                            │
│   0.1590    0.0560  -0.1030   -64.78%  616  coq-vst/floyd/go_lower.v.html                                                                 │
│   0.6940    0.5920  -0.1020   -14.70%  820  coq-unimath/UniMath/CategoryTheory/Limits/Examples/IsoCommaLimits.v.html                      │
│   0.1010    0.0000  -0.1010  -100.00%   61  coq-iris-examples/theories/spanning_tree/proof.v.html                                         │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[gares]

@coqbot run full ci

[Tragicus]

Should I worry about the macOS failure?

[SkySkimmer]

You can lobby for a quick merge of #19836

[Tragicus]

Well, that was definitely quick. I did not even have time to get there.

[gares]

@coqbot merge now

[coqbot-app]

@gares: You cannot merge this PR because:

• There is still a needs: full CI label.

[gares]

@coqbot merge now

[coqbot-app]

@gares: You can't merge the PR because it hasn't been approved yet.

[gares]

@Tragicus please rebase and I'll merge

[SkySkimmer]

this needs a changelog entry

[pi8027]

I confirm that lemma-overloading.dev compiles with this branch of Coq.

[gares]

@coqbot merge now

[SkySkimmer]

Did this break analysis (example failure https://gitlab.inria.fr/coq/coq/-/jobs/4971156)?

[Tragicus]

Yes, indeed, I opened an overlay at math-comp/analysis#1402.