Stop "optimizing" schemes by reusing preexisting schemes in Type for other sorts by SkySkimmer · Pull Request #21241 · rocq-prover/rocq

SkySkimmer · 2025-10-28T14:19:24Z

Overlays (backwards compatible):

Adapt to rocq-prover/rocq#21241 (byte_rec not defined from byte_rect) stdlib#221
Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined from eq_rect) mit-plv/bbv#55
Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined from eq_rect) mit-plv/kami#44
Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect) mit-plv/bedrock2#498

not backwards compatible:

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect) rocq-community/coq-dpdgraph#154

SkySkimmer · 2025-10-28T14:20:01Z

We just remove the Print byte_rec (and also Print byte_ind) since it's useless AFAICT We keep Print byte_rect since that lets us see the output for each byte

… from eq_rect)

Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined from eq_rect)

coqbot-app · 2025-10-29T00:07:58Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-neural-net-interp-computed-lite │  236.00   239.01  -1.26 │  2264973148238   2264942833139   0.00 │  845036   850440  -0.64 │
│                rocq-metarocq-common │   41.10    41.42  -0.77 │   266911500892    266636821784   0.10 │  912384   910220   0.24 │
│                           rocq-core │    6.48     6.53  -0.77 │    40718916850     40685816175   0.08 │  454084   454804  -0.16 │
│                         coq-coqutil │   46.30    46.62  -0.69 │   289668884388    289538813880   0.04 │  559904   562848  -0.52 │
│              rocq-mathcomp-fingroup │   25.64    25.81  -0.66 │   167579977030    167598318375  -0.01 │  565288   565360  -0.01 │
│                 rocq-mathcomp-order │   83.50    84.02  -0.62 │   607363026889    607468982489  -0.02 │ 1517016  1535552  -1.21 │
│              coq-mathcomp-odd-order │  567.82   571.25  -0.60 │  4102832502774   4104178681605  -0.03 │ 2624384  2633256  -0.34 │
│                            coq-corn │  664.20   667.96  -0.56 │  4555493609468   4555623879900  -0.00 │  730420   731620  -0.16 │
│           rocq-metarocq-safechecker │  314.45   316.07  -0.51 │  2362726639605   2360763455375   0.08 │ 1875676  1873312   0.13 │
│              rocq-mathcomp-solvable │   94.44    94.80  -0.38 │   647752096392    647693354145   0.01 │ 1123044  1121236   0.16 │
│                      rocq-equations │    8.55     8.58  -0.35 │    59259752488     59230376021   0.05 │  398004   396528   0.37 │
│                    coq-math-classes │   82.88    83.14  -0.31 │   502737977243    502653902301   0.02 │  517048   516596   0.09 │
│               coq-mathcomp-analysis │  921.55   924.33  -0.30 │  6864653202238   6862633717251   0.03 │ 1966388  1966584  -0.01 │
│                        coq-rewriter │  340.00   340.94  -0.28 │  2532990944145   2533226635330  -0.01 │ 1281460  1277500   0.31 │
│               rocq-mathcomp-algebra │  298.43   299.24  -0.27 │  2202977767136   2202954529253   0.00 │ 1496172  1494864   0.09 │
│                 rocq-mathcomp-field │  169.51   169.91  -0.24 │  1282960909130   1283351332336  -0.03 │ 2051096  2051264  -0.01 │
│                           coq-color │  229.80   230.33  -0.23 │  1457469673747   1455640088210   0.13 │ 1129840  1130344  -0.04 │
│         coq-rewriter-perf-SuperFast │  481.84   482.73  -0.18 │  3759552973755   3758853845371   0.02 │ 1264112  1273944  -0.77 │
│                        coq-compcert │  297.36   297.90  -0.18 │  1943013060661   1944524537172  -0.08 │ 1265604  1193232   6.07 │
│               rocq-metarocq-erasure │  472.99   473.76  -0.16 │  3245229800358   3243302929507   0.06 │ 1911616  1905308   0.33 │
│                             coq-vst │  841.75   843.12  -0.16 │  6377891857282   6377017783224   0.01 │ 2004048  2210912  -9.36 │
│                    coq-fiat-parsers │  274.73   275.12  -0.14 │  2115071855249   2115247977333  -0.01 │ 2351996  2347068   0.21 │
│             rocq-mathcomp-character │   92.67    92.80  -0.14 │   648013548859    648073249272  -0.01 │ 1625296  1625260   0.00 │
│                        coq-coqprime │   52.67    52.74  -0.13 │   358852543530    358809607046   0.01 │  806060   806208  -0.02 │
│                 coq-category-theory │  580.78   581.50  -0.12 │  4293093139794   4291534910311   0.04 │  971148   970824   0.03 │
│                   coq-iris-examples │  369.60   370.04  -0.12 │  2441995825599   2442313982075  -0.01 │ 1147564  1144240   0.29 │
│                      coq-coquelicot │   44.12    44.16  -0.09 │   261546474276    261537451222   0.00 │  832296   832096   0.02 │
│                 rocq-metarocq-pcuic │  627.87   628.24  -0.06 │  4006652468020   4003180774568   0.09 │ 1891000  1879404   0.62 │
│                       coq-fourcolor │ 1345.46  1345.51  -0.00 │ 12416351070295  12416272234155   0.00 │  966872   966912  -0.00 │
│                         coq-unimath │ 1779.73  1778.20   0.09 │ 14821348903037  14821128224196   0.00 │ 1064776  1068860  -0.38 │
│                      coq-verdi-raft │  497.27   496.75   0.10 │  3445131727938   3444779240525   0.01 │  821396   820724   0.08 │
│                       coq-fiat-core │   54.89    54.79   0.18 │   334573054589    334639809653  -0.02 │  481384   483852  -0.51 │
│                  rocq-mathcomp-boot │   38.25    38.18   0.18 │   225918326177    225838996053   0.04 │  659756   659788  -0.00 │
│                            coq-hott │  158.17   157.80   0.23 │  1086790943163   1086423441012   0.03 │  468516   468572  -0.01 │
│               coq-engine-bench-lite │  125.08   124.75   0.26 │   937222151185    934847598188   0.25 │  989720   990464  -0.08 │
│              rocq-metarocq-template │   82.17    81.95   0.27 │   563330603444    562250570366   0.19 │ 1044236  1025436   1.83 │
│                        rocq-bignums │   25.00    24.93   0.28 │   157954232739    157951492114   0.00 │  455868   456836  -0.21 │
│          coq-performance-tests-lite │  903.10   900.57   0.28 │  7271860310134   7270254915471   0.02 │ 2194356  2194396  -0.00 │
│                           coq-verdi │   42.75    42.62   0.31 │   283955124380    283915770370   0.01 │  525984   526144  -0.03 │
│                            coq-core │    2.85     2.84   0.35 │    19662354806     19661695939   0.00 │  103968   104432  -0.44 │
│                        rocq-runtime │   73.56    73.29   0.37 │   534225795457    534295698572  -0.01 │  509672   511000  -0.26 │
│          rocq-metarocq-translations │   15.57    15.51   0.39 │   109894371433    109733671421   0.15 │  779676   771320   1.08 │
│                         rocq-stdlib │  442.95   440.75   0.50 │  1533286613557   1533234494934   0.00 │  624364   630688  -1.00 │
│                 rocq-metarocq-utils │   23.90    23.68   0.93 │   153691378787    153609350121   0.05 │  587092   587440  -0.06 │
│             rocq-mathcomp-ssreflect │    1.06     1.04   1.92 │     7197333847      7191768073   0.08 │  598388   598268   0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-elpi (dependency install failed in NEW)
coq-bedrock2 (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                            │
│   OLD     NEW    DIFF     %DIFF    Ln                     FILE                                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.271  0.982  0.7103    261.62%   12  rocq-stdlib/theories/MSets/MSets.v.html                                                            │
│    3.90   4.59  0.6951     17.83%  492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                               │
│    21.5   22.1  0.6387      2.97%  651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                          │
│    19.1   19.7  0.5896      3.08%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                  │
│    1.04   1.47  0.4371     42.21%  813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                          │
│    48.4   48.8  0.3499      0.72%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│    7.01   7.36  0.3471      4.95%  604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│   0.258  0.576  0.3189    123.79%   11  rocq-stdlib/theories/Numbers/DecimalString.v.html                                                  │
│    1.42   1.74  0.3123     21.92%   75  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                                              │
│   0.338  0.646  0.3081     91.26%   18  rocq-stdlib/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v.html                                   │
│   1.065  1.366  0.3010     28.26%  937  coq-vst/veric/binop_lemmas2.v.html                                                                 │
│   0.291  0.568  0.2772     95.41%   13  rocq-stdlib/theories/micromega/ZCoeff.v.html                                                       │
│    16.4   16.7  0.2674      1.63%   32  coq-performance-tests-lite/src/pattern.v.html                                                      │
│  0.0184  0.285  0.2669   1450.64%  384  coq-mathcomp-analysis/theories/topology_theory/compact.v.html                                      │
│   0.223  0.487  0.2646    118.75%   14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                               │
│   0.361  0.622  0.2618     72.61%    1  rocq-stdlib/theories/Reals/Cauchy/ConstructiveExtra.v.html                                         │
│   0.247  0.504  0.2572    104.11%   13  rocq-stdlib/theories/ZArith/Zmax.v.html                                                            │
│ 0.00216  0.244  0.2417  11173.56%   76  coq-mathcomp-odd-order/theories/PFsection2.v.html                                                  │
│    17.8   18.0  0.2342      1.32%  670  coq-performance-tests-lite/src/Nia.v.html                                                          │
│    9.89   10.1  0.2319      2.35%  496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                       │
│    1.43   1.66  0.2273     15.87%  313  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│    1.99   2.21  0.2171     10.91%    2  coq-mathcomp-analysis/theories/homotopy_theory/homotopy.v.html                                     │
│    11.6   11.8  0.2038      1.75%  388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html           │
│   0.262  0.464  0.2027     77.44%   13  rocq-stdlib/theories/QArith/Qreduction.v.html                                                      │
│ 0.00620  0.199  0.1924   3105.57%  137  coq-mathcomp-odd-order/theories/BGsection1.v.html                                                  │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD      NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    203       201  -2.8562   -1.40%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   1.66      1.08  -0.5746  -34.68%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                     │
│   3.08      2.58  -0.4999  -16.21%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│   39.1      38.7  -0.4240   -1.08%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│  0.681     0.280  -0.4004  -58.83%    16  rocq-stdlib/theories/Structures/OrdersEx.v.html                                               │
│   8.40      8.01  -0.3840   -4.57%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│   1.05     0.730  -0.3228  -30.66%    41  rocq-stdlib/theories/ZArith/Zdiv_facts.v.html                                                 │
│   1.36      1.04  -0.3187  -23.52%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│  0.266  0.000448  -0.2659  -99.83%   383  coq-mathcomp-analysis/theories/topology_theory/compact.v.html                                 │
│  0.359    0.0995  -0.2592  -72.26%   638  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│   38.3      38.0  -0.2570   -0.67%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                │
│  0.266    0.0111  -0.2548  -95.82%    75  coq-mathcomp-odd-order/theories/PFsection2.v.html                                             │
│  0.840     0.591  -0.2489  -29.64%   160  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                            │
│  0.561     0.319  -0.2420  -43.17%    36  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│  0.444     0.212  -0.2322  -52.32%   246  rocq-stdlib/theories/Structures/OrdersEx.v.html                                               │
│ 32.157    31.933  -0.2240   -0.70%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│  0.220  0.000469  -0.2193  -99.79%   559  rocq-mathcomp-field/field/closed_field.v.html                                                 │
│   36.6      36.3  -0.2179   -0.60%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│  0.216   0.00130  -0.2152  -99.40%   513  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html                        │
│  0.529     0.315  -0.2144  -40.52%    35  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│  0.217   0.00378  -0.2134  -98.26%   276  coq-mathcomp-odd-order/theories/BGsection5.v.html                                             │
│  0.524     0.311  -0.2126  -40.59%    17  rocq-stdlib/theories/Logic/IndefiniteDescription.v.html                                       │
│  0.642     0.434  -0.2083  -32.44%    83  rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html                                       │
│  0.757     0.551  -0.2068  -27.30%    36  rocq-stdlib/theories/FSets/FSetAVL.v.html                                                     │
│  0.583     0.377  -0.2060  -35.33%    11  rocq-stdlib/theories/Strings/BinaryString.v.html                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

We just remove the Print byte_rec (and also Print byte_ind) since it's useless AFAICT We keep Print byte_rect since that lets us see the output for each byte

SkySkimmer · 2025-10-29T14:47:27Z

(elpi failed in bench because dep menhir is hosted on inria gitlab which was having network trouble, it worked when tried again for mathcomp)

…other sorts

Adapt to rocq-prover/rocq#21241 (byte_rec not defined from byte_rect)

)

SkySkimmer · 2025-11-10T10:27:28Z

All backwards compatible are merged and the submodule stack should be up to date so this is ready @ppedrot

ppedrot · 2025-11-10T10:55:14Z

@coqbot merge now

coqbot-app · 2025-11-10T10:55:19Z

@ppedrot: Please take care of the following overlays:

21241-SkySkimmer-no-opt-schemes.sh

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect)

SkySkimmer requested a review from a team as a code owner October 28, 2025 14:19

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 28, 2025

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

SkySkimmer added the needs: changelog entry This should be documented in doc/changelog. label Oct 28, 2025

rocq-prover deleted a comment from coqbot-app Bot Oct 28, 2025

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 28, 2025

SkySkimmer force-pushed the no-opt-schemes branch from c350660 to 0ac1d25 Compare October 28, 2025 14:30

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

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 28, 2025

SkySkimmer added a commit to SkySkimmer/bbv that referenced this pull request Oct 28, 2025

Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined…

5e98561

… from eq_rect)

SkySkimmer added a commit to SkySkimmer/kami that referenced this pull request Oct 28, 2025

Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined…

188cc3a

… from eq_rect)

SkySkimmer force-pushed the no-opt-schemes branch from 0ac1d25 to 44edb62 Compare October 28, 2025 15:19

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

samuelgruetter added a commit to mit-plv/bbv that referenced this pull request Oct 28, 2025

Merge pull request #55 from SkySkimmer/no-opt-schemes

032537e

Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined from eq_rect)

samuelgruetter added a commit to mit-plv/kami that referenced this pull request Oct 28, 2025

Merge pull request #44 from SkySkimmer/no-opt-schemes

1b42619

Adapt to rocq-prover/rocq#21241 (stop relying on eq_rec being defined from eq_rect)

SkySkimmer added a commit to SkySkimmer/bedrock2 that referenced this pull request Oct 29, 2025

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect)

2cb9c77

SkySkimmer added a commit to SkySkimmer/coq-dpdgraph that referenced this pull request Oct 29, 2025

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect)

af79625

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 29, 2025

SkySkimmer force-pushed the no-opt-schemes branch from 44edb62 to 15f9cdd Compare October 29, 2025 14:35

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

SkySkimmer added a commit to SkySkimmer/bedrock2 that referenced this pull request Oct 30, 2025

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect)

bd87177

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 30, 2025

SkySkimmer force-pushed the no-opt-schemes branch from 15f9cdd to 523f060 Compare October 30, 2025 12:05

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

Stop "optimizing" schemes by reusing preexisting schemes in Type for …

1528055

…other sorts

SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Oct 30, 2025

SkySkimmer added this to the 9.2+rc1 milestone Oct 30, 2025

SkySkimmer force-pushed the no-opt-schemes branch from 523f060 to 1528055 Compare October 30, 2025 13:06

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

SkySkimmer added a commit to rocq-prover/stdlib that referenced this pull request Oct 31, 2025

Merge pull request #221 from SkySkimmer/no-opt-schemes

c6dbe35

Adapt to rocq-prover/rocq#21241 (byte_rec not defined from byte_rect)

ppedrot self-assigned this Nov 3, 2025

andres-erbsen pushed a commit to mit-plv/bedrock2 that referenced this pull request Nov 6, 2025

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect) (#498

461aa20

)

thomas-lamiaux mentioned this pull request Nov 6, 2025

Replace the old code generating eliminators #21259

Merged

6 tasks

ppedrot approved these changes Nov 10, 2025

View reviewed changes

coqbot-app Bot merged commit 1c733b5 into rocq-prover:master Nov 10, 2025
8 checks passed

ppedrot added a commit to rocq-community/coq-dpdgraph that referenced this pull request Nov 10, 2025

Merge pull request #154 from SkySkimmer/no-opt-schemes

544c583

Adapt to rocq-prover/rocq#21241 (eq_rec not defined using eq_rect)

SkySkimmer deleted the no-opt-schemes branch November 12, 2025 10:47

SkySkimmer mentioned this pull request Nov 12, 2025

Extend Scheme command to support custom schemes #21271

Closed

5 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Stop "optimizing" schemes by reusing preexisting schemes in Type for other sorts#21241

Stop "optimizing" schemes by reusing preexisting schemes in Type for other sorts#21241
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:no-opt-schemes

SkySkimmer commented Oct 28, 2025 •

edited

Loading

Uh oh!

SkySkimmer commented Oct 28, 2025

Uh oh!

coqbot-app Bot commented Oct 29, 2025

Uh oh!

SkySkimmer commented Oct 29, 2025

Uh oh!

SkySkimmer commented Nov 10, 2025

Uh oh!

ppedrot commented Nov 10, 2025

Uh oh!

Uh oh!

coqbot-app Bot commented Nov 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

SkySkimmer commented Oct 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Oct 28, 2025

Uh oh!

coqbot-app Bot commented Oct 29, 2025

Uh oh!

SkySkimmer commented Oct 29, 2025

Uh oh!

SkySkimmer commented Nov 10, 2025

Uh oh!

ppedrot commented Nov 10, 2025

Uh oh!

Uh oh!

coqbot-app Bot commented Nov 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

SkySkimmer commented Oct 28, 2025 •

edited

Loading