8000 Set some basic rewriting primitives in Type opaque for TC search. by ppedrot · Pull Request #18910 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Set some basic rewriting primitives in Type opaque for TC search. #18910

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
Merged
merged 2 commits into from
Apr 19, 2024
Merged

Set some basic rewriting primitives in Type opaque for TC search. #18910

merged 2 commits into from
Apr 19, 2024

Conversation

ppedrot
Copy link
Member
@ppedrot ppedrot commented Apr 7, 2024 •
edited
Loading

The corresponding Prop primitives are already set opaque in Classes.Init, hence I think this is an oversight. These low-level primitives being transparent mean that TC search when setoid rewriting in Type fires off a crapload of search branches that should not be there to begin with. Hopefully nobody relies on that in the wild.

cc @mattam82

Backward compatible overlay:

@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 7, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 7, 2024
@ppedrot
Copy link
Member Author
ppedrot commented Apr 7, 2024

@coqbot bench

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Apr 8, 2024

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                          coq-stdlib │  364.72   378.40  -3.62 │  1523163576905   1577830974288  -3.46 │  1310053465451   1343424307348  -2.48 │  718152   718004   0.02 │
│                       coq-equations │    7.64     7.75  -1.42 │    31292938178     31451548084  -0.50 │    50977446711     50992685381  -0.03 │  386092   386236  -0.04 │
│                            coq-corn │  726.31   733.26  -0.95 │  3283534652082   3314672846937  -0.94 │  5138703616627   5187888172505  -0.95 │  803748   802224   0.19 │
│                    coq-fiat-parsers │  312.77   314.79  -0.64 │  1385460009277   1391716840682  -0.45 │  2430503890163   2434242593096  -0.15 │ 2373824  2379700  -0.25 │
│            coq-metacoq-translations │   17.04    17.13  -0.53 │    75185257853     75276050453  -0.12 │   124859943412    124837729432   0.02 │  849196   847096   0.25 │
│                coq-mathcomp-algebra │  234.58   235.73  -0.49 │  1061277809283   1066460482156  -0.49 │  1765918513355   1765897939421   0.00 │ 1288628  1288520   0.01 │
│              coq-mathcomp-ssreflect │   94.44    94.81  -0.39 │   426316586778    427674668016  -0.32 │   665963380575    665978044899  -0.00 │ 1358184  1359912  -0.13 │
│                        coq-compcert │  283.92   284.80  -0.31 │  1274909428680   1277957422260  -0.24 │  1953037899252   1953132967142  -0.00 │ 1109768  1110908  -0.10 │
│                       coq-fiat-core │   60.04    60.21  -0.28 │   249415941015    249675865056  -0.10 │   369541644484    369535397873   0.00 │  479068   478572   0.10 │
│                      coq-coquelicot │   39.78    39.89  -0.28 │   176474614701    176483760807  -0.01 │   250105103935    250091108259   0.01 │  849784   853100  -0.39 │
│               coq-mathcomp-solvable │  117.55   117.82  -0.23 │   535994629292    536343706178  -0.07 │   858835877388    858824614421   0.00 │  863304   864188  -0.10 │
│          coq-performance-tests-lite │  708.78   710.20  -0.20 │  3172810882935   3177101104009  -0.14 │  5646554618115   5645926139280   0.01 │ 1588460  1588772  -0.02 │
│ coq-neural-net-interp-computed-lite │  293.93   294.49  -0.19 │  1340320136377   1342219926096  -0.14 │  3419516134540   3419570954992  -0.00 │ 1120284  1118032   0.20 │
│                           coq-color │  239.40   239.76  -0.15 │  1067009382330   1068261524941  -0.12 │  1577694506183   1577484704160   0.01 │ 1192612  1192604   0.00 │
│                           coq-verdi │   49.51    49.58  -0.14 │   221930738220    221864282761   0.03 │   345380199180    345402403477  -0.01 │  531960   533552  -0.30 │
│                            coq-core │  129.88   130.06  -0.14 │   498673665838    498219903335   0.09 │   531730502839    531989601807  -0.05 │  440696   439272   0.32 │
│                       coq-fourcolor │ 1358.76  1359.93  -0.09 │  6179494091680   6183673499819  -0.07 │ 12151870669373  12151822785062   0.00 │ 2128148  2130208  -0.10 │
│                            coq-hott │  157.12   157.17  -0.03 │   695171075379    695692155249  -0.07 │  1114162095444   1114228261378  -0.01 │  548080   547868   0.04 │
│                         coq-unimath │ 2403.78  2404.43  -0.03 │ 10895032571460  10898866046033  -0.04 │ 21707484893060  21706762371267   0.00 │ 1270452  1271868  -0.11 │
│                        coq-coqprime │   48.69    48.70  -0.02 │   217713064301    217609319523   0.05 │   334672673787    334682128156  -0.00 │  787976   789072  -0.14 │
│              coq-mathcomp-odd-order │  775.31   775.20   0.01 │  3539743696470   3539150774749   0.02 │  6020015116612   6020200009568  -0.00 │ 1617220  1614856   0.15 │
│               coq-mathcomp-fingroup │   30.46    30.45   0.03 │   138474455537    138162054359   0.23 │   209039899744    209075577507  -0.02 │  562948   562932   0.00 │
│                        coq-rewriter │  390.49   390.34   0.04 │  1760901596815   1760177484375   0.04 │  2964140264125   2964175533584  -0.00 │ 1487144  1487060   0.01 │
│                    coq-math-classes │   86.19    86.14   0.06 │   385201047157    384600499062   0.16 │   536813523218    536848208388  -0.01 │  506756   506360   0.08 │
│              coq-mathcomp-character │  103.72   103.65   0.07 │   471705030026    471238809024   0.10 │   746536175308    746526451234   0.00 │ 1041616  1043120  -0.14 │
│        coq-fiat-crypto-with-bedrock │ 6161.63  6157.29   0.07 │ 27903448150946  27882829134269   0.07 │ 50950271316567  50957250394363  -0.01 │ 3245916  3245836   0.00 │
│         coq-rewriter-perf-SuperFast │  792.00   791.14   0.11 │  3544932681516   3536742475498   0.23 │  6198118581639   6198039926636   0.00 │ 1581340  1587092  -0.36 │
│                                 coq │  728.76   727.80   0.13 │  3060900832480   3058912604450   0.06 │  5457542797211   5465444206299  -0.14 │ 2717156  2717180  -0.00 │
│                      coq-verdi-raft │  585.78   584.96   0.14 │  2657232379301   2653247612349   0.15 │  4
8000
210432823702   4211852713102  -0.03 │  846644   848420  -0.21 │
│                             coq-vst │  878.97   875.91   0.35 │  3972720020783   3959496061038   0.33 │  6746371275409   6746249134422   0.00 │ 2200264  2202156  -0.09 │
│                coq-metacoq-template │  150.36   149.81   0.37 │   661532529132    659709708035   0.28 │  1038830154494   1038760294538   0.01 │ 1161240  1161136   0.01 │
│                  coq-mathcomp-field │  135.87   135.17   0.52 │   613528652061    610703089522   0.46 │  1016922806229   1016970004420  -0.00 │ 1389860  1386524   0.24 │
│                   coq-iris-examples │  467.07   464.57   0.54 │  2113141686808   2102258494883   0.52 │  3269215377663   3268817225251   0.01 │ 1101536  1101192   0.03 │
│               coq-engine-bench-lite │  157.80   156.93   0.55 │   661940565878    658655467352   0.50 │  1227230815848   1224569758193   0.22 │ 1227116  1227172  -0.00 │
│                         coq-coqutil │   43.07    42.81   0.61 │   188586289092    187651222772   0.50 │   271905571725    271981232628  -0.03 │  565380   566648  -0.22 │
│                         coq-bignums │   29.83    29.61   0.74 │   134635805538    133525290970   0.83 │   194511487923    194493430957   0.01 │  480152   479512   0.13 │
│                        coq-bedrock2 │  384.73   381.19   0.93 │  1736786446501   1721619333970   0.88 │  3350004542372   3349640834452   0.01 │  915028   914948   0.01 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-metacoq-pcuic
coq-category-theory

coq-metacoq-safechecker (dependency coq-metacoq-pcuic failed)
coq-metacoq-erasure (dependency coq-metacoq-pcuic failed)

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  49.5620   50.9320  1.3700   2.76%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                    │
│  62.4160   63.7700  1.3540   2.17%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│   2.3220    3.4280  1.1060  47.63%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                         │
│ 153.0510  153.7850  0.7340   0.48%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│   2.3770    3.1090  0.7320  30.80%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                         │
│ 235.7560  236.3610  0.6050   0.26%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                         │
│  95.4390   96.0340  0.5950   0.62%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                │
│  39.2410   39.7920  0.5510   1.40%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  34.0880   34.5290  0.4410   1.29%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html   │
│  26.9680   27.3760  0.4080   1.51%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                       │
│  82.0490   82.4500  0.4010   0.49%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│  27.4000   27.6960  0.2960   1.08%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│   8.5870    8.8470  0.2600   3.03%   673  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                                        │
│  46.8330   47.0780  0.2450   0.52%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                          │
│  16.9180   17.1630  0.2450   1.45%    12  coq-fourcolor/theories/job550to553.v.html                                                          │
│  15.0840   15.3200  0.2360   1.56%   613  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html            │
│  23.0370   23.2690  0.2320   1.01%    12  coq-fourcolor/theories/job554to562.v.html                                                          │
│  14.8600   15.0830  0.2230   1.50%   611  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html            │
│   0.5580    0.7710  0.2130  38.17%   590  coq-stdlib/Strings/Byte.v.html                                                                     │
│  25.1570   25.3690  0.2120   0.84%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                              │
│  17.7980   18.0070  0.2090   1.17%    32  coq-performance-tests-lite/src/pattern.v.html                                                      │
│   3.1280    3.3320  0.2040   6.52%   142  coq-vst/veric/Clight_mapsto_memory_block.v.html                                                    │
│   0.4320    0.6330  0.2010  46.53%    21  coq-stdlib/MSets/MSetPositive.v.html                                                               │
│   0.2990    0.4900  0.1910  63.88%  1364  coq-stdlib/FSets/FMapAVL.v.html                                                                    │
│  46.3640   46.5520  0.1880   0.41%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html       │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF     %DIFF   Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  50.9090   49.4890  -1.4200   -2.79%  558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│   1.8620    0.7780  -1.0840  -58.22%  736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                            │
│ 133.9900  132.9530  -1.0370   -0.77%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│  99.2520   98.2620  -0.9900   -1.00%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│  73.3430   72.7190  -0.6240   -0.85%  905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                              │
│   3.0100    2.4630  -0.5470  -18.17%  102  coq-fiat-parsers/src/Parsers/ParserImplementation.v.html                                          │
│   2.5800    2.0810  -0.4990  -19.34%   32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│  29.6700   29.1970  -0.4730   -1.59%   12  coq-fourcolor/theories/job001to106.v.html                                                         │
│  81.3220   80.8780  -0.4440   -0.55%  365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│  44.0950   43.6750  -0.4200   -0.95%  827  coq-vst/veric/binop_lemmas4.v.html                                                                │
│  25.1070   24.6890  -0.4180   -1.66%   12  coq-fourcolor/theories/job499to502.v.html                                                         │
│ 253.6920  253.3030  -0.3890   -0.15%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html     │
│   2.0140    1.6370  -0.3770  -18.72%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│   1.1940    0.8220  -0.3720  -31.16%  384  coq-stdlib/MSets/MSetAVL.v.html                                                                   │
│ 100.4600  100.0960  -0.3640   -0.36%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│  37.4610   37.0980  -0.3630   -0.97%  548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│   0.9170    0.5570  -0.3600  -39.26%  170  coq-stdlib/Numbers/HexadecimalNat.v.html                                                          │
│   1.2000    0.8480  -0.3520  -29.33%  467  coq-stdlib/Numbers/DecimalFacts.v.html                                                            │
│  28.8620   28.5120  -0.3500   -1.21%   32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html              │
│   0.4880    0.1450  -0.3430  -70.29%  915  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                            │
│  67.2230   66.8830  -0.3400   -0.51%  368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│   0.6620    0.3490  -0.3130  -47.28%  868  coq-stdlib/MSets/MSetRBT.v.html                                                                   │
│   0.5130    0.2090  -0.3040  -59.26%   12  coq-stdlib/MSets/MSets.v.html                                                                     │
│   3.4190    3.1260  -0.2930   -8.57%  122  coq-stdlib/setoid_ring/Ncring_initial.v.html                                                      │
│  18.4480   18.1630  -0.2850   -1.54%   12  coq-fourcolor/theories/job207to214.v.html                                                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Apr 8, 2024

🔴 CI failures at commit 11d9f29 without any failure in the test-suite

✔️ Corresponding jobs for the base commit c481f44 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-metacoq
  • You can also pass me a specific list of targets to minimize as arguments.

@ppedrot
Copy link
Member Author
ppedrot commented Apr 8, 2024

The stdlib speed up is real, this is CReals rewriting going way faster.

ppedrot added a commit to ppedrot/category-theory that referenced this pull request Apr 8, 2024
@ppedrot
Adapt w.r.t. rocq-prover/rocq#18910.
f8295f0 
We guide unification a bit to prevent TC resolution from relying on a previously
transparent Coq primitive.
@ppedrot
Copy link
Member Author
ppedrot commented Apr 8, 2024

The fix in category-theory is a one-liner, so I think this is a safe change.

ppedrot added a commit to ppedrot/metacoq that referenced this pull request Apr 9, 2024
@ppedrot
Adapt w.r.t. rocq-prover/rocq#18910.
2d9b6f0
ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Apr 9, 2024
@ppedrot
Merge pull request #1076 from ppedrot/setoid-type-core-tc-opaque
74918fc 
Adapt w.r.t. rocq-prover/rocq#18910.
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 10, 2024
@ppedrot ppedrot force-pushed the setoid-type-core-tc-opaque branch from 11d9f29 to c6af6a2 Compare April 10, 2024 21:01
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 10, 2024
@ppedrot
Copy link
Member Author
ppedrot commented Apr 10, 2024

@coqbot bench

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Apr 11, 2024

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│            coq-metacoq-translations │   16.76    17.10  -1.99 │    75419360944     76319915060  -1.18 │   124962421279    124984302256  -0.02 │  847332   847200   0.02 │
│                 coq-category-theory │  752.15   764.96  -1.67 │  3422984101408   3482313791825  -1.70 │  5744718831575   5800046130922  -0.95 │  970848   976476  -0.58 │
│                    coq-math-classes │   85.86    86.68  -0.95 │   386567470259    388847677683  -0.59 │   537466126791    537317379754   0.03 │  506032   505780   0.05 │
│ coq-neural-net-in
8000
terp-computed-lite │  294.99   297.48  -0.84 │  1345779815109   1358713176517  -0.95 │  3420978296264   3420984791427  -0.00 │ 1118316  1118148   0.02 │
│                            coq-corn │  729.35   734.88  -0.75 │  3311995351871   3339436008719  -0.82 │  5138769914054   5187674299603  -0.94 │  802372   802444  -0.01 │
│             coq-metacoq-safechecker │  417.25   420.18  -0.70 │  1910222888882   1923800817255  -0.71 │  3195236659605   3200392685066  -0.16 │ 1906884  1897288   0.51 │
│                            coq-hott │  156.31   157.24  -0.59 │   699102291911    702753713916  -0.52 │  1113908276103   1113896767226   0.00 │  549576   549504   0.01 │
│               coq-mathcomp-fingroup │   30.49    30.67  -0.59 │   138959115993    139165321585  -0.15 │   209110047396    209140956803  -0.01 │  562872   564508  -0.29 │
│                  coq-mathcomp-field │  134.99   135.73  -0.55 │   616596042806    620363479912  -0.61 │  1016584216177   1016645640845  -0.01 │ 1396800  1396956  -0.01 │
│                        coq-compcert │  282.04   283.20  -0.41 │  1276204094281   1281300777549  -0.40 │  1953759741784   1953768280983  -0.00 │ 1185704  1184748   0.08 │
│                       coq-fiat-core │   60.02    60.26  -0.40 │   251149000716    251610150648  -0.18 │   371193749696    371174464788   0.01 │  484468   484644  -0.04 │
│                   coq-metacoq-pcuic │  791.49   794.52  -0.38 │  3608715910375   3623332644170  -0.40 │  5407250032731   5407618075312  -0.01 │ 2388028  2388364  -0.01 │
│                          coq-stdlib │  368.68   370.04  -0.37 │  1565443074301   1576531161552  -0.70 │  1310552299589   1343785777977  -2.47 │  717120   716324   0.11 │
│                             coq-vst │  877.99   880.65  -0.30 │  3992542843818   4003843944639  -0.28 │  6760644531341   6760850328063  -0.00 │ 2196644  2196364   0.01 │
│              coq-mathcomp-odd-order │  777.80   780.07  -0.29 │  3562478780362   3571585734121  -0.25 │  6018825801167   6018910565343  -0.00 │ 1613644  1615740  -0.13 │
│                       coq-equations │    7.59     7.61  -0.26 │    31326316358     31384149401  -0.18 │    50899122370     50889313690   0.02 │  387164   386152   0.26 │
│          coq-performance-tests-lite │  705.68   706.83  -0.16 │  3188657798444   3192511314884  -0.12 │  5645973083284   5643736692082   0.04 │ 1588680  1589456  -0.05 │
│                                 coq │  725.59   726.75  -0.16 │  3062730705310   3061436536391   0.04 │  5466146860624   5478082083275  -0.22 │ 2485464  2638560  -5.80 │
│                         coq-bignums │   29.76    29.80  -0.13 │   135309334695    135280845683   0.02 │   194481918560    194458309049   0.01 │  479076   478796   0.06 │
│                            coq-core │  127.76   127.92  -0.13 │   504632298861    503265769681   0.27 │   530481579401    530159193884   0.06 │  441512   440288   0.28 │
│                        coq-coqprime │   48.47    48.52  -0.10 │   217965942001    218230071580  -0.12 │   335138434786    335138025522   0.00 │  789600   789600   0.00 │
│                        coq-rewriter │  388.49   388.83  -0.09 │  1766956841561   1767422660054  -0.03 │  2964216570913   2964180661182   0.00 │ 1485468  1484152   0.09 │
│         coq-rewriter-perf-SuperFast │  785.37   785.59  -0.03 │  3568890759457   3570882486528  -0.06 │  6200421266373   6199923236011   0.01 │ 1582564  1582716  -0.01 │
│               coq-engine-bench-lite │  156.34   156.38  -0.03 │   662007533175    662582686511  -0.09 │  1225000623042   1226454441853  -0.12 │ 1226864  1226884  -0.00 │
│                         coq-coqutil │   42.67    42.68  -0.02 │   187771554865    189197349566  -0.75 │   272929198159    272862021341   0.02 │  566544   566344   0.04 │
│                   coq-iris-examples │  466.76   466.15   0.13 │  2120928336452   2118678567764   0.11 │  3270303867553   3269834562687   0.01 │ 1096808  1096980  -0.02 │
│              coq-mathcomp-character │  103.85   103.71   0.13 │   474525653965    473897347000   0.13 │   746425004789    746426335642  -0.00 │ 1047632  1048324  -0.07 │
│                         coq-unimath │ 2431.80  2428.45   0.14 │ 11073244760478  11058978240677   0.13 │ 21948665869653  21948657702949   0.00 │ 1270788  1270260   0.04 │
│        coq-fiat-crypto-with-bedrock │ 6141.75  6132.08   0.16 │ 27974682259158  27930849387946   0.16 │ 50965361175604  50964061586313   0.00 │ 3246056  3246988  -0.03 │
│                      coq-verdi-raft │  584.60   583.67   0.16 │  2660767050079   2656175790961   0.17 │  4213207723935   4213097928185   0.00 │  846056   848164  -0.25 │
│                coq-metacoq-template │  149.43   149.18   0.17 │   663650630135    662057447132   0.24 │  1038870880432   1038690106321   0.02 │ 1158632  1159276  -0.06 │
│                       coq-fourcolor │ 1350.93  1348.38   0.19 │  6176625855433   6166270879172   0.17 │ 12151826112998  12151800508932   0.00 │ 2128140  2128104   0.00 │
│                      coq-coquelicot │   39.85    39.75   0.25 │   177069410977    177489100816  -0.24 │   250533415464    250545887869  -0.00 │  850752   853680  -0.34 │
│                 coq-metacoq-erasure │  504.44   503.12   0.26 │  2301607729797   2295212730538   0.28 │  3597825791517   3597555022969   0.01 │ 1901512  1900628   0.05 │
│                        coq-bedrock2 │  379.55   378.42   0.30 │  1730390655738   1723934572137   0.37 │  3352850089040   3352614881730   0.01 │  898372   900708  -0.26 │
│                    coq-fiat-parsers │  313.08   312.14   0.30 │  1396409219541   1394475190563   0.14 │  2437790100549   2441355780914  -0.15 │ 2379432  2381344  -0.08 │
│                coq-mathcomp-algebra │  236.74   235.80   0.40 │  1080882398282   1076146255132   0.44 │  1772174525598   1772089105425   0.00 │ 1301460  1301312   0.01 │
│                           coq-color │  238.77   237.48   0.54 │  1071471859563   1068520754087   0.28 │  1579997232669   1579682079111   0.02 │ 1195828  1197228  -0.12 │
│                           coq-verdi │   49.69    49.39   0.61 │   223452240012    222123273362   0.60 │   345811256061    345840080321  -0.01 │  530892   532100  -0.23 │
│               coq-mathcomp-solvable │  118.45   117.64   0.69 │   541157168147    537796743200   0.62 │   858253235135    858286321329  -0.00 │  865220   864404   0.09 │
│              coq-mathcomp-ssreflect │   93.47    92.70   0.83 │   426273056461    423152799239   0.74 │   665458471043    665451899108   0.00 │ 1395588  1397376  -0.13 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                         │
│   OLD       NEW      DIFF    %DIFF    Ln                    FILE                                                                        │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   2.3570    3.6090  1.2520    53.12%  490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                   │
│  62.4240   63.4300  1.0060     1.61%  609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                  │
│  95.4920   96.2770  0.7850     0.82%  103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                          │
│  38.7140   39.4370  0.7230     1.87%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html               │
│  99.8420  100.5080  0.6660     0.67%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                  │
│  66.2100   66.8730  0.6630     1.00%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│  41.6880   42.2760  0.5880     1.41%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                 │
│  28.8750   29.3770  0.5020     1.74%   12  coq-fourcolor/theories/job001to106.v.html                                                    │
│  21.3300   21.8070  0.4770     2.24%   40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html │
│ 132.8640  133.2640  0.4000     0.30%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                       │
│  24.0370   24.3610  0.3240     1.35%   85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                       │
│  25.4090   25.7230  0.3140     1.24%  345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                           │
│   0.3280    0.6070  0.2790    85.06%  868  coq-stdlib/MSets/MSetRBT.v.html                                                              │
│  43.8140   44.0750  0.2610     0.60%  827  coq-vst/veric/binop_lemmas4.v.html                                                           │
│  17.6950   17.9530  0.2580     1.46%   32  coq-performance-tests-lite/src/pattern.v.html                                                │
│  23.4860   23.7310  0.2450     1.04%   12  coq-fourcolor/theories/job231to234.v.html                                                    │
│  15.3680   15.6130  0.2450     1.59%  417  coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html            │
│  25.7250   25.9520  0.2270     0.88%  129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                        │
│   3.7770    4.0030  0.2260     5.98%  275  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│   7.3130    7.5380  0.2250     3.08%  356  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                 │
│  25.0700   25.2900  0.2200     0.88%   24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                        │
│   9.5680    9.7790  0.2110     2.21%   79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                   │
│   0.0050    0.2120  0.2070  4140.00%  324  coq-metacoq-pcuic/pcuic/theories/Bidirectional/BDToPCUIC.v.html                              │
│   0.0130    0.2190  0.2060  1584.62%  161  coq-metacoq-pcuic/pcuic/theories/PCUICPrincipality.v.html                                    │
│   0.0520    0.2530  0.2010   386.54%   41  coq-metacoq-pcuic/pcuic/theories/Bidirectional/BDStrengthening.v.html                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 256.7870  253.8340  -2.9530   -1.15%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│   1.4880    0.0450  -1.4430  -96.98%    81  coq-metacoq-safechecker/safechecker/theories/PCUICWfReduction.v.html                                    │
│ 180.7430  179.5320  -1.2110   -0.67%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   1.8270    0.7300  -1.0970  -60.04%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                                  │
│  94.9910   94.3720  -0.6190   -0.65%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  11.4670   10.9200  -0.5470   -4.77%    55  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                                    │
│  94.8030   94.2760  -0.5270   -0.56%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   2.9210    2.4280  -0.4930  -16.88%   102  coq-fiat-parsers/src/Parsers/ParserImplementation.v.html                                                │
│  81.3270   80.8390  -0.4880   -0.60%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  67.1310   66.7100  -0.4210   -0.63%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                         │
│  10.5580   10.1680  -0.3900   -3.69%   496  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                                             │
│   7.0510    6.6760  -0.3750   -5.32%    63  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                                    │
│  38.0330   37.6830  -0.3500   -0.92%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  26.7220   26.3850  -0.3370   -1.26%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  22.2420   21.9450  -0.2970   -1.34%  1073  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                                     │
│  29.0000   28.7200  -0.2800   -0.97%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                      │
│   1.2600    0.9820  -0.2780  -22.06%    36  coq-category-theory/Structure/Pullback/Limit.v.html                                                     │
│   3.3430    3.0650  -0.2780   -8.32%    77  coq-category-theory/Structure/Monoidal/Compose.v.html                                                   │
│  25.8400   25.5780  -0.2620   -1.01%    12  coq-fourcolor/theories/job399to438.v.html                                                               │
│   8.8070    8.5470  -0.2600   -2.95%   149  coq-category-theory/Structure/Monoid.v.html                                                             │
│  36.5930   36.3410  -0.2520   -0.69%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│   3.4160    3.1680  -0.2480   -7.26%   122  coq-stdlib/setoid_ring/Ncring_initial.v.html                                                            │
│   4.7670    4.5200  -0.2470   -5.18%     5  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v.html          │
│   1.0920    0.8650  -0.2270  -20.79%  2242  coq-corn/reals/stdlib/CMTIntegrableFunctions.v.html                                                     │
│   0.3780    0.1520  -0.2260  -59.79%   915  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 11, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 11, 2024
@ppedrot ppedrot added the part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics. label Apr 11, 2024
@ppedrot ppedrot added this to the 8.20+rc1 milestone Apr 11, 2024
@ppedrot ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Apr 11, 2024
@ppedrot ppedrot marked this pull request as ready for review April 11, 2024 11:30
@ppedrot ppedrot requested a review from a team as a code owner April 11, 2024 11:30
@ppedrot
Copy link
Member Author
ppedrot commented Apr 11, 2024

Should be ready now.

SkySkimmer
SkySkimmer reviewed Apr 15, 2024
View reviewed changes
test-suite/bugs/bug_7675_3.v Outdated
@@ -58,19 +58,20 @@ Ltac test S b1 b2 b3 b4 :=
unfold arrow, Basics.arrow; now rewrite <- HR | clear Ht ].

Goal True.
test Ri true true true true.
Proof.
(* test Ri true true true true. *)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

shouldn't these be edited to fit the new result?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The test doesn't make sense now. I could just remove them if you prefer.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really understand the test so I don't know why it wouldn't make sense, removing is ok I guess
cc @olaure01 who wrote the test AFAICT

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The original goal of the test was to track different behaviors between setoid rewriting in Prop and in Type, but I think they know behave similarly on these examples.

@SkySkimmer SkySkimmer self-assigned this Apr 15, 2024
@SkySkimmer SkySkimmer added the needs: test-suite update Test case should be added to / updated in the test-suite. label Apr 18, 2024
ppedrot added 2 commits April 18, 2024 12:28
@ppedrot
Set some basic rewriting primitives in Type opaque for TC search.
906301d 
The corresponding Prop primitives are already set opaque in Classes.Init,
hence I think this is an overview. These low-level primitives being transparent
mean that TC search when setoid rewriting in Type fires off a crapload of
search branches that should not be there to begin with. Hopefully nobody relies
on that in the wild.
@ppedrot
Document the changes.
73c46f4
@ppedrot ppedrot force-pushed the setoid-type-core-tc-opaque branch from 236e681 to 73c46f4 Compare April 18, 2024 10:29
@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 Apr 18, 2024
@ppedrot ppedrot 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 Apr 18, 2024
@ppedrot
9E88
Copy link
Member Author
ppedrot commented Apr 18, 2024

Just removed the commented out examples from the test.

@ppedrot ppedrot removed the needs: test-suite update Test case should be added to / updated in the test-suite. label Apr 18, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d1da9f7 into rocq-prover:master Apr 19, 2024
6 checks passed
@ppedrot ppedrot deleted the setoid-type-core-tc-opaque branch April 19, 2024 12:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@olaure01 olaure01 olaure01 left review comments

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: fix This fixes a bug or incorrect documentation. part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@ppedrot @SkySkimmer @olaure01
0