Add a generic mechanism for rewriting with any equality satisfying J by tabareau · Pull Request #21098 · rocq-prover/rocq

tabareau · 2025-09-19T14:40:49Z

This PR has a mechanism to make rewrite and discrimante parametrized over any equality satisfying reflexivity and Martin-Löf style J eliminator. The (ad-hoc) parametrization is done using typeclass inference.

This PR is on top of #21161 which provides a way to use the typeclass system on a different DB than typeclass_instances. For equality, we use the DB rewrite_instances. This avoids being sensitive to the local content of typeclass_instances.

Instead of having simply on class for J, we support all the variants used by rewrite (e.g., non-dependent, _r , forward, and so on) for backward compatibility.

Note some for some use cases, supporting those variants is crucial for the guard condition as a rewritten term is a substerm only if the rewriting occurs as a direct pattern-matching (hence for instance the tricky definition of eq_rect_r_dep).

Previously, all those subtleties were handle under the hood by generating internal_rew_... scheme on the fly.

We can now rewrite with an equality where the transport is not based on matching (see for instance Observational.v in the test-suite).

For backward compatibility reason, eq_rec_r is now a annotation over eq_rect_r.

Overlays (to be merged before the current PR)

ppedrot · 2025-09-24T13:43:15Z

@coqbot run full ci

tabareau · 2025-09-25T11:44:51Z

@coqbot run full ci

tabareau · 2025-11-14T18:29:16Z

@coqbot run full ci

tabareau · 2025-11-18T16:09:56Z

@coqbot run full ci

tabareau · 2025-11-19T08:52:18Z

@coqbot run full ci

tabareau · 2025-11-19T14:34:48Z

@coqbot run full ci

tabareau · 2025-11-20T13:55:39Z

@coqbot bench

coqbot-app · 2025-11-21T00:17:36Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]   │
│                                     │                         │                                       │                          │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF  │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼──────────────────────────┤
│                            coq-core │    2.93     2.97  -1.35 │    19670110007     19675272102  -0.03 │  106180   106368   -0.18 │
│          rocq-metarocq-translations │   15.32    15.45  -0.84 │   109304518472    108807407636   0.46 │  771964   771964    0.00 │
│                           coq-verdi │   42.56    42.89  -0.77 │   284064417434    284362587074  -0.10 │  527176   525152    0.39 │
│         coq-rewriter-perf-SuperFast │  475.97   477.83  -0.39 │  3727486801851   3728643163030  -0.03 │ 1251548  1241580    0.80 │
│                 coq-category-theory │  577.78   579.89  -0.36 │  4277624378277   4289358264450  -0.27 │  991552   939740    5.51 │
│                        coq-rewriter │  330.19   330.78  -0.18 │  2476620799201   2473900657533   0.11 │ 1501420  1518052   -1.10 │
│                        coq-coqprime │   52.51    52.59  -0.15 │   357894750195    357064484258   0.23 │  820616   821184   -0.07 │
│               coq-engine-bench-lite │  127.99   128.15  -0.12 │   952972150869    948089726725   0.51 │ 1084144  1108320   -2.18 │
│        coq-fiat-crypto-with-bedrock │ 7190.02  7192.21  -0.03 │ 59551676987819  59494498115087   0.10 │ 3132344  3271764   -4.26 │
│                         coq-coqutil │   45.97    45.97   0.00 │   286196285575    285577114232   0.22 │  560824   565096   -0.76 │
│                       coq-fiat-core │   54.05    54.04   0.02 │   330842298977    330058849238   0.24 │  481652   481804   -0.03 │
│                 rocq-metarocq-utils │   23.51    23.50   0.04 │   152552462991    152163573311   0.26 │  592464   591124    0.23 │
│                        coq-bedrock2 │  350.44   350.29   0.04 │  2908865002570   2907480415980   0.05 │  833304   830924    0.29 │
│                         coq-unimath │ 1783.37  1781.36   0.11 │ 14804385815258  14791084548535   0.09 │ 1114320  1095540    1.71 │
│                    coq-fiat-parsers │  273.58   273.08   0.18 │  2105062360157   2103102893107   0.09 │ 2033828  2343192  -13.20 │
│                           coq-color │  229.45   229.03   0.18 │  1447524340475   1443205356546   0.30 │ 1150752  1151948   -0.10 │
│                   coq-iris-examples │  365.64   364.91   0.20 │  2408634803194   2401256788039   0.31 │ 1119436  1123676   -0.38 │
│                        rocq-bignums │   24.70    24.65   0.20 │   157579827226    156932922677   0.41 │  458052   456376    0.37 │
│                    coq-math-classes │   82.66    82.48   0.22 │   500598537691    500008570689   0.12 │  516716   516848   -0.03 │
│                      coq-verdi-raft │  497.57   496.35   0.25 │  3428563527142   3415172040345   0.39 │  820824   821908   -0.13 │
│                rocq-metarocq-common │   40.34    40.24   0.25 │   259872594796    259270063943   0.23 │  893592   895600   -0.22 │
│               rocq-metarocq-erasure │  474.75   473.36   0.29 │  3245979264361   3240334432061   0.17 │ 1934016  1803908    7.21 │
│                        rocq-runtime │   74.01    73.79   0.30 │   536029197145    535919951249   0.02 │  510576   512340   -0.34 │
│          coq-performance-tests-lite │  901.84   898.93   0.32 │  7255865638171   7252460406627   0.05 │ 2202656  2204300   -0.07 │
│                 rocq-metarocq-pcuic │  626.64   623.98   0.43 │  4000758069003   3981172527589   0.49 │ 2510352  1892896   32.62 │
│           rocq-metarocq-safechecker │  310.48   308.94   0.50 │  2322111336414   2313370339197   0.38 │ 1884860  1864128    1.11 │
│              rocq-metarocq-template │   81.54    81.08   0.57 │   561965495833    558411810440   0.64 │ 1021968  1026096   -0.40 │
│                        coq-compcert │  299.74   298.03   0.57 │  1963400241261   1949220085562   0.73 │ 1164116  1158224    0.51 │
│                             coq-vst │  832.35   827.03   0.64 │  6304994635980   6274938404794   0.48 │ 2147376  2003776    7.17 │
│                      rocq-equations │    8.54     8.48   0.71 │    58358787983     58138147793   0.38 │  398640   396704    0.49 │
│                         rocq-stdlib │  445.14   440.93   0.95 │  1539214480915   1534038980246   0.34 │  628200   633632   -0.86 │
│ coq-neural-net-interp-computed-lite │  236.67   234.41   0.96 │  2264730085384   2264124673044   0.03 │  847836   849016   -0.14 │
│                           rocq-core │    6.70     6.60   1.52 │    41405248132     40989962618   1.01 │  456640   457352   -0.16 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-hott (in NEW)
rocq-elpi (in NEW)

rocq-mathcomp-boot (dependency rocq-elpi failed)
rocq-mathcomp-order (dependency rocq-elpi failed)
rocq-mathcomp-ssreflect (dependency rocq-elpi failed)
rocq-mathcomp-fingroup (dependency rocq-elpi failed)
rocq-mathcomp-algebra (dependency rocq-elpi failed)
rocq-mathcomp-solvable (dependency rocq-elpi failed)
rocq-mathcomp-field (dependency rocq-elpi failed)
rocq-mathcomp-character (dependency rocq-elpi failed)
coq-mathcomp-odd-order (dependency rocq-elpi failed)
coq-mathcomp-analysis (dependency rocq-elpi failed)
coq-corn (dependency rocq-elpi failed)
coq-coquelicot (dependency rocq-elpi failed)
coq-fourcolor (dependency rocq-elpi failed)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                      │
│  OLD     NEW     DIFF    %DIFF    Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    199     201  2.1591    1.08%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│ 31.994  34.148  2.1540    6.73%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│   63.6    65.5  1.8356    2.88%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│   23.3    25.0  1.6496    7.07%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                         │
│   94.7    95.7  1.0085    1.06%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  38.96  39.582  0.6220    1.60%   834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│   42.6    43.2  0.6118    1.44%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                       │
│   3.26    3.87  0.6035   18.49%   557  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│   94.8    95.3  0.4873    0.51%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   82.7    83.1  0.4097    0.50%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│   44.7    45.1  0.4060    0.91%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html           │
│   8.56    8.96  0.3947    4.61%  1154  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/SymbolicProofs.v.html                   │
│   1.79    2.19  0.3946   22.04%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
│  0.431   0.825  0.3938   91.33%   300  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                            │
│  0.171   0.517  0.3462  202.18%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                │
│  0.299   0.644  0.3451  115.58%   719  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│   21.5    21.9  0.3333    1.55%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│   36.3    36.6  0.3157    0.87%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│  3.847   4.161  0.3140    8.16%   477  coq-vst/veric/expr_lemmas3.v.html                                                             │
│   2.06    2.36  0.2981   14.47%   469  rocq-metarocq-safechecker/safechecker/theories/PCUICEqualityDec.v.html                        │
│   6.45    6.75  0.2977    4.62%   476  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html               │
│   42.2    42.4  0.2891    0.69%   246  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                  │
│   12.3    12.6  0.2771    2.26%   505  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v.html │
│   10.1    10.3  0.2768    2.75%   417  coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html             │
│   30.3    30.6  0.2733    0.90%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html          │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│  OLD     NEW     DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    180     175  -4.8737   -2.70%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   6.59    5.22  -1.3740  -20.84%   130  coq-category-theory/Functor/Strong/Product.v.html                                                       │
│   2.57    1.35  -1.2205  -47.55%   549  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                           │
│    237     236  -0.9321   -0.39%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│ 35.189  34.349  -0.8400   -2.39%   147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│ 34.098   33.37  -0.7280   -2.14%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│   64.8    64.3  -0.5370   -0.83%   716  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                   │
│   4.55    4.02  -0.5294  -11.64%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                    │
│   94.1    93.5  -0.5173   -0.55%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│   30.9    30.4  -0.4708   -1.53%   225  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                            │
│    134     133  -0.4701   -0.35%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│   2.76    2.33  -0.4366  -15.80%   240  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│    119     119  -0.4216   -0.35%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│   15.1    14.7  -0.4171   -2.77%   841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   31.3    30.9  -0.4155   -1.33%   334  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                              │
│   25.3    24.9  -0.3863   -1.53%   226  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                            │
│   1.51    1.13  -0.3741  -24.83%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                               │
│   2.61    2.24  -0.3715  -14.24%   275  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│   38.6    38.2  -0.3714   -0.96%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│   63.8    63.4  -0.3671   -0.58%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   36.4    36.1  -0.3294   -0.91%   224  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                            │
│   42.2    41.9  -0.3207   -0.76%   223  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                            │
│   38.2    38.0  -0.2818   -0.74%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                          │
│   19.8    19.5  -0.2810   -1.42%   227  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                            │
│  0.604   0.330  -0.2744  -45.41%     1  rocq-stdlib/theories/Reals/Cauchy/ConstructiveExtra.v.html                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

tabareau · 2025-11-21T09:50:04Z

@coqbot run full ci

tabareau · 2025-11-21T11:02:39Z

@coqbot run full ci

tabareau · 2025-11-21T17:43:06Z

@coqbot run full ci

tabareau · 2025-11-22T15:41:28Z

@ppedrot The PR is ready for review.
I fixed the Bedrock2 issue (see mit-plv/bedrock2#503),
but the CI still seems to be running on the previous commit.
No more performance problems.

JasonGross · 2025-11-22T18:57:45Z

bedrock2 should be automatically bumped in rupicola and then in fiat-crypto within the next 24h, then the update will show here

ppedrot · 2025-11-24T09:51:35Z

@coqbot run full ci

ppedrot · 2025-11-24T09:52:33Z

@coqbot bench

coqbot-app · 2025-11-24T23:08:38Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]   │
│                                     │                         │                                       │                          │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF  │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼──────────────────────────┤
│              rocq-mathcomp-fingroup │   26.14    26.49  -1.32 │   172228288732    171997013588   0.13 │  602892   602972   -0.01 │
│                 rocq-metarocq-utils │   23.43    23.71  -1.18 │   153326481916    152992701968   0.22 │  591224   588804    0.41 │
│                      coq-coquelicot │   44.52    44.96  -0.98 │   265794388677    265634025527   0.06 │  847892   842188    0.68 │
│          rocq-metarocq-translations │   15.31    15.43  -0.78 │   109645143095    109103144835   0.50 │  773032   775088   -0.27 │
│                           coq-verdi │   42.80    43.06  -0.60 │   285256349605    284284694468   0.34 │  527844   529580   -0.33 │
│                    coq-math-classes │   82.44    82.87  -0.52 │   501530357354    500669698625   0.17 │  514424   515148   -0.14 │
│                           coq-color │  229.07   230.18  -0.48 │  1451910423428   1448285235208   0.25 │ 1151732  1135884    1.40 │
│                         rocq-stdlib │  442.93   444.95  -0.45 │  1540813513121   1535106258346   0.37 │  626592   631180   -0.73 │
│               coq-engine-bench-lite │  127.53   128.08  -0.43 │   949176337701    946420304955   0.29 │ 1085016  1084512    0.05 │
│                            coq-corn │  647.83   650.50  -0.41 │  4375173236900   4369765281450   0.12 │  743148   734756    1.14 │
│ coq-neural-net-interp-computed-lite │  236.23   237.13  -0.38 │  2266039810168   2265360325870   0.03 │  843984   848144   -0.49 │
│                      coq-verdi-raft │  496.24   497.22  -0.20 │  3431847809875   3417340146299   0.42 │  819468   818744    0.09 │
│             rocq-mathcomp-character │  100.04   100.23  -0.19 │   712017741063    712186142946  -0.02 │ 2129168  2130724   -0.07 │
│                         coq-unimath │ 1781.98  1785.31  -0.19 │ 14818837737191  14801411271561   0.12 │ 1112456  1097736    1.34 │
│                       coq-fiat-core │   54.50    54.60  -0.18 │   333427065656    332740247129   0.21 │  481944   481848    0.02 │
│                        coq-rewriter │  331.78   332.34  -0.17 │  2477567679309   2475158647548   0.10 │ 1439800  1439768    0.00 │
│                 rocq-metarocq-pcuic │  625.19   626.24  -0.17 │  3997105946972   3982789198767   0.36 │ 1837644  1894672   -3.01 │
│               rocq-metarocq-erasure │  473.95   474.66  -0.15 │  3246378298315   3235304802852   0.34 │ 1927576  1799228    7.13 │
│                   coq-iris-examples │  364.46   364.92  -0.13 │  2410154591241   2401717682395   0.35 │ 1131592  1126752    0.43 │
│         coq-rewriter-perf-SuperFast │  478.72   479.26  -0.11 │  3730069233458   3728088466776   0.05 │ 1281864  1262724    1.52 │
│        coq-fiat-crypto-with-bedrock │ 7209.64  7217.72  -0.11 │ 59568866047948  59502930243986   0.11 │ 3152960  3186192   -1.04 │
│                        coq-coqprime │   52.54    52.59  -0.10 │   359010450680    358176667819   0.23 │  822676   822584    0.01 │
│          coq-performance-tests-lite │  902.00   902.81  -0.09 │  7259060496174   7252286695012   0.09 │ 2205628  2203896    0.08 │
│                  rocq-mathcomp-boot │   38.81    38.84  -0.08 │   230297540778    229921241254   0.16 │  746464   746608   -0.02 │
│                        coq-bedrock2 │  351.02   351.20  -0.05 │  2910833415528   2909423083985   0.05 │  840376   823444    2.06 │
│                rocq-metarocq-common │   40.35    40.36  -0.02 │   260277562847    259637550402   0.25 │  896372   894064    0.26 │
│             rocq-mathcomp-ssreflect │    1.15     1.15   0.00 │     8148624756      8145364321   0.04 │  861408   861412   -0.00 │
│                 coq-category-theory │  582.54   582.34   0.03 │  4295172965385   4291984418531   0.07 │  918500   919208   -0.08 │
│              rocq-metarocq-template │   81.66    81.62   0.05 │   563265474132    559387357295   0.69 │ 1038180  1035432    0.27 │
│              rocq-mathcomp-solvable │  103.29   103.22   0.07 │   716510901469    715563052938   0.13 │ 1525036  1525200   -0.01 │
│                       coq-fourcolor │ 1365.98  1364.41   0.12 │ 12555257865949  12551905805280   0.03 │ 1404828  1403612    0.09 │
│           rocq-metarocq-safechecker │  312.42   311.95   0.15 │  2326875013448   2318350666814   0.37 │ 1885732  1880644    0.27 │
│                        rocq-bignums │   24.95    24.91   0.16 │   157771810285    157155773979   0.39 │  461608   462256   -0.14 │
│                        rocq-runtime │   74.38    74.24   0.19 │   538259810476    537930072191   0.06 │  514560   514516    0.01 │
│              coq-mathcomp-odd-order │  602.69   601.54   0.19 │  4346988939184   4344393790713   0.06 │ 3393192  3394224   -0.03 │
│                         coq-coqutil │   46.23    46.14   0.20 │   288426865757    287334179899   0.38 │  565284   563104    0.39 │
│                    coq-fiat-parsers │  275.98   275.24   0.27 │  2109975054482   2107842237089   0.10 │ 2033928  2348064  -13.38 │
│                        coq-compcert │  299.82   298.86   0.32 │  1965499084587   1951176292818   0.73 │ 1159768  1289632  -10.07 │
│               rocq-mathcomp-algebra │  329.39   327.43   0.60 │  2433360327125   2431601147091   0.07 │ 2057264  2049104    0.40 │
│                             coq-vst │  834.72   829.67   0.61 │  6310309092582   6277472255354   0.52 │ 2149492  2163656   -0.65 │
│                 rocq-mathcomp-field │  190.03   188.69   0.71 │  1426838968664   1427376460582  -0.04 │ 2787176  2796784   -0.34 │
│               coq-mathcomp-analysis │ 1055.60  1046.88   0.83 │  7897660124663   7896354586971   0.02 │ 2586616  2584972    0.06 │
│                 rocq-mathcomp-order │   82.30    81.54   0.93 │   601781255497    601849180366  -0.01 │ 2059740  2059832   -0.00 │
│                           rocq-elpi │   15.88    15.72   1.02 │   111846043987    111613658752   0.21 │  572880   572648    0.04 │
│                      rocq-equations │    8.71     8.61   1.16 │    59892407330     59722789394   0.28 │  397964   397660    0.08 │
│                           rocq-core │    6.76     6.63   1.96 │    41517304266     41052456328   1.13 │  455048   456436   -0.30 │
│                            coq-core │    2.86     2.80   2.14 │    19675506442     19685680833  -0.05 │  106392   106364    0.03 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-hott (in NEW)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD      NEW     DIFF     %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   31.976  33.552  1.5760      4.93%   97  coq-vst/veric/binop_lemmas5.v.html                                                                      │
│      176     177  1.4110      0.80%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   38.878  39.742  0.8640      2.22%  834  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│     94.5    95.3  0.7826      0.83%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│      236     237  0.7805      0.33%  141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│     94.8    95.5  0.7139      0.75%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│     44.2    44.9  0.6290      1.42%  578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│     82.4    83.1  0.6197      0.75%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│   0.0167   0.613  0.5962   3569.25%  263  coq-mathcomp-analysis/theories/hoelder.v.html                                                           │
│     32.1    32.7  0.5850      1.82%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     31.1    31.6  0.5682      1.83%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     31.0    31.6  0.5626      1.81%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     30.8    31.4  0.5621      1.82%  139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     30.9    31.4  0.5550      1.80%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     30.9    31.4  0.5323      1.72%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│     31.0    31.5  0.5288      1.71%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│ 0.000923   0.513  0.5126  55532.94%  219  coq-mathcomp-analysis/theories/ess_sup_inf.v.html                                                       │
│ 0.000889   0.492  0.4908  55205.96%  464  coq-mathcomp-analysis/theories/normedtype_theory/ereal_normedtype.v.html                                │
│ 0.000779   0.486  0.4855  62317.20%   36  coq-mathcomp-analysis/theories/measure_theory/dirac_measure.v.html                                      │
│     30.8    31.3  0.4819      1.56%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│    33.64  34.086  0.4460      1.33%  194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│   34.753  35.168  0.4150      1.19%  147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│     21.6    22.0  0.3843      1.78%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│     36.9    37.3  0.3779      1.02%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  0.00276   0.369  0.3665  13268.43%   88  rocq-mathcomp-field/field/finfield.v.html                                                               │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SPEED UPS                                                              │
│                                                                                                                                            │
│  OLD     NEW      DIFF     %DIFF   Ln                     FILE                                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   202       200  -1.2010   -0.60%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│  12.1      11.0  -1.0892   -9.03%  194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                           │
│  64.8      63.7  -1.0740   -1.66%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│   119       119  -0.8236   -0.69%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│  59.9      59.1  -0.8029   -1.34%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                           │
│  52.5      51.7  -0.7778   -1.48%  526  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│  93.9      93.3  -0.6548   -0.70%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                        │
│  29.8      29.2  -0.6369   -2.14%  715  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│  19.0      18.4  -0.6189   -3.26%   31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                          │
│  64.7      64.1  -0.5792   -0.90%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│  7.74      7.21  -0.5385   -6.95%  602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html     │
│  65.0      64.5  -0.5019   -0.77%  716  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                              │
│  13.4      12.9  -0.4942   -3.69%  269  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                      │
│  45.3      44.9  -0.4939   -1.09%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                │
│ 0.494  0.000483  -0.4930  -99.90%  465  coq-mathcomp-analysis/theories/normedtype_theory/ereal_normedtype.v.html                           │
│  1.80      1.35  -0.4435  -24.69%   70  rocq-mathcomp-algebra/algebra/qpoly.v.html                                                         │
│  24.1      23.7  -0.3993   -1.66%   85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                             │
│  1.16     0.775  -0.3856  -33.22%  215  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                 │
│  36.8      36.4  -0.3779   -1.03%  553  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│ 0.532     0.156  -0.3758  -70.67%  586  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│  4.40      4.02  -0.3755   -8.54%  199  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                        │
│ 0.750     0.375  -0.3749  -49.97%   14  rocq-stdlib/theories/extraction/ExtrOcamlZBigInt.v.html                                            │
│ 0.369   0.00175  -0.3669  -99.53%   89  rocq-mathcomp-field/field/finfield.v.html                                                          │
│  45.4      45.0  -0.3668   -0.81%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                   │
│  7.45      7.08  -0.3623   -4.87%  604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

tabareau · 2025-11-25T09:58:46Z

@coqbot run full ci

tabareau · 2025-11-26T14:22:18Z

@coqbot run full ci

tabareau · 2025-11-26T14:28:22Z

@coqbot run full ci

ppedrot · 2025-11-27T14:53:57Z

@coqbot merge now

coqbot-app · 2025-11-27T14:54:03Z

@ppedrot: Please take care of the following overlays:

21098-tabareau-sortpoly-equality.sh

tabareau requested review from a team as code owners September 19, 2025 14:40

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 19, 2025

tabareau marked this pull request as draft September 19, 2025 15:05

tabareau force-pushed the sortpoly-equality branch 10 times, most recently from 5d85858 to 04fdca3 Compare September 24, 2025 13:41

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 24, 2025

tabareau force-pushed the sortpoly-equality branch from 04fdca3 to 9e27b8c Compare September 25, 2025 09:03

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 25, 2025

tabareau force-pushed the sortpoly-equality branch 4 times, most recently from a30387b to 428b37f Compare September 25, 2025 09:46

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 25, 2025

tabareau marked this pull request as ready for review September 25, 2025 11:58

tabareau requested review from a team as code owners September 25, 2025 11:58

tabareau force-pushed the sortpoly-equality branch from 428b37f to e8c319f Compare September 25, 2025 12:59

ppedrot reviewed Nov 13, 2025

View reviewed changes

Comment thread tactics/equality.ml Outdated

ppedrot reviewed Nov 13, 2025

View reviewed changes

Comment thread tactics/equality.ml Outdated

tabareau mentioned this pull request Nov 20, 2025

add overlay (backward compat) mit-plv/kami#45

Merged

ppedrot reviewed Nov 26, 2025

View reviewed changes

Comment thread test-suite/success/RegisterScheme.v Outdated

ppedrot reviewed Nov 26, 2025

View reviewed changes

Comment thread tactics/tactics.ml Outdated

ppedrot reviewed Nov 26, 2025

View reviewed changes

Comment thread plugins/ssr/ssrequality.ml Outdated

ppedrot reviewed Nov 26, 2025

View reviewed changes

Comment thread tactics/equality.ml Outdated

add a generic mechanism for rewriting with any equality satisfying J

b635f87

ppedrot approved these changes Nov 26, 2025

View reviewed changes

This was referenced Nov 27, 2025

Adapt with respect to rocq-prover/rocq#21098 HoTT/Coq-HoTT#2331

Merged

Adapt with respect to rocq-prover/rocq#21371 HoTT/Coq-HoTT#2332

Merged

Uh oh!

Conversation

tabareau commented Sep 19, 2025 • edited by proux01 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Overlays (to be merged before the current PR)

Uh oh!

ppedrot commented Sep 24, 2025

Uh oh!

tabareau commented Sep 25, 2025

Uh oh!

Uh oh!

Uh oh!

tabareau commented Nov 14, 2025

Uh oh!

tabareau commented Nov 18, 2025

Uh oh!

tabareau commented Nov 19, 2025

Uh oh!

tabareau commented Nov 19, 2025

Uh oh!

tabareau commented Nov 20, 2025

Uh oh!

coqbot-app Bot commented Nov 21, 2025

Uh oh!

tabareau commented Nov 21, 2025

Uh oh!

tabareau commented Nov 21, 2025

Uh oh!

tabareau commented Nov 21, 2025

Uh oh!

tabareau commented Nov 22, 2025

Uh oh!

JasonGross commented Nov 22, 2025

Uh oh!

ppedrot commented Nov 24, 2025

Uh oh!

ppedrot commented Nov 24, 2025

Uh oh!

coqbot-app Bot commented Nov 24, 2025

Uh oh!

tabareau commented Nov 25, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tabareau commented Nov 26, 2025

Uh oh!

tabareau commented Nov 26, 2025

Uh oh!

ppedrot commented Nov 27, 2025

Uh oh!

coqbot-app Bot commented Nov 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

tabareau commented Sep 19, 2025 •

edited by proux01

Loading