Skip to content

Add a generic mechanism for rewriting with any equality satisfying J #21098

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Add a generic mechanism for rewriting with any equality satisfying J #21098

wants to merge 9 commits into from
+717 −221

Conversation

@tabareau
Copy link
Contributor

@tabareau tabareau commented Sep 19, 2025 •
edited by proux01
Loading

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)

@tabareau tabareau requested review from a team as code owners September 19, 2025 14:40
@coqbot-app 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 tabareau marked this pull request as draft September 19, 2025 15:05
@tabareau tabareau force-pushed the sortpoly-equality branch 10 times, most recently from 5d85858 to 04fdca3 Compare September 24, 2025 13:41
@ppedrot
Copy link
Member

ppedrot commented Sep 24, 2025

@coqbot run full ci

@coqbot-app 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
@coqbot-app 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 tabareau force-pushed the sortpoly-equality branch 4 times, most recently from a30387b to 428b37f Compare September 25, 2025 09:46
@tabareau
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app 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 tabareau marked this pull request as ready for review September 25, 2025 11:58
@tabareau tabareau requested review from a team as code owners September 25, 2025 11:58
@coqbot-app 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 Oct 23, 2025
@coqbot-app 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 Oct 23, 2025
@tabareau
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app 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 Oct 23, 2025
@tabareau
Copy link
Contributor Author

@coqbot run full ci

@tabareau
Copy link
Contributor Author

@coqbot bench

1 similar comment
@tabareau
Copy link
Contributor Author

@coqbot bench

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 24, 2025

🏁 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 │     7033376641      7034421497  -0.01 │  598596   598412   0.03 │
│                         rocq-stdlib │  438.94   446.50  -1.69 │  1534400992790   1532967680926   0.09 │  628988   624584   0.71 │
│                 rocq-metarocq-utils │   23.43    23.65  -0.93 │   152778581593    152972479380  -0.13 │  590372   587424   0.50 │
│                       coq-fourcolor │ 1346.84  1350.89  -0.30 │ 12418633142135  12414648756267   0.03 │  967624   968584  -0.10 │
│                        rocq-runtime │   73.62    73.75  -0.18 │   534641934657    534405919893   0.04 │  509920   510840  -0.18 │
│          coq-performance-tests-lite │  901.32   901.35  -0.00 │  7267986962951   7269629079982  -0.02 │ 2214528  2192300   1.01 │
│                            coq-core │    2.92     2.92  -0.00 │    19667849263     19659835326   0.04 │  104388   104560  -0.16 │
│              coq-mathcomp-odd-order │  571.76   571.02   0.13 │  4103661278653   4102522149748   0.03 │ 2630864  2631608  -0.03 │
│               coq-mathcomp-analysis │  926.48   925.28   0.13 │  6884268041358   6884467175221  -0.00 │ 1968184  1964544   0.19 │
│                        coq-coqprime │   52.41    52.34   0.13 │   358381183344    357805786506   0.16 │  804392   804116   0.03 │
│                         coq-unimath │ 1778.15  1775.29   0.16 │ 14825622413487  14805325664215   0.14 │ 1059916  1064660  -0.45 │
│              rocq-mathcomp-solvable │   94.74    94.57   0.18 │   647913558997    647245179058   0.10 │ 1123536  1122336   0.11 │
│                       coq-fiat-core │   54.75    54.64   0.20 │   332500698964    331848204248   0.20 │  482928   481584   0.28 │
│                         coq-coqutil │   46.22    46.12   0.22 │   288341665619    287807740338   0.19 │  560332   564836  -0.80 │
│                    coq-math-classes │   82.48    82.29   0.23 │   501546036630    500986311403   0.11 │  515528   515896  -0.07 │
│         coq-rewriter-perf-SuperFast │  482.14   480.92   0.25 │  3759270489853   3757977631790   0.03 │ 1252896  1257772  -0.39 │
│                           rocq-elpi │   15.37    15.33   0.26 │   107668007788    107294723749   0.35 │  560284   559792   0.09 │
│                            coq-corn │  667.02   665.15   0.28 │  4552918967999   4551419521587   0.03 │  736628   729548   0.97 │
│                 rocq-mathcomp-order │   83.89    83.65   0.29 │   607351999236    607285252425   0.01 │ 1535564  1526680   0.58 │
│                  rocq-mathcomp-boot │   38.28    38.17   0.29 │   225785235938    225594174582   0.08 │  660000   662028  -0.31 │
│                           coq-color │  230.14   229.46   0.30 │  1455755452646   1451274458189   0.31 │ 1132384  1128580   0.34 │
│             rocq-mathcomp-character │   92.76    92.48   0.30 │   648023368073    647362709300   0.10 │ 1625496  1623356   0.13 │
│                rocq-metarocq-common │   41.30    41.16   0.34 │   266471916759    266214407777   0.10 │  909732   912244  -0.28 │
│                    coq-fiat-parsers │  275.13   273.84   0.47 │  2111425789884   2107947993189   0.16 │ 2351692  2352012  -0.01 │
│                      coq-coquelicot │   43.10    42.89   0.49 │   256617887776    255796447010   0.32 │  833556   833884  -0.04 │
│                 rocq-mathcomp-field │  170.67   169.76   0.54 │  1283588207296   1283093102919   0.04 │ 2049000  2048628   0.02 │
│                           coq-verdi │   42.64    42.41   0.54 │   283529900429    283059832316   0.17 │  524336   526880  -0.48 │
│               rocq-mathcomp-algebra │  299.51   297.83   0.56 │  2203511117704   2202162010412   0.06 │ 1495332  1497616  -0.15 │
│ coq-neural-net-interp-computed-lite │  236.23   234.80   0.61 │  2263241763619   2263264157981  -0.00 │  845176   850272  -0.60 │
│              rocq-mathcomp-fingroup │   25.79    25.61   0.70 │   167410267657    167239170413   0.10 │  569244   565256   0.71 │
│                        coq-rewriter │  342.41   339.63   0.82 │  2535391383693   2530537472944   0.19 │ 1289616  1271140   1.45 │
│                   coq-iris-examples │  370.68   367.60   0.84 │  2445675989598   2440036590052   0.23 │ 1151872  1142388   0.83 │
│               coq-engine-bench-lite │  125.60   124.51   0.88 │   943165898246    933548733997   1.03 │  988672   990704  -0.21 │
│                 rocq-metarocq-pcuic │  631.05   625.57   0.88 │  4014369810541   4001392033359   0.32 │ 1877436  1879888  -0.13 │
│                             coq-vst │  847.41   839.36   0.96 │  6408836829121   6372114470690   0.58 │ 2267620  2210976   2.56 │
│                        rocq-bignums │   25.16    24.90   1.04 │   159011006453    157953922881   0.67 │  455608   457328  -0.38 │
│           rocq-metarocq-safechecker │  317.87   314.45   1.09 │  2371219570549   2360777822911   0.44 │ 1875620  1878552  -0.16 │
│                      coq-verdi-raft │  499.47   494.06   1.10 │  3454461626202   3441414710425   0.38 │  824212   821660   0.31 │
│                        coq-compcert │  299.64   296.13   1.19 │  1955744702530   1941793364729   0.72 │ 1184660  1192360  -0.65 │
│                           rocq-core │    6.78     6.68   1.50 │    41408257842     40676385674   1.80 │  457688   452744   1.09 │
│                      rocq-equations │    8.71     8.36   4.19 │    59312404714     59069585390   0.41 │  396732   396920  -0.05 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-hott (in NEW)
rocq-metarocq-template (in NEW)
rocq-metarocq-erasure (dependency install failed in NEW)
rocq-metarocq-translations (dependency install failed in NEW)
coq-bedrock2 (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)
coq-category-theory (in NEW)

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                             │
│                                                                                                                                          │
│   OLD      NEW     DIFF     %DIFF     Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   31.929  33.923  1.9940      6.25%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│      200     201  1.7352      0.87%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   41.391  42.468  1.0770      2.60%   834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│    0.404   1.457  1.0530    260.64%   946  coq-vst/veric/binop_lemmas2.v.html                                                            │
│    3.797    4.27  0.4730     12.46%   477  coq-vst/veric/expr_lemmas3.v.html                                                             │
│     16.3    16.7  0.4671      2.87%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                     │
│     38.1    38.5  0.4322      1.14%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                │
│     18.9    19.3  0.4059      2.14%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                             │
│     96.7    97.0  0.3521      0.36%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│     38.7    39.1  0.3361      0.87%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│     2.05    2.37  0.3203     15.63%   469  rocq-metarocq-safechecker/safechecker/theories/PCUICEqualityDec.v.html                        │
│    6.146    6.46  0.3140      5.11%   192  coq-vst/veric/binop_lemmas5.v.html                                                            │
│    0.484   0.787  0.3031     62.61%   597  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│    4.272   4.559  0.2870      6.72%   171  coq-vst/veric/binop_lemmas5.v.html                                                            │
│    0.280   0.552  0.2713     96.80%    19  rocq-stdlib/theories/MSets/MSetFacts.v.html                                                   │
│    0.389   0.649  0.2599     66.79%   615  rocq-stdlib/theories/setoid_ring/Field_theory.v.html                                          │
│    0.333   0.588  0.2545     76.43%     1  rocq-stdlib/theories/ZArith/Zdivisibility.v.html                                              │
│     96.6    96.9  0.2500      0.26%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│    0.417   0.665  0.2489     59.75%     1  rocq-stdlib/theories/btauto/Algebra.v.html                                                    │
│  0.00181   0.241  0.2394  13246.04%   147  rocq-mathcomp-field/field/algnum.v.html                                                       │
│  0.00195   0.239  0.2366  12115.31%   227  rocq-mathcomp-solvable/solvable/extraspecial.v.html                                           │
│     8.13    8.36  0.2347      2.89%  1265  coq-verdi-raft/theories/Raft/CommonTheorems.v.html                                            │
│ 0.000636   0.222  0.2212  34787.42%   232  rocq-mathcomp-field/field/closed_field.v.html                                                 │
│ 0.000562   0.219  0.2182  38826.16%   558  rocq-mathcomp-field/field/closed_field.v.html                                                 │
│    0.349   0.565  0.2163     62.03%    16  rocq-stdlib/theories/extraction/ExtrOcamlIntConv.v.html                                       │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                        TOP 25 SPEED UPS                                                         │
│                                                                                                                                 │
│  OLD      NEW     DIFF     %DIFF    Ln                   FILE                                                                   │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   3.77     3.17  -0.5972  -15.84%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                          │
│   26.4     25.8  -0.5957   -2.25%    12  coq-fourcolor/theories/proof/job466to485.v.html                                        │
│   25.3     24.7  -0.5766   -2.28%    12  coq-fourcolor/theories/proof/job319to322.v.html                                        │
│   22.1     21.6  -0.5724   -2.58%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                              │
│   26.0     25.5  -0.5220   -2.01%    12  coq-fourcolor/theories/proof/job618to622.v.html                                        │
│   4.68     4.23  -0.4588   -9.80%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                   │
│  35.07   34.618  -0.4520   -1.29%   147  coq-vst/veric/expr_lemmas4.v.html                                                      │
│   16.5     16.1  -0.3838   -2.32%    32  coq-performance-tests-lite/src/pattern.v.html                                          │
│   20.9     20.5  -0.3796   -1.81%    12  coq-fourcolor/theories/proof/job283to286.v.html                                        │
│ 34.032   33.661  -0.3710   -1.09%   194  coq-vst/veric/expr_lemmas4.v.html                                                      │
│   1.52     1.17  -0.3534  -23.27%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                              │
│  0.567    0.238  -0.3285  -57.97%   104  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_under.v.html │
│   1.09    0.761  -0.3275  -30.08%   215  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                     │
│   24.5     24.2  -0.3232   -1.32%    12  coq-fourcolor/theories/proof/job231to234.v.html                                        │
│  0.466    0.155  -0.3109  -66.73%   586  rocq-stdlib/theories/Strings/Byte.v.html                                               │
│   8.44     8.13  -0.3085   -3.66%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                      │
│  0.463    0.177  -0.2862  -61.84%   592  rocq-stdlib/theories/MSets/MSetAVL.v.html                                              │
│  0.252  0.00362  -0.2483  -98.56%   148  rocq-mathcomp-field/field/algnum.v.html                                                │
│   3.56     3.31  -0.2449   -6.89%   213  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                     │
│  0.675    0.433  -0.2412  -35.76%    21  rocq-stdlib/theories/FSets/FMapAVL.v.html                                              │
│  0.599    0.358  -0.2410  -40.21%    11  rocq-stdlib/theories/Strings/OctalString.v.html                                        │
│  0.239  0.00268  -0.2366  -98.88%   228  rocq-mathcomp-solvable/solvable/extraspecial.v.html                                    │
│  0.996    0.769  -0.2271  -22.81%   170  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                     │
│   1.21    0.987  -0.2256  -18.60%  2109  rocq-stdlib/theories/FSets/FMapFacts.v.html                                            │
│   31.3     31.0  -0.2254   -0.72%    12  coq-fourcolor/theories/proof/job254to270.v.html                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app 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 Oct 24, 2025
@tabareau
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app 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 Oct 24, 2025
@coqbot-app 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 Oct 24, 2025
@tabareau tabareau requested a review from a team as a code owner October 24, 2025 12:45
@tabareau
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app 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 Oct 24, 2025
@tabareau
Copy link
Contributor Author

@coqbot bench

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 24, 2025

🏁 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.85     2.92  -2.40 │    19702162158     19660151072   0.21 │  104340   104024    0.30 │
│ coq-neural-net-interp-computed-lite │  237.67   238.27  -0.25 │  2263245600100   2263255975236  -0.00 │  850504   844000    0.77 │
│                rocq-metarocq-common │   41.30    41.39  -0.22 │   266467157295    266201485279   0.10 │  911756   912368   -0.07 │
│               rocq-mathcomp-algebra │  299.32   299.80  -0.16 │  2203248066937   2202263563911   0.04 │ 1494064  1493160    0.06 │
│                       coq-fourcolor │ 1347.33  1349.27  -0.14 │ 12418568511495  12414495076039   0.03 │  967812   968432   -0.06 │
│               coq-mathcomp-analysis │  922.79   923.75  -0.10 │  6859062301670   6858188367121   0.01 │ 1970444  1967972    0.13 │
│                  rocq-mathcomp-boot │   38.13    38.14  -0.03 │   225783644745    225580168810   0.09 │  660252   661900   -0.25 │
│                        rocq-runtime │   73.73    73.69   0.05 │   534591289258    534521662138   0.01 │  510244   509040    0.24 │
│                            coq-corn │  667.25   666.42   0.12 │  4552917020154   4551154788975   0.04 │  737608   729864    1.06 │
│              rocq-mathcomp-solvable │   95.02    94.89   0.14 │   647922694891    647248464469   0.10 │ 1123556  1119268    0.38 │
│          coq-performance-tests-lite │  902.46   901.04   0.16 │  7272986595438   7264747281656   0.11 │ 2212936  2193804    0.87 │
│         coq-rewriter-perf-SuperFast │  481.66   480.80   0.18 │  3759551556427   3757324461146   0.06 │ 1295320  1275896    1.52 │
│                         coq-unimath │ 1779.40  1775.27   0.23 │ 14824736691571  14805600227386   0.13 │ 1061168  1066216   -0.47 │
│                           coq-color │  229.59   228.84   0.33 │  1455590519566   1451215026268   0.30 │ 1132708  1129704    0.27 │
│                 rocq-mathcomp-order │   84.17    83.87   0.36 │   607280781107    607244411648   0.01 │ 1534556  1525148    0.62 │
│                      coq-coquelicot │   43.44    43.27   0.39 │   256635972135    255811314996   0.32 │  835216   836636   -0.17 │
│                        coq-coqprime │   52.62    52.40   0.42 │   358458893993    357822152401   0.18 │  806452   803992    0.31 │
│                 rocq-metarocq-utils │   23.61    23.50   0.47 │   152744712949    152993869264  -0.16 │  588344   586260    0.36 │
│             rocq-mathcomp-character │   92.97    92.49   0.52 │   647933786300    647508983050   0.07 │ 1623820  1625016   -0.07 │
│                       coq-fiat-core │   54.56    54.24   0.59 │   332488808958    331799971827   0.21 │  481884   481664    0.05 │
│                   coq-iris-examples │  370.32   367.93   0.65 │  2445591797957   2440069593520   0.23 │ 1151576  1142256    0.82 │
│                    coq-math-classes │   82.66    82.10   0.68 │   501621820483    500958313338   0.13 │  517340   516184    0.22 │
│                         rocq-stdlib │  444.10   441.09   0.68 │  1534268805734   1532906990235   0.09 │  628780   624612    0.67 │
│                        rocq-bignums │   24.97    24.80   0.69 │   158968370683    157948565028   0.65 │  457932   456752    0.26 │
│                    coq-fiat-parsers │  274.85   272.94   0.70 │  2109301992694   2107912529716   0.07 │ 2025248  2349816  -13.81 │
│               coq-engine-bench-lite │  125.16   124.22   0.76 │   937252746717    932569182504   0.50 │  988408   991040   -0.27 │
│                 rocq-metarocq-pcuic │  630.57   625.56   0.80 │  4014337982875   4001475553912   0.32 │ 1875188  1880752   -0.30 │
│                      coq-verdi-raft │  500.10   496.12   0.80 │  3454395568432   3441371974664   0.38 │  823816   823648    0.02 │
│                 rocq-mathcomp-field │  171.37   169.97   0.82 │  1283711455780   1283043003705   0.05 │ 2049252  2048220    0.05 │
│                           rocq-elpi │   15.40    15.27   0.85 │   107654959819    107290718115   0.34 │  560568   560104    0.08 │
│              coq-mathcomp-odd-order │  572.81   567.91   0.86 │  4103965149748   4102697603425   0.03 │ 2632212  2631000    0.05 │
│              rocq-mathcomp-fingroup │   25.81    25.58   0.90 │   167413910346    167218273254   0.12 │  567616   567128    0.09 │
│                             coq-vst │  848.11   840.08   0.96 │  6409073241407   6372137518644   0.58 │ 2267888  2210920    2.58 │
│                        coq-rewriter │  343.50   340.14   0.99 │  2535519418297   2530560099172   0.20 │ 1289060  1271212    1.40 │
│           rocq-metarocq-safechecker │  317.22   314.05   1.01 │  2371102775415   2360721342339   0.44 │ 1875868  1878012   -0.11 │
│                        coq-compcert │  299.91   296.72   1.08 │  1955710176879   1941909209076   0.71 │ 1184608  1190092   -0.46 │
│                           coq-verdi │   42.75    42.24   1.21 │   283564565703    283048426619   0.18 │  523344   531100   -1.46 │
│                           rocq-core │    6.65     6.57   1.22 │    41429277938     40684871464   1.83 │  454544   454432    0.02 │
│                      rocq-equations │    8.61     8.46   1.77 │    59294929891     59073122831   0.38 │  397652   397348    0.08 │
│                         coq-coqutil │   46.57    45.68   1.95 │   288338377116    287807349115   0.18 │  560604   563144   -0.45 │
│             rocq-mathcomp-ssreflect │    1.06     1.03   2.91 │     7031565310      7034411403  -0.04 │  598656   598304    0.06 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-hott (in NEW)
rocq-metarocq-template (in NEW)
rocq-metarocq-erasure (dependency install failed in NEW)
rocq-metarocq-translations (dependency install failed in NEW)
coq-bedrock2 (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)
coq-category-theory (in NEW)

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SLOW DOWNS                                                       │
│                                                                                                                              │
│   OLD      NEW     DIFF     %DIFF    Ln                  FILE                                                                │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   31.852  34.081  2.2290      7.00%   97  coq-vst/veric/binop_lemmas5.v.html                                                 │
│    0.402   1.454  1.0520    261.69%  946  coq-vst/veric/binop_lemmas2.v.html                                                 │
│     38.0    39.0  1.0461      2.75%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html     │
│     16.0    16.8  0.8392      5.26%   32  coq-performance-tests-lite/src/pattern.v.html                                      │
│   41.615  42.337  0.7220      1.73%  834  coq-vst/veric/binop_lemmas4.v.html                                                 │
│     39.1    39.6  0.5556      1.42%  236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html         │
│    3.774   4.297  0.5230     13.86%  477  coq-vst/veric/expr_lemmas3.v.html                                                  │
│     36.5    37.0  0.4687      1.28%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                       │
│     21.2    21.7  0.4577      2.16%  651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                          │
│     2.03    2.38  0.3539     17.47%  469  rocq-metarocq-safechecker/safechecker/theories/PCUICEqualityDec.v.html             │
│     1.96    2.29  0.3257     16.62%    2  coq-mathcomp-analysis/theories/homotopy_theory/homotopy.v.html                     │
│    0.354   0.669  0.3146     88.78%   10  rocq-stdlib/theories/extraction/ExtrHaskellZNum.v.html                             │
│    6.148   6.452  0.3040      4.94%  192  coq-vst/veric/binop_lemmas5.v.html                                                 │
│  0.00376   0.302  0.2987   7953.06%  202  coq-mathcomp-analysis/theories/normedtype_theory/ereal_normedtype.v.html           │
│    0.351   0.649  0.2982     85.01%  249  rocq-stdlib/theories/Structures/OrdersEx.v.html                                    │
│    4.272   4.568  0.2960      6.93%  171  coq-vst/veric/binop_lemmas5.v.html                                                 │
│    0.340   0.630  0.2895     85.05%   12  rocq-stdlib/theories/MSets/MSets.v.html                                            │
│    0.318   0.581  0.2628     82.63%   11  rocq-stdlib/theories/QArith/Qpower.v.html                                          │
│     1.02    1.28  0.2595     25.53%   89  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html              │
│     25.0    25.2  0.2577      1.03%   79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │
│    2.923   3.171  0.2480      8.48%  475  coq-vst/veric/binop_lemmas3.v.html                                                 │
│  0.00179   0.243  0.2415  13470.61%  147  rocq-mathcomp-field/field/algnum.v.html                                            │
│  0.00215   0.240  0.2382  11101.07%  227  rocq-mathcomp-solvable/solvable/extraspecial.v.html                                │
│    0.491   0.727  0.2365     48.18%   13  rocq-stdlib/theories/FSets/FMapPositive.v.html                                     │
│ 0.000630   0.223  0.2226  35337.14%  232  rocq-mathcomp-field/field/closed_field.v.html                                      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SPEED UPS                                                               │
│                                                                                                                                             │
│  OLD      NEW     DIFF     %DIFF    Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    203      203  -0.8314   -0.41%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│   3.31     2.55  -0.7689  -23.20%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                          │
│   1.71     1.12  -0.5880  -34.45%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                          │
│   7.46     6.94  -0.5180   -6.94%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│ 35.093   34.589  -0.5040   -1.44%   147  coq-vst/veric/expr_lemmas4.v.html                                                                  │
│   8.44     7.98  -0.4601   -5.45%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                  │
│   1.57     1.11  -0.4573  -29.19%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                          │
│  0.752    0.341  -0.4110  -54.65%     1  rocq-stdlib/theories/Zmod/ZstarDef.v.html                                                          │
│   3.60     3.20  -0.3978  -11.04%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                      │
│   15.1     14.8  -0.3414   -2.26%    12  coq-fourcolor/theories/proof/job215to218.v.html                                                    │
│   1.85     1.53  -0.3278  -17.68%   313  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│   25.7     25.4  -0.3213   -1.25%    12  coq-fourcolor/theories/proof/job299to302.v.html                                                    │
│  34.03   33.721  -0.3090   -0.91%   194  coq-vst/veric/expr_lemmas4.v.html                                                                  │
│  0.529    0.236  -0.2928  -55.35%    13  rocq-stdlib/theories/micromega/ZCoeff.v.html                                                       │
│  0.477    0.200  -0.2774  -58.14%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                     │
│  0.488    0.226  -0.2629  -53.83%    19  rocq-stdlib/theories/ZArith/Int.v.html                                                             │
│   7.55     7.29  -0.2603   -3.45%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html     │
│ 15.439    15.19  -0.2490   -1.61%  1209  coq-vst/floyd/Component.v.html                                                                     │
│  0.252  0.00376  -0.2480  -98.51%   148  rocq-mathcomp-field/field/algnum.v.html                                                            │
│   25.6     25.3  -0.2460   -0.96%    12  coq-fourcolor/theories/proof/job291to294.v.html                                                    │
│  0.534    0.290  -0.2443  -45.76%    36  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                          │
│   25.6     25.4  -0.2398   -0.94%    12  coq-fourcolor/theories/proof/job223to226.v.html                                                    │
│  0.240  0.00267  -0.2369  -98.89%   228  rocq-mathcomp-solvable/solvable/extraspecial.v.html                                                │
│   26.2     26.0  -0.2295   -0.87%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  0.686    0.465  -0.2213  -32.24%    60  rocq-stdlib/theories/Numbers/DecimalString.v.html                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 25, 2025

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                      rocq-equations │    8.47     8.59  -1.40 │    59276494955     59063839488   0.36 │  397788   396328   0.37 │
│             rocq-mathcomp-ssreflect │    1.06     1.07  -0.93 │     7034015658      7027745032   0.09 │  598620   598296   0.05 │
│                rocq-metarocq-common │   40.97    41.31  -0.82 │   266503403553    266243288029   0.10 │  912144   911556   0.06 │
│              rocq-mathcomp-fingroup │   25.59    25.72  -0.51 │   167456975231    167324963650   0.08 │  565572   565452   0.02 │
│               coq-mathcomp-analysis │  920.39   923.90  -0.38 │  6859161534917   6857976285683   0.02 │ 1968808  1968400   0.02 │
│             rocq-mathcomp-character │   92.57    92.91  -0.37 │   648019188545    647592511273   0.07 │ 1623580  1623548   0.00 │
│                            coq-corn │  664.59   666.95  -0.35 │  4552950699713   4551242126935   0.04 │  734972   731468   0.48 │
│                           rocq-elpi │   15.15    15.20  -0.33 │   107654082157    107280889545   0.35 │  560232   559888   0.06 │
│              coq-mathcomp-odd-order │  567.87   569.03  -0.20 │  4104345307254   4103201834518   0.03 │ 2632856  2632872  -0.00 │
│              rocq-mathcomp-solvable │   94.78    94.95  -0.18 │   647937145310    647492072969   0.07 │ 1125492  1124876   0.05 │
│         coq-rewriter-perf-SuperFast │  481.34   482.08  -0.15 │  3759022405821   3757672568702   0.04 │ 1258968  1262928  -0.31 │
│ coq-neural-net-interp-computed-lite │  235.90   235.97  -0.03 │  2263222582105   2263254296006  -0.00 │  845168   843840   0.16 │
│                        coq-rewriter │  340.38   340.24   0.04 │  2535836597224   2530488394378   0.21 │ 1291944  1271408   1.62 │
│                      coq-coquelicot │   42.91    42.84   0.16 │   256671065895    255871505374   0.31 │  833224   833812  -0.07 │
│               coq-engine-bench-lite │  125.27   125.03   0.19 │   943657540788    935660599077   0.85 │  988324   989956  -0.16 │
│                   coq-iris-examples │  369.90   369.19   0.19 │  2445571430064   2440151586544   0.22 │ 1150372  1145780   0.40 │
│                        rocq-runtime │   73.64    73.49   0.20 │   534570982305    534562806687   0.00 │  510072   509624   0.09 │
│               rocq-mathcomp-algebra │  298.88   298.26   0.21 │  2203472075544   2202411831772   0.05 │ 1482816  1494104  -0.76 │
│          coq-performance-tests-lite │  902.83   900.92   0.21 │  7268082791455   7266283643605   0.02 │ 2214148  2194228   0.91 │
│                    coq-fiat-parsers │  274.37   273.77   0.22 │  2111344071632   2107763834841   0.17 │ 2347936  2349916  -0.08 │
│                    coq-math-classes │   82.25    82.06   0.23 │   501581014213    500992326143   0.12 │  516324   515328   0.19 │
│                  rocq-mathcomp-boot │   38.27    38.18   0.24 │   225811426569    225727565055   0.04 │  660212   661568  -0.20 │
│                           coq-verdi │   42.52    42.42   0.24 │   283558517964    283073979983   0.17 │  524564   529328  -0.90 │
│                 rocq-mathcomp-field │  171.00   170.57   0.25 │  1283682187541   1283016678818   0.05 │ 2043940  2050756  -0.33 │
│                         coq-coqutil │   45.93    45.81   0.26 │   288279652670    287792002852   0.17 │  560612   562924  -0.41 │
│                       coq-fiat-core │   54.77    54.60   0.31 │   332502828537    331828863649   0.20 │  483992   481784   0.46 │
│                         coq-unimath │ 1780.99  1775.18   0.33 │ 14824946657584  14805485957350   0.13 │ 1060660  1066848  -0.58 │
│                           coq-color │  230.30   229.48   0.36 │  1455664261257   1451259294522   0.30 │ 1132644  1129532   0.28 │
│                      coq-verdi-raft │  497.77   495.89   0.38 │  3454327827582   3441464837040   0.37 │  824144   823100   0.13 │
│                       coq-fourcolor │ 1354.69  1348.77   0.44 │ 12418692403772  12414721625047   0.03 │  967780   967052   0.08 │
│                 rocq-metarocq-utils │   23.55    23.44   0.47 │   152790498529    152958099478  -0.11 │  588148   587124   0.17 │
│                        coq-coqprime │   52.61    52.36   0.48 │   358404986915    357851738152   0.15 │  804472   804052   0.05 │
│                 rocq-mathcomp-order │   83.73    83.32   0.49 │   607308428143    607356697304  -0.01 │ 1534860  1534144   0.05 │
│                 rocq-metarocq-pcuic │  629.23   626.00   0.52 │  4014671797528   4001851173267   0.32 │ 1875328  1880908  -0.30 │
│                            coq-core │    2.90     2.88   0.69 │    19658596691     19665436366  -0.03 │  104368   104096   0.26 │
│                             coq-vst │  846.29   839.68   0.79 │  6409108136149   6372343863465   0.58 │ 2265120  2210880   2.45 │
│           rocq-metarocq-safechecker │  317.03   314.22   0.89 │  2371403927459   2360787178434   0.45 │ 1877248  1870932   0.34 │
│                        coq-compcert │  299.20   296.50   0.91 │  1955810847024   1941974863654   0.71 │ 1207688  1187664   1.69 │
│                         rocq-stdlib │  444.31   439.85   1.01 │  1534469077456   1532841064310   0.11 │  627132   624028   0.50 │
│                        rocq-bignums │   25.24    24.96   1.12 │   158961413659    157994927488   0.61 │  457416   457916  -0.11 │
│                           rocq-core │    6.69     6.57   1.83 │    41418946626     40683294316   1.81 │  454532   452344   0.48 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-hott (in NEW)
rocq-metarocq-template (in NEW)
rocq-metarocq-erasure (dependency install failed in NEW)
rocq-metarocq-translations (dependency install failed in NEW)
coq-bedrock2 (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)
coq-category-theory (in NEW)

🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                    TOP 25 SLOW DOWNS                                                    │
│                                                                                                                         │
│   OLD     NEW     DIFF    %DIFF    Ln                  FILE                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  32.126  33.847  1.7210     5.36%   97  coq-vst/veric/binop_lemmas5.v.html                                              │
│   0.403   1.453  1.0500   260.55%  946  coq-vst/veric/binop_lemmas2.v.html                                              │
│    96.5    97.3  0.7782     0.81%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  41.119  41.877  0.7580     1.84%  834  coq-vst/veric/binop_lemmas4.v.html                                              │
│    1.41    1.96  0.5526    39.25%  313  rocq-stdlib/theories/Strings/Byte.v.html                                        │
│    96.2    96.7  0.5161     0.54%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│    4.10    4.59  0.4989    12.18%  492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html            │
│   3.787   4.251  0.4640    12.25%  477  coq-vst/veric/expr_lemmas3.v.html                                               │
│   0.869    1.23  0.3657    42.09%  408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                       │
│    32.8    33.2  0.3593     1.09%   12  coq-fourcolor/theories/proof/job439to465.v.html                                 │
│    18.2    18.5  0.3386     1.87%   12  coq-fourcolor/theories/proof/job271to278.v.html                                 │
│   0.269   0.602  0.3327   123.70%   12  rocq-stdlib/theories/MSets/MSets.v.html                                         │
│    24.3    24.6  0.3275     1.35%   12  coq-fourcolor/theories/proof/job486to489.v.html                                 │
│    2.03    2.35  0.3231    15.93%  469  rocq-metarocq-safechecker/safechecker/theories/PCUICEqualityDec.v.html          │
│    1.55    1.87  0.3189    20.54%   75  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                           │
│    19.2    19.5  0.3151     1.64%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html               │
│    25.2    25.5  0.3137     1.25%   12  coq-fourcolor/theories/proof/job517to530.v.html                                 │
│ 0.00373   0.302  0.2978  7995.73%  202  coq-mathcomp-analysis/theories/normedtype_theory/ereal_normedtype.v.html        │
│    29.4    29.6  0.2843     0.97%   12  coq-fourcolor/theories/proof/job323to383.v.html                                 │
│  0.0896   0.352  0.2627   293.28%  312  rocq-stdlib/theories/Reals/Abstract/ConstructiveAbs.v.html                      │
│   6.166   6.428  0.2620     4.25%  192  coq-vst/veric/binop_lemmas5.v.html                                              │
│    2.01    2.27  0.2565    12.76%    2  coq-mathcomp-analysis/theories/homotopy_theory/homotopy.v.html                  │
│    27.0    27.3  0.2560     0.95%   12  coq-fourcolor/theories/proof/job611to617.v.html                                 │
│    25.1    25.4  0.2458     0.98%   12  coq-fourcolor/theories/proof/job227to230.v.html                                 │
│   0.354   0.596  0.2425    68.50%   11  rocq-stdlib/theories/QArith/Qround.v.html                                       │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│  OLD     NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  30.7      30.2  -0.5143   -1.67%    12  coq-fourcolor/theories/proof/job165to189.v.html                                               │
│  8.39      7.97  -0.4191   -5.00%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│ 0.555     0.148  -0.4063  -73.24%    11  rocq-stdlib/theories/omega/OmegaLemmas.v.html                                                 │
│ 0.520     0.130  -0.3904  -75.03%  1166  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│  48.9      48.5  -0.3817   -0.78%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│  1.62      1.24  -0.3795  -23.38%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│ 0.520     0.234  -0.2862  -55.07%    18  rocq-stdlib/theories/micromega/VarMap.v.html                                                  │
│ 0.601     0.327  -0.2737  -45.58%    11  rocq-stdlib/theories/ZArith/Zdiv_facts.v.html                                                 │
│  36.7      36.4  -0.2681   -0.73%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│  1.02     0.747  -0.2680  -26.40%   170  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                            │
│ 0.251   0.00364  -0.2475  -98.55%   148  rocq-mathcomp-field/field/algnum.v.html                                                       │
│  3.22      2.98  -0.2383   -7.41%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│ 0.489     0.262  -0.2269  -46.39%    17  rocq-stdlib/theories/Logic/IndefiniteDescription.v.html                                       │
│   201       201  -0.2232   -0.11%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│ 0.221  0.000098  -0.2213  -99.96%   219  rocq-mathcomp-algebra/algebra/spectral.v.html                                                 │
│ 0.733     0.514  -0.2194  -29.93%    21  rocq-stdlib/theories/MSets/MSetPositive.v.html                                                │
│ 0.542     0.323  -0.2194  -40.47%    19  rocq-stdlib/theories/Sorting/Heap.v.html                                                      │
│ 0.220  0.000824  -0.2187  -99.62%   112  rocq-mathcomp-field/field/galois.v.html                                                       │
│ 0.218   0.00261  -0.2155  -98.80%   145  coq-fourcolor/theories/proof/discretize.v.html                                                │
│  26.3      26.1  -0.2151   -0.82%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│ 0.213   0.00122  -0.2119  -99.43%   513  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html                        │
│ 0.196   0.00194  -0.1943  -99.01%   136  coq-mathcomp-odd-order/theories/BGsection1.v.html                                             │
│  19.1      19.0  -0.1936   -1.01%    12  coq-fourcolor/theories/proof/job207to214.v.html                                               │
│ 0.230    0.0367  -0.1932  -84.02%    84  rocq-metarocq-pcuic/pcuic/theories/Bidirectional/BDUnique.v.html                              │
│ 0.196   0.00376  -0.1924  -98.09%    11  coq-mathcomp-odd-order/theories/BGsection2.v.html                                             │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@tabareau
Copy link
Contributor Author

I think the PR is ready (the first order heuristic is not used anymore and can be removed here). Only rocq-community/paramcoq#142 needs to be fixed @ppedrot.

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

Reviewers

@JasonGross JasonGross JasonGross left review comments

@gares gares gares left review comments

@ppedrot ppedrot ppedrot left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@tabareau @ppedrot @JasonGross @SkySkimmer @jfehrle @Zimmi48 @gares