NotificationsYou must be signed in to change notification settings
Fork676
Star5k

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.

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

Already on GitHub?Sign in to your account

Jump to bottom

Do not call recursively self on subterm strategy.#20338

Merged

coqbot-app merged 1 commit intorocq-prover:masterfromppedrot:rewrite-no-rec-subterm

Mar 20, 2025

Merged

Do not call recursively self on subterm strategy.#20338

coqbot-app merged 1 commit intorocq-prover:masterfromppedrot:rewrite-no-rec-subterm

Mar 20, 2025

Conversation

Copy link

Member

ppedrot commentedMar 10, 2025

I do not know why this was done this way, in practice it probably does not matter insofar as virtually all calls to subterm are wrapped in a fixpoint.

Do not call recursively self on subterm strategy.

db7a93e

I do not know why this was done this way, in practice it probably does notmatter insofar as virtually all calls to subterm are wrapped in a fixpoint.

ppedrot added kind: cleanup

Code removal, deprecation, refactorings, etc.

request: full CIUse this label when you want your next push to trigger a full CI. labels

Mar 10, 2025

ppedrot added this to the9.1+rc1 milestone

Mar 10, 2025

ppedrot requested a review froma team as acode owner

March 10, 2025 10:09

coqbot-appbot removed the request: full CIUse this label when you want your next push to trigger a full CI. label

Mar 10, 2025

Copy link

MemberAuthor

ppedrot commentedMar 10, 2025

@coqbot bench

Copy link

Contributor

coqbot-appbot commentedMar 10, 2025

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  ││                                     │                         │                                       │                         ││            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤│              coq-mathcomp-ssreflect │   83.67    85.25  -1.85 │   569382911659    569375203651   0.00 │ 1486564  1487492  -0.06 ││                           rocq-core │    6.48     6.60  -1.82 │    40944922796     40946422819  -0.00 │  441004   435652   1.23 ││                      rocq-equations │    8.92     9.01  -1.00 │    62557048203     62570472524  -0.02 │  397180   396508   0.17 ││               coq-mathcomp-solvable │   80.18    80.97  -0.98 │   547546574082    547578705961  -0.01 │  895192   895036   0.02 ││             coq-metacoq-safechecker │  341.93   344.35  -0.70 │  2603673971659   2603777951542  -0.00 │ 1668012  1666628   0.08 ││               coq-engine-bench-lite │  124.07   124.61  -0.43 │   937822066407    935672406728   0.23 │ 1077512  1077476   0.00 ││                 coq-category-theory │  596.44   597.57  -0.19 │  4437194619690   4437389830207  -0.00 │  955644   957804  -0.23 ││                         coq-unimath │ 2287.51  2288.07  -0.02 │ 18188306453605  18188006853858   0.00 │ 1087340  1084120   0.30 ││                        rocq-bignums │   30.54    30.54   0.00 │   194874554067    194898045382  -0.01 │  480672   480728  -0.01 ││                           rocq-elpi │   12.69    12.69   0.00 │    91273072770     91283247378  -0.01 │  481200   481236  -0.01 ││                           coq-verdi │   44.18    44.18   0.00 │   294435046555    294409753899   0.01 │  519072   515812   0.63 ││         coq-rewriter-perf-SuperFast │  471.66   470.95   0.15 │  3744578612666   3745199517980  -0.02 │ 1203112  1200012   0.26 ││                coq-mathcomp-algebra │  169.25   168.97   0.17 │  1201809820728   1201854387023  -0.00 │ 1102452  1102076   0.03 ││                        coq-rewriter │  333.23   332.63   0.18 │  2506507321403   2505843862801   0.03 │ 1325000  1325856  -0.06 ││                 coq-metacoq-erasure │  515.96   514.99   0.19 │  3555813647404   3555729581719   0.00 │ 1788884  1782368   0.37 ││                        rocq-runtime │   74.43    74.27   0.22 │   537042089653    536927598146   0.02 │  483408   485320  -0.39 ││               coq-mathcomp-analysis │  570.33   569.10   0.22 │  4180575284471   4180379446150   0.00 │ 1496792  1496448   0.02 ││                            coq-hott │  161.14   160.78   0.22 │  1123322902324   1123438626402  -0.01 │  488060   488548  -0.10 ││        coq-fiat-crypto-with-bedrock │ 6105.32  6090.90   0.24 │ 49757120769296  49764735311418  -0.02 │ 3123704  3122220   0.05 ││                   coq-iris-examples │  395.36   394.36   0.25 │  2641857849364   2641990234675  -0.01 │ 1095896  1100020  -0.37 ││                    coq-fiat-parsers │  272.78   271.95   0.31 │  2115515070993   2114272574280   0.06 │ 2287708  2285840   0.08 ││                   coq-metacoq-utils │   22.85    22.78   0.31 │   150112176685    150072792691   0.03 │  578264   578252   0.00 ││              coq-mathcomp-odd-order │  487.67   486.02   0.34 │  3484954613633   3484865143595   0.00 │ 1667908  1667112   0.05 ││                            coq-corn │  676.50   673.96   0.38 │  4648462848841   4648546081268  -0.00 │  702636   702072   0.08 ││            coq-metacoq-translations │   16.57    16.50   0.42 │   119966924004    119953961765   0.01 │  752976   751204   0.24 ││                      coq-coquelicot │   37.53    37.36   0.46 │   228000937497    228012435644  -0.01 │  819352   823424  -0.49 ││                  coq-mathcomp-field │   91.81    91.39   0.46 │   667419860246    667453687429  -0.01 │ 1326488  1330236  -0.28 ││                        coq-compcert │  308.74   307.26   0.48 │  2027156724934   2027243188778  -0.00 │ 1102308  1101136   0.11 ││                           coq-color │  246.30   245.02   0.52 │  1540155195374   1540152415280   0.00 │ 1052720  1049180   0.34 ││ coq-neural-net-interp-computed-lite │  234.17   232.74   0.61 │  2248190630885   2248217803840  -0.00 │  869600   874420  -0.55 ││                      coq-verdi-raft │  538.91   535.43   0.65 │  3699769052105   3699706255517   0.00 │  827072   824948   0.26 ││                   coq-metacoq-pcuic │  649.77   645.57   0.65 │  4175256171407   4174155765988   0.03 │ 2241156  2241272  -0.01 ││                coq-metacoq-template │  145.81   144.82   0.68 │   979124160662    979095709685   0.00 │  947172   949428  -0.24 ││                        coq-coqprime │   52.04    51.64   0.77 │   357934616155    358002691720  -0.02 │  794060   794332  -0.03 ││                         rocq-stdlib │  211.60   209.70   0.91 │  1324796148041   1324805245089  -0.00 │  597164   600284  -0.52 ││                       coq-fourcolor │ 1316.32  1304.43   0.91 │ 12221631926102  12221638802665  -0.00 │  766296   766328  -0.00 ││          coq-performance-tests-lite │  902.96   894.56   0.94 │  7286753487103   7284356143613   0.03 │ 2475248  2477976  -0.11 ││               coq-mathcomp-fingroup │   23.10    22.87   1.01 │   148908927174    148937508630  -0.02 │  501076   501164  -0.02 ││                  coq-metacoq-common │   65.31    64.64   1.04 │   420413983180    420367360791   0.01 │  912220   910036   0.24 ││                         coq-coqutil │   44.52    44.06   1.04 │   279674833723    279713356341  -0.01 │  557820   555776   0.37 ││                             coq-vst │  875.15   865.11   1.16 │  6565856530867   6565723435179   0.00 │ 2202364  2201460   0.04 ││              coq-mathcomp-character │   70.21    69.14   1.55 │   480192816291    480806292096  -0.13 │ 1147700  1147864  -0.01 ││                            coq-core │    2.82     2.77   1.81 │    19447285033     19439293544   0.04 │   92052    91856   0.21 ││                    coq-math-classes │   86.79    85.22   1.84 │   525333459749    525424808763  -0.02 │  505324   505868  -0.11 ││                       coq-fiat-core │   57.36    56.20   2.06 │   347240364431    346537686732   0.20 │  470580   472240  -0.35 │└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

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

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐│                                                            TOP 25 SLOW DOWNS                                                             ││                                                                                                                                          ││  OLD     NEW     DIFF   %DIFF   Ln                      FILE                                                                             │├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤│   23.0    26.5  3.4326  14.91%  129coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                               ││   99.3     101  1.5888   1.60%  999coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                     ││   99.6     101  1.2226   1.23%  968coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                     ││    199     200  1.0857   0.54%    8coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html       ││   65.3    66.2  0.8972   1.37%  609coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html       ││   55.6    56.3  0.7039   1.27%  731coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                               ││   17.8    18.4  0.5655   3.17%   32coq-performance-tests-lite/src/pattern.v.html                                                       ││   36.8    37.2  0.4602   1.25%    2coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                             ││   32.1    32.5  0.4471   1.39%   12coq-fourcolor/theories/proof/job439to465.v.html                                                     ││   59.7    60.2  0.4247   0.71%   27coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                            ││ 31.933  32.348  0.4150   1.30%   97coq-vst/veric/binop_lemmas5.v.html                                                                  ││   24.1    24.5  0.3947   1.64%   12coq-fourcolor/theories/proof/job503to506.v.html                                                     ││   20.9    21.3  0.3840   1.84%  213coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                    ││   21.0    21.4  0.3734   1.78%    6coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html ││   78.3    78.7  0.3727   0.48%   48coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                             ││   35.0    35.4  0.3613   1.03%  120coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html               ││   23.6    23.9  0.3536   1.50%   12coq-fourcolor/theories/proof/job486to489.v.html                                                     ││   28.1    28.5  0.3503   1.25%   12coq-fourcolor/theories/proof/job563to588.v.html                                                     ││   30.0    30.4  0.3410   1.14%  607coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                               ││   24.7    25.1  0.3376   1.37%   12coq-fourcolor/theories/proof/job299to302.v.html                                                     ││   24.2    24.5  0.3329   1.38%   12coq-fourcolor/theories/proof/job319to322.v.html                                                     ││   26.3    26.6  0.3305   1.26%   12coq-fourcolor/theories/proof/job531to534.v.html                                                     ││   24.6    25.0  0.3257   1.32%   12coq-fourcolor/theories/proof/job517to530.v.html                                                     ││   30.4    30.7  0.3200   1.05%   12coq-fourcolor/theories/proof/job254to270.v.html                                                     ││   25.2    25.5  0.3180   1.26%   12coq-fourcolor/theories/proof/job466to485.v.html                                                     │└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐│                                                              TOP 25 SPEED UPS                                                               ││                                                                                                                                             ││ OLD   NEW    DIFF     %DIFF    Ln                      FILE                                                                                 │├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤│  174   173  -1.3033   -0.75%   233coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html ││ 29.6  28.7  -0.8845   -2.99%   146coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            ││ 27.8  26.9  -0.8795   -3.17%   149coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            ││ 27.2  26.5  -0.7331   -2.69%    68coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html      ││ 21.9  21.3  -0.6116   -2.80%    49coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 ││ 15.0  14.4  -0.6032   -4.03%   841coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 ││  236   236  -0.5950   -0.25%   141coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              ││ 11.9  11.4  -0.4592   -3.86%   812coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               ││ 9.69  9.29  -0.3940   -4.07%   434coq-mathcomp-odd-order/theories/PFsection12.v.html                                                      ││ 7.76  7.45  -0.3144   -4.05%   446coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               ││  133   133  -0.2926   -0.22%   155coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              ││ 8.06  7.78  -0.2771   -3.44%   822coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               ││ 19.0  18.8  -0.2734   -1.44%   481coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                       ││ 13.1  12.8  -0.2673   -2.04%   931coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               ││ 23.0  22.7  -0.2630   -1.15%   373coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                      ││ 10.1  9.80  -0.2558   -2.54%   325coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                    ││ 9.47  9.24  -0.2381   -2.51%   345coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                              ││ 6.20  5.97  -0.2343   -3.78%   792coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               ││ 5.83  5.60  -0.2337   -4.01%   130coq-category-theory/Functor/Strong/Product.v.html                                                       ││ 1.66  1.43  -0.2279  -13.71%  1375coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html           ││ 39.0  38.7  -0.2244   -0.58%   835coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  ││ 7.65  7.45  -0.2034   -2.66%   420coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                    ││ 10.2  9.96  -0.2029   -2.00%   214coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                    ││ 2.42  2.23  -0.1972   -8.14%   620coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 ││ 45.3  45.1  -0.1954   -0.43%   110coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html            │└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘