Fix FIrrelevant conversion in RR by yannl35133 · Pull Request #19414 · rocq-prover/rocq

yannl35133 · 2024-07-23T13:39:28Z

Overlays:

Adapt to rocq-prover/rocq#19414 (abstract CClosure.usubs) Mtac2/Mtac2#432 (backwards compatible)

yannl35133 · 2024-09-13T11:06:23Z

@coqbot run full ci

coqbot-app · 2025-03-05T02:28:41Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2026-01-12T02:47:53Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

ppedrot · 2026-05-05T15:07:23Z

@coqbot bench

coqbot-app · 2026-05-06T01:58:31Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│             rocq-mathcomp-ssreflect │    1.04     1.06  -1.89 │     6785351807      6789552393  -0.06 │  589720   589828  -0.02 │
│                        rocq-bignums │   25.46    25.70  -0.93 │   163759567391    163747400175   0.01 │  458536   458748  -0.05 │
│                    coq-math-classes │   83.40    83.99  -0.70 │   508230943047    508168889195   0.01 │  514188   513768   0.08 │
│                         rocq-stdlib │  436.00   438.18  -0.50 │  1564302254584   1563959477083   0.02 │  646712   648736  -0.31 │
│                        rocq-runtime │   75.79    76.15  -0.47 │   549649941037    549456191057   0.04 │  493916   493784   0.03 │
│                       coq-fiat-core │   56.05    56.25  -0.36 │   341835910745    341680135473   0.05 │  483032   484876  -0.38 │
│                            coq-corn │  669.30   670.99  -0.25 │  4501823694624   4499585503641   0.05 │  718560   754616  -4.78 │
│                         coq-unimath │ 1866.17  1870.28  -0.22 │ 15288487083606  15253996370450   0.23 │ 1085868  1062212   2.23 │
│ coq-neural-net-interp-computed-lite │  236.26   236.77  -0.22 │  2267131080794   2266977662528   0.01 │  897072   894800   0.25 │
│                   coq-iris-examples │  370.20   370.98  -0.21 │  2419500644212   2422396762246  -0.12 │ 1115232  1113196   0.18 │
│                           coq-color │  233.13   233.59  -0.20 │  1481497262147   1481660697562  -0.01 │ 1169688  1170496  -0.07 │
│                      coq-coquelicot │   40.00    40.04  -0.10 │   244041005963    243454389046   0.24 │  829644   835112  -0.65 │
│                  rocq-mathcomp-boot │   39.20    39.21  -0.03 │   230629793185    230638028967  -0.00 │  640968   637660   0.52 │
│                 rocq-mathcomp-order │   81.25    81.26  -0.01 │   598628349239    598372863232   0.04 │ 1581812  1579796   0.13 │
│                            coq-core │    2.68     2.68   0.00 │    18566691570     18564360358   0.01 │   90716    90840  -0.14 │
│                           coq-verdi │   44.01    43.99   0.05 │   293352129119    293067185685   0.10 │  520048   526352  -1.20 │
│          coq-performance-tests-lite │  902.52   902.00   0.06 │  7247331534896   7241059249639   0.09 │ 1267904  1269768  -0.15 │
│                        coq-coqprime │   53.58    53.49   0.17 │   365574170364    365193720095   0.10 │  821920   824024  -0.26 │
│                        coq-bedrock2 │  361.05   360.26   0.22 │  3005431599550   2999439058245   0.20 │  874528   882036  -0.85 │
│                         coq-coqutil │   47.43    47.32   0.23 │   293785442597    293688488594   0.03 │  569792   569344   0.08 │
│                            coq-hott │  158.03   157.64   0.25 │  1065419492966   1065562813335  -0.01 │  466740   462232   0.98 │
│        coq-fiat-crypto-with-bedrock │ 7342.51  7319.57   0.31 │ 60351895172455  60196439400591   0.26 │ 3057644  3093180  -1.15 │
│                        coq-rewriter │  334.15   333.00   0.35 │  2480834862827   2477630647271   0.13 │ 1550660  1546716   0.25 │
│                      coq-verdi-raft │  500.24   498.27   0.40 │  3450649414656   3446490809840   0.12 │  834888   823612   1.37 │
│               coq-engine-bench-lite │  129.42   128.88   0.42 │   962316047688    959336813296   0.31 │ 1005328  1005364  -0.00 │
│                    coq-fiat-parsers │  280.40   279.03   0.49 │  2146397514274   2136367539469   0.47 │ 2304712  2328700  -1.03 │
│                           rocq-core │    6.87     6.83   0.59 │    41545282424     41546997385  -0.00 │  446880   446056   0.18 │
│                           rocq-elpi │   16.31    16.16   0.93 │   116014085496    115987423165   0.02 │  448956   448924   0.01 │
│         coq-rewriter-perf-SuperFast │  489.81   474.36   3.26 │  3779943557222   3731323908232   1.30 │ 1302988  1260888   3.34 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-fingroup (in NEW)
coq-compcert (dependency install failed in NEW)
rocq-equations (in NEW)

rocq-mathcomp-algebra (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-field (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-character (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-fingroup failed)
rocq-metarocq-utils (dependency rocq-equations failed)
rocq-metarocq-common (dependency rocq-equations failed)
rocq-metarocq-template (dependency rocq-equations failed)
rocq-metarocq-pcuic (dependency rocq-equations failed)
rocq-metarocq-safechecker (dependency rocq-equations failed)
rocq-metarocq-erasure (dependency rocq-equations failed)
rocq-metarocq-translations (dependency rocq-equations failed)
coq-fourcolor (dependency rocq-mathcomp-fingroup failed)
coq-vst (dependency coq-compcert failed)
coq-category-theory (dependency rocq-equations failed)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                   TOP 25 SLOW DOWNS                                                    │
│                                                                                                                        │
│  OLD   NEW    DIFF   %DIFF   Ln                   FILE                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  5.53  7.18  1.6465  29.78%  217  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│   236   238  1.5103   0.64%  141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html           │
│  55.2  56.5  1.2696   2.30%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html             │
│   107   108  1.1726   1.09%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html               │
│  34.3  35.5  1.1674   3.40%  898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                 │
│  17.7  18.8  1.0446   5.89%   31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                            │
│  36.7  37.7  1.0257   2.79%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                         │
│  31.1  32.1  0.9833   3.16%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  32.4  33.4  0.9826   3.03%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  31.2  32.1  0.9490   3.04%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  31.3  32.2  0.8754   2.80%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  31.3  32.2  0.8678   2.77%  139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  31.3  32.1  0.8488   2.71%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  31.4  32.2  0.8329   2.65%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│  2.46  3.29  0.8310  33.83%   34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html               │
│  26.4  27.2  0.7920   3.00%  794  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                 │
│  31.3  32.1  0.7907   2.53%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │
│   133   134  0.7434   0.56%  155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html           │
│  26.9  27.6  0.7191   2.67%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html         │
│  26.6  27.3  0.7093   2.67%   34  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │
│  28.7  29.4  0.6516   2.27%  145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html         │
│  15.3  16.0  0.6475   4.23%  898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                 │
│  28.5  29.1  0.5745   2.02%   31  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │
│  15.0  15.6  0.5595   3.73%  841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html              │
│ 0.827  1.34  0.5104  61.70%  408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                            │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SPEED UPS                                                          │
│                                                                                                                                    │
│  OLD    NEW    DIFF     %DIFF   Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  94.2   93.1  -1.1021   -1.17%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  84.4   83.5  -0.9178   -1.09%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│  51.2   50.5  -0.6937   -1.36%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│  56.7   56.1  -0.6267   -1.11%  516  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│  22.3   21.6  -0.6230   -2.80%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│  93.6   93.1  -0.5279   -0.56%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  10.7   10.3  -0.4132   -3.85%  743  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│ 0.656  0.283  -0.3730  -56.88%  374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                │
│  64.5   64.1  -0.3513   -0.54%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│  9.13   8.78  -0.3451   -3.78%  453  coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html                                    │
│   201    200  -0.3280   -0.16%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  22.3   22.0  -0.2831   -1.27%  520  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│  24.5   24.2  -0.2748   -1.12%  345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                            │
│  22.0   21.8  -0.2613   -1.18%  338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│ 0.570  0.310  -0.2596  -45.58%   14  rocq-stdlib/theories/ZArith/auxiliary.v.html                                                  │
│ 0.551  0.296  -0.2553  -46.34%   14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                          │
│  35.9   35.6  -0.2538   -0.71%  195  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  1.32   1.07  -0.2530  -19.17%   89  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                         │
│ 0.521  0.270  -0.2513  -48.22%   12  rocq-stdlib/theories/ZArith/Znumtheory.v.html                                                 │
│ 0.716  0.465  -0.2512  -35.09%   59  rocq-stdlib/theories/ZArith/Zeuclid.v.html                                                    │
│  13.7   13.4  -0.2493   -1.82%  930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html         │
│  9.55   9.30  -0.2450   -2.57%  950  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html         │
│ 0.547  0.303  -0.2437  -44.54%   19  rocq-stdlib/theories/ZArith/Int.v.html                                                        │
│ 0.480  0.252  -0.2273  -47.39%  707  rocq-stdlib/theories/MSets/MSetList.v.html                                                    │
│ 0.512  0.307  -0.2045  -39.98%   11  rocq-stdlib/theories/omega/OmegaLemmas.v.html                                                 │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

yannl35133 · 2026-05-06T12:46:54Z

@coqbot bench

coqbot-app · 2026-05-06T23:18:19Z

🏁 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.71     2.81  -3.56 │    18569473029     18603838298  -0.18 │   90760    90884  -0.14 │
│               coq-engine-bench-lite │  129.25   129.86  -0.47 │   963138634191    963063718811   0.01 │ 1105616  1005840   9.92 │
│                           rocq-elpi │   16.21    16.28  -0.43 │   116183317281    116125541479   0.05 │  448576   448368   0.05 │
│                         coq-coqutil │   47.36    47.48  -0.25 │   292804183590    292642199742   0.06 │  564060   565020  -0.17 │
│                        rocq-bignums │   25.27    25.32  -0.20 │   159913197176    159834629032   0.05 │  463300   458280   1.10 │
│          coq-performance-tests-lite │  902.11   903.04  -0.10 │  7231010504239   7226325252947   0.06 │ 1324652  1308032   1.27 │
│                      coq-coquelicot │   39.29    39.33  -0.10 │   237485005742    236933491441   0.23 │  830048   830144  -0.01 │
│               rocq-metarocq-erasure │  477.23   477.52  -0.06 │  3261098949274   3262902241599  -0.06 │ 1817048  1786400   1.72 │
│ coq-neural-net-interp-computed-lite │  236.60   236.58   0.01 │  2266346991632   2266569795104  -0.01 │  881076   881136  -0.01 │
│              rocq-metarocq-template │   83.35    83.31   0.05 │   569925104628    569677541185   0.04 │ 1088668  1086712   0.18 │
│                 rocq-metarocq-pcuic │  649.33   648.96   0.06 │  4125165111825   4123674366337   0.04 │ 2473792  2510816  -1.47 │
│                    coq-math-classes │   83.05    82.95   0.12 │   502407167775    502313211052   0.02 │  514452   514200   0.05 │
│                           coq-color │  231.93   231.62   0.13 │  1468006339020   1467183056342   0.06 │ 1165588  1165736  -0.01 │
│                  rocq-mathcomp-boot │   39.33    39.25   0.20 │   231368725040    231342657802   0.01 │  658356   659960  -0.24 │
│                      rocq-equations │    8.56     8.54   0.23 │    58697633773     58666589103   0.05 │  399936   400340  -0.10 │
│                        rocq-runtime │   76.33    76.15   0.24 │   550584310756    550404106218   0.03 │  494492   495472  -0.20 │
│                    coq-fiat-parsers │  278.21   277.43   0.28 │  2125915431823   2124490726974   0.07 │ 2265392  2270248  -0.21 │
│                        coq-coqprime │   53.26    53.09   0.32 │   362733419387    362541186889   0.05 │  824132   825752  -0.20 │
│                           coq-verdi │   43.63    43.49   0.32 │   290168858315    289784050531   0.13 │  535292   526532   1.66 │
│           rocq-metarocq-safechecker │  345.24   344.13   0.32 │  2521664096966   2516390711335   0.21 │ 1857908  1854400   0.19 │
│                   coq-iris-examples │  367.55   366.32   0.34 │  2389386169091   2393366070721  -0.17 │ 1092380  1086192   0.57 │
│                            coq-hott │  159.90   159.34   0.35 │  1073483277518   1073806677290  -0.03 │  462048   467836  -1.24 │
│                       coq-fiat-core │   56.05    55.84   0.38 │   340000902316    339789169685   0.06 │  483000   482956   0.01 │
│                 rocq-mathcomp-order │   82.07    81.76   0.38 │   600402621721    600162369742   0.04 │ 1596156  1588656   0.47 │
│        coq-fiat-crypto-with-bedrock │ 7329.83  7301.92   0.38 │ 60187975191028  60056314461205   0.22 │ 3006348  2994060   0.41 │
│                      coq-verdi-raft │  497.28   495.23   0.41 │  3430848852418   3426905704309   0.12 │  832524   814400   2.23 │
│                 coq-category-theory │  556.84   554.06   0.50 │  4052242698137   4052281703891  -0.00 │  911808   926356  -1.57 │
│                        coq-rewriter │  334.62   332.68   0.58 │  2475797738513   2471468837972   0.18 │ 1499432  1468932   2.08 │
│                rocq-metarocq-common │   41.18    40.94   0.59 │   263366400209    263071360837   0.11 │  896324   894468   0.21 │
│                            coq-corn │  664.68   659.89   0.73 │  4435756947452   4435239402276   0.01 │  731236   772892  -5.39 │
│                           rocq-core │    6.88     6.83   0.73 │    41656159189     41644830394   0.03 │  443704   445288  -0.36 │
│                         rocq-stdlib │  440.00   436.39   0.83 │  1555252403064   1554533591551   0.05 │  632476   630364   0.34 │
│             rocq-mathcomp-ssreflect │    1.13     1.12   0.89 │     7128395030      7134636023  -0.09 │  585884   587628  -0.30 │
│                         coq-unimath │ 1849.35  1831.17   0.99 │ 15292007318010  15258801098721   0.22 │ 1098968  1095348   0.33 │
│                        coq-bedrock2 │  364.32   359.43   1.36 │  2995403951623   2990414818828   0.17 │  833928   838716  -0.57 │
│                 rocq-metarocq-utils │   24.47    24.11   1.49 │   157281084043    157277114743   0.00 │  587440   591208  -0.64 │
│         coq-rewriter-perf-SuperFast │  491.24   477.23   2.94 │  3768305623908   3714936296400   1.44 │ 1272348  1242588   2.40 │
│          rocq-metarocq-translations │   16.80    15.74   6.73 │   117231462148    111091180814   5.53 │  900288   781356  15.22 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-fingroup (in NEW)
coq-compcert (dependency install failed in NEW)

rocq-mathcomp-algebra (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-field (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-character (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-fingroup failed)
coq-fourcolor (dependency rocq-mathcomp-fingroup failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                      │
│  OLD   NEW    DIFF    %DIFF   Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  54.2  59.6  5.4675   10.09%  296  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                │
│  63.5  67.4  3.8787    6.11%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│  30.8  32.5  1.7521    5.70%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  30.9  32.5  1.5896    5.14%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  30.8  32.3  1.5474    5.03%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  30.9  32.4  1.5170    4.91%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  31.0  32.5  1.5028    4.85%  139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  30.9  32.4  1.4750    4.77%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  32.1  33.6  1.4441    4.50%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  30.9  32.3  1.3868    4.49%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html              │
│  82.4  83.5  1.1272    1.37%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│ 0.401  1.42  1.0203  254.31%  547  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                     │
│  2.46  3.30  0.8335   33.85%   34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│  48.4  49.3  0.8242    1.70%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│  25.2  26.0  0.8200    3.25%  550  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  34.0  34.7  0.7210    2.12%  898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                              │
│  42.3  43.0  0.7090    1.68%  221  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                      │
│  36.4  37.0  0.6697    1.84%  222  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                      │
│  24.2  24.9  0.6566    2.71%  550  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                   │
│  14.8  15.5  0.6392    4.30%  841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                           │
│ 0.892  1.52  0.6290   70.56%  572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                         │
│  21.5  22.2  0.6216    2.89%  651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                         │
│  42.9  43.4  0.5467    1.27%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                           │
│  7.26  7.76  0.4985    6.86%  294  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                │
│  30.7  31.2  0.4796    1.56%  223  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│  OLD    NEW    DIFF     %DIFF    Ln                     FILE                                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  7.22   5.53  -1.6896  -23.40%   217  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  95.1   93.7  -1.4209   -1.49%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  94.9   93.6  -1.2853   -1.35%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  1.99  0.986  -1.0087  -50.57%   546  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  38.8   38.1  -0.7323   -1.89%   276  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                       │
│  43.9   43.2  -0.6970   -1.59%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│  51.8   51.2  -0.6425   -1.24%   571  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  2.45   1.89  -0.5658  -23.06%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                      │
│  46.7   46.2  -0.4964   -1.06%   278  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  36.3   35.8  -0.4625   -1.27%   195  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  8.14   7.77  -0.3739   -4.59%  1831  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│ 0.595  0.227  -0.3675  -61.78%    18  rocq-stdlib/theories/micromega/VarMap.v.html                                                     │
│  44.3   43.9  -0.3482   -0.79%   257  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  2.50   2.16  -0.3404  -13.59%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│ 0.689  0.368  -0.3207  -46.55%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                   │
│  26.6   26.3  -0.3168   -1.19%    62  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html                                   │
│  14.2   13.9  -0.3165   -2.22%   216  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                         │
│  31.0   30.7  -0.3081   -0.99%   596  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
│  4.34   4.04  -0.3059   -7.04%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                             │
│ 0.521  0.243  -0.2783  -53.43%     4  rocq-stdlib/theories/extraction/ExtrHaskellZInt.v.html                                           │
│  9.80   9.52  -0.2727   -2.78%    87  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                            │
│  38.6   38.3  -0.2645   -0.68%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                   │
│ 0.923  0.666  -0.2564  -27.79%   214  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│  44.8   44.5  -0.2517   -0.56%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                 │
│  59.1   58.8  -0.2452   -0.41%   659  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

… call term_of_fconstr

SkySkimmer · 2026-05-28T12:25:48Z

@coqbot run full ci

Adapt to rocq-prover/rocq#19414 (abstract CClosure.usubs)

yannl35133 added kind: fix This fixes a bug or incorrect documentation. part: kernel needs: merge of dependency This PR depends on another PR being merged first. part: rewrite rules labels Jul 23, 2024

yannl35133 requested a review from a team as a code owner July 23, 2024 13:39

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 Jul 23, 2024

yannl35133 force-pushed the fix-firrelevant-conversion branch from 6dbb97d to c8264d6 Compare July 23, 2024 14:14

yannl35133 force-pushed the fix-firrelevant-conversion branch from c8264d6 to 704d5ae Compare September 5, 2024 14:49

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 6, 2024

yannl35133 force-pushed the fix-firrelevant-conversion branch from 704d5ae to 6313ceb Compare September 6, 2024 13:18

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 6, 2024

yannl35133 removed the needs: merge of dependency This PR depends on another PR being merged first. label Sep 6, 2024

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 13, 2024

ppedrot reviewed Sep 19, 2024

View reviewed changes

Comment thread kernel/cClosure.mli Outdated

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 18, 2024

yannl35133 force-pushed the fix-firrelevant-conversion branch from 6313ceb to 0cc47b6 Compare November 21, 2024 14:31

coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Nov 21, 2024

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 3, 2025

coqbot-app Bot added the stale This PR will be closed unless it is rebased. label Mar 5, 2025

yannl35133 force-pushed the fix-firrelevant-conversion branch from 0cc47b6 to 91524bd Compare March 5, 2025 18:21

coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Mar 5, 2025

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 17, 2025

yannl35133 force-pushed the fix-firrelevant-conversion branch from 91524bd to 53678c5 Compare July 22, 2025 11:34

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 22, 2025

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Dec 11, 2025

SkySkimmer reviewed Apr 29, 2026

View reviewed changes

Comment thread kernel/cClosure.ml Outdated

SkySkimmer reviewed Apr 29, 2026

View reviewed changes

Comment thread kernel/cClosure.ml Outdated

yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

yannl35133 force-pushed the fix-firrelevant-conversion branch from 745e6f6 to 09a1000 Compare April 29, 2026 16:03

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 1, 2026

yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label May 5, 2026

yannl35133 force-pushed the fix-firrelevant-conversion branch from 09a1000 to 8df8790 Compare May 5, 2026 12:58

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 5, 2026

ppedrot self-assigned this May 5, 2026

yannl35133 added a commit to Yann-Leray/Mtac2 that referenced this pull request May 5, 2026

Adapt to rocq-prover/rocq#19414 (abstract CClosure.usubs)

4d7a655

yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2026

yannl35133 force-pushed the fix-firrelevant-conversion branch from 8df8790 to 4b34d7f Compare May 6, 2026 12:42

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2026

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 20, 2026

yannl35133 added 3 commits May 27, 2026 16:40

Add higher-order substitution to CClosure so that rewrite rules don't…

d0e1343

… call term_of_fconstr

Add test case

d725029

overlay

3ce4f06

yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label May 27, 2026

yannl35133 force-pushed the fix-firrelevant-conversion branch from 4b34d7f to 3ce4f06 Compare May 27, 2026 14:44

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 27, 2026

SkySkimmer added this to the 9.3+rc1 milestone May 28, 2026

Janno added a commit to Mtac2/Mtac2 that referenced this pull request May 28, 2026

Merge pull request #432 from Yann-Leray/fix-firrelevant-conversion

ae651c5

Adapt to rocq-prover/rocq#19414 (abstract CClosure.usubs)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix FIrrelevant conversion in RR#19414

Fix FIrrelevant conversion in RR#19414
yannl35133 wants to merge 3 commits into
rocq-prover:masterfrom
Yann-Leray:fix-firrelevant-conversion

yannl35133 commented Jul 23, 2024 •

edited

Loading

Uh oh!

yannl35133 commented Sep 13, 2024

Uh oh!

Uh oh!

coqbot-app Bot commented Mar 5, 2025

Uh oh!

coqbot-app Bot commented Jan 12, 2026

Uh oh!

Uh oh!

Uh oh!

ppedrot commented May 5, 2026

Uh oh!

coqbot-app Bot commented May 6, 2026

Uh oh!

yannl35133 commented May 6, 2026

Uh oh!

coqbot-app Bot commented May 6, 2026

Uh oh!

SkySkimmer commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

yannl35133 commented Jul 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

yannl35133 commented Sep 13, 2024

Uh oh!

Uh oh!

coqbot-app Bot commented Mar 5, 2025

Uh oh!

coqbot-app Bot commented Jan 12, 2026

Uh oh!

Uh oh!

Uh oh!

ppedrot commented May 5, 2026

Uh oh!

coqbot-app Bot commented May 6, 2026

Uh oh!

yannl35133 commented May 6, 2026

Uh oh!

coqbot-app Bot commented May 6, 2026

Uh oh!

SkySkimmer commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

yannl35133 commented Jul 23, 2024 •

edited

Loading