8000 Set firstorder solver explicitly to auto with core in prelude by TheoWinterhalter · Pull Request #20820 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Set firstorder solver explicitly to auto with core in prelude #20820

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 1 commit into
base: master
Choose a base branch
from
Open

Set firstorder solver explicitly to auto with core in prelude #20820

wants to merge 1 commit into from
+1 −1

Conversation

TheoWinterhalter
Copy link
Contributor

This PR proposes to Set Firstorder Solver auto with core. in the prelude so that

Print Firstorder Solver.

outputs

Firstorder solver tactic is auto with core

instead of the current

Firstorder solver tactic is <rocq-runtime.plugins.firstorder::auto_with@0>

which is arguably much less informative / confusing.

@TheoWinterhalter TheoWinterhalter requested a review from a team as a code owner June 27, 2025 13:10
@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 Jun 27, 2025
@TheoWinterhalter @Zimmi48
Set firstorder solver to explicitly use auto with core
98f21d3 
Co-authored-by: Théo Zimmermann <theo.zimmermann@telecom-paris.fr>
@TheoWinterhalter TheoWinterhalter force-pushed the auto_with_core_prelude branch from 66a593c to 98f21d3 Compare June 27, 2025 13:17
@TheoWinterhalter TheoWinterhalter changed the title Set firstorder solver explicitly in prelude Set firstorder solver explicitly to auto with core in prelude Jun 27, 2025
@ppedrot ppedrot self-assigned this Jun 27, 2025
@ppedrot
Copy link
Member
ppedrot commented Jun 27, 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 Jun 27, 2025
@ppedrot ppedrot added the kind: cleanup Code removal, deprecation, refactorings, etc. label Jun 27, 2025
@ppedrot ppedrot added this to the 9.2+rc1 milestone Jun 27, 2025
@ppedrot
Copy link
Member
ppedrot commented Jun 27, 2025 •
edited
Loading

Actually, I checked the code and auto and friends are buggy: if the core db is passed explicitly, it will be used twice in the proof search. Here is a small snippet:

Axiom foo : nat -> False.

Hint Resolve foo : core.

Goal False.
Proof.
debug auto with core.
(* debug auto: *)
(*
* assumption. (*fail*)
* intro. (*fail*)
* simple apply foo (in core). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
* simple apply foo (in core). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
*)

@ppedrot ppedrot added the needs: independent fix The PR reveals an independent bug. label Jun 27, 2025
@ppedrot
Copy link
Member
ppedrot commented Jun 27, 2025

See #20823.

@ppedrot
Copy link
Member
ppedrot commented Jun 27, 2025

Out of curiosity, to assess whether this is really observable, @coqbot bench

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jun 28, 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.76     2.89  -4.50 │    19797654370     19836785636  -0.20 │   96300    96376  -0.08 │
│                        coq-compcert │  309.24   313.20  -1.26 │  2034731012496   2034798496328  -0.00 │ 1146532  1146648  -0.01 │
│                           coq-color │  247.82   250.49  -1.07 │  1566254258966   1565824648622   0.03 │ 1135456  1135128   0.03 │
│                      rocq-equations │    8.92     9.01  -1.00 │    63288804553     63247198050   0.07 │  399588   400220  -0.16 │
│                         rocq-stdlib │  446.25   450.38  -0.92 │  1599262480149   1592522771895   0.42 │  615948   619056  -0.50 │
│          rocq-metarocq-translations │   16.51    16.66  -0.90 │   117463059452    117488171126  -0.02 │  761560   762548  -0.13 │
│                        coq-bedrock2 │  346.17   349.25  -0.88 │  2896402382561   2896237791617   0.01 │  875172   875040   0.02 │
│                 rocq-metarocq-pcuic │  643.64   648.89  -0.81 │  4156300134692   4156282163918   0.00 │ 2324860  2326924  -0.09 │
│                rocq-metarocq-common │   41.87    42.16  -0.69 │   270353716097    270269099112   0.03 │  912624   920424  -0.85 │
│                       coq-fiat-core │   58.09    58.47  -0.65 │   357574730670    357592042935  -0.00 │  484860   488044  -0.65 │
│                 rocq-mathcomp-field │  160.43   161.47  -0.64 │  1215777692266   1215634614233   0.01 │ 1906904  1907060  -0.01 │
│               rocq-metarocq-erasure │  504.92   507.84  -0.57 │  3450245248658   3450549311946  -0.01 │ 1828576  1828556   0.00 │
│                        coq-coqprime │   51.08    51.34  -0.51 │   352439733864    352427656819   0.00 │  805408   807512  -0.26 │
│                        coq-rewriter │  334.78   336.22  -0.43 │  2504979139726   2504940404963   0.00 │ 1311964  1312116  -0.01 │
│                         coq-coqutil │   45.36    45.52  -0.35 │   285440362758    285564120486  -0.04 │  565488   563980   0.27 │
│                             coq-vst │  845.25   847.58  -0.27 │  6441196146170   6441501826448  -0.00 │ 2231836  2235864  -0.18 │
│               coq-engine-bench-lite │  125.14   125.45  -0.25 │   942349549030    940928272458   0.15 │ 1099608  1099584   0.00 │
│              rocq-mathcomp-solvable │   93.72    93.94  -0.23 │   640809895102    640886654107  -0.01 │ 1040148  1043740  -0.34 │
│                      coq-coquelicot │   37.89    37.96  -0.18 │   228682783606    228735065657  -0.02 │  826392   828356  -0.24 │
│                         coq-unimath │ 1756.62  1759.48  -0.16 │ 14653316193122  14652868975482   0.00 │ 1086976  1089056  -0.19 │
│                    coq-fiat-parsers │  278.68   279.11  -0.15 │  2148329014395   2148369543450  -0.00 │ 2349712  2353800  -0.17 │
│                    coq-math-classes │   86.52    86.60  -0.09 │   534227643429    533177641900   0.20 │  512612   513564  -0.19 │
│              rocq-mathcomp-fingroup │   23.26    23.28  -0.09 │   152132922352    152097230704   0.02 │  530960   531192  -0.04 │
│             rocq-mathcomp-character │   87.24    87.29  -0.06 │   615319912270    614817644813   0.08 │ 1475500  1482028  -0.44 │
│                       coq-fourcolor │ 1331.85  1332.19  -0.03 │ 12372418881753  12373442557032  -0.01 │  896496   896724  -0.03 │
│               rocq-mathcomp-algebra │  285.71   285.77  -0.02 │  2133160549164   2133814436124  -0.03 │ 1422284  1422316  -0.00 │
│                        rocq-bignums │   27.82    27.82   0.00 │   181170096416    181177086758  -0.00 │  480336   480428  -0.02 │
│             rocq-mathcomp-ssreflect │    1.29     1.29   0.00 │     9177645096      9180853611  -0.03 │  556536   556592  -0.01 │
│         coq-rewriter-perf-SuperFast │  477.23   477.07   0.03 │  3742458449922   3743563886072  -0.03 │ 1239148  1245892  -0.54 │
│              coq-mathcomp-odd-order │  580.91   580.55   0.06 │  4172370750103   4172105144369   0.01 │ 2222888  2224252  -0.06 │
│                 rocq-metarocq-utils │   23.21    23.17   0.17 │   151348858315    151334404673   0.01 │  584108   581124   0.51 │
│              rocq-metarocq-template │   82.29    82.14   0.18 │   570079245968    570101448235  -0.00 │  992756   992672   0.01 │
│                      coq-verdi-raft │  527.28   526.31   0.18 │  3681877232088   3681823476037   0.00 │  845060   847728  -0.31 │
│           rocq-metarocq-safechecker │  321.98   321.33   0.20 │  2410214971704   2410327145709  -0.00 │ 1787872  1786796   0.06 │
│                           rocq-core │    6.36     6.34   0.32 │    39182922635     39084464187   0.25 │  445048   441996   0.69 │
│                            coq-corn │  681.20   678.91   0.34 │  4691976655844   4689158872013   0.06 │  708728   709204  -0.07 │
│          coq-performance-tests-lite │  890.63   887.07   0.40 │  7188273958215   7188646472451  -0.01 │ 1938792  1940544  -0.09 │
│                            coq-hott │  154.66   154.03   0.41 │  1067566310210   1067613687527  -0.00 │  486220   489128  -0.59 │
│ coq-neural-net-interp-computed-lite │  232.92   231.97   0.41 │  2249442591154   2249426139049   0.00 │  902180   905856  -0.41 │
│                 coq-category-theory │  614.84   612.33   0.41 │  4517313628849   4517215072703   0.00 │  973956   972316   0.17 │
│               coq-mathcomp-analysis │  914.28   909.84   0.49 │  6789659325295   6793279906985  -0.05 │ 1917468  1917360   0.01 │
│                        rocq-runtime │   74.15    73.77   0.52 │   536717535133    536530502955   0.03 │  494304   494232   0.01 │
│                   coq-iris-examples │  358.72   355.97   0.77 │  2380976188250   2380990908126  -0.00 │ 1062168  1060380   0.17 │
│                           coq-verdi │   44.29    43.90   0.89 │   295227584871    295130696199   0.03 │  527360   525508   0.35 │
│                           rocq-elpi │   12.86    12.72   1.10 │    91763114924     91696529925   0.07 │  485068   485664  -0.12 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-fiat-crypto-with-bedrock (in NEW)

🐢 Top 25 slow downs 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                    │
│  OLD    NEW    DIFF    %DIFF    Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  93.5   94.9  1.4044    1.50%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  93.4   94.6  1.2076    1.29%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   198    199  0.6265    0.32%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│ 0.434  0.883  0.4492  103.56%   474  rocq-stdlib/theories/MSets/MSetWeakList.v.html                                                │
│  1.10   1.50  0.4003   36.38%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│ 0.229  0.620  0.3910  171.05%   707  rocq-stdlib/theories/MSets/MSetList.v.html                                                    │
│ 0.558  0.925  0.3667   65.70%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│ 0.385  0.749  0.3640   94.45%  1982  rocq-stdlib/theories/FSets/FMapFacts.v.html                                                   │
│  2.25   2.56  0.3008   13.34%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│ 0.472  0.758  0.2864   60.68%    13  rocq-stdlib/theories/FSets/FMapPositive.v.html                                                │
│ 0.251  0.532  0.2814  112.23%    11  rocq-stdlib/theories/QArith/Qminmax.v.html                                                    │
│ 0.367  0.647  0.2802   76.30%   487  rocq-stdlib/theories/MSets/MSetWeakList.v.html                                                │
│  26.6   26.9  0.2502    0.94%    12  coq-fourcolor/theories/proof/job611to617.v.html                                               │
│  27.0   27.2  0.2192    0.81%    12  coq-fourcolor/theories/proof/job287to290.v.html                                               │
│  3.08   3.30  0.2179    7.08%   213  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                            │
│ 0.254  0.470  0.2163   85.20%   313  rocq-stdlib/theories/Reals/Abstract/ConstructiveLUB.v.html                                    │
│ 0.218  0.432  0.2139   97.99%   246  rocq-stdlib/theories/Structures/OrdersEx.v.html                                               │
│  25.3   25.5  0.2031    0.80%    12  coq-fourcolor/theories/proof/job499to502.v.html                                               │
│  5.16   5.37  0.2022    3.92%   130  coq-category-theory/Functor/Strong/Product.v.html                                             │
│ 0.470  0.667  0.1969   41.89%    10  rocq-mathcomp-character/character/vcharacter.v.html                                           │
│ 0.316  0.512  0.1959   62.00%   868  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│ 0.223  0.418  0.1958   87.97%   330  coq-corn/metric2/FinEnum.v.html                                                               │
│  23.0   23.2  0.1939    0.84%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html            │
│  20.4   20.5  0.1689    0.83%    12  coq-fourcolor/theories/proof/job283to286.v.html                                               │
│  1.26   1.43  0.1644   13.03%     7  coq-mathcomp-analysis/theories/lebesgue_measure.v.html                                        │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                  TOP 25 SPEED UPS                                                  │
│                                                                                                                    │
│  OLD     NEW     DIFF     %DIFF    Ln                 FILE                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   66.5    63.0  -3.5200   -5.29%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                │
│   40.1    38.8  -1.3310   -3.32%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│   3.95    3.29  -0.6611  -16.74%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                              │
│  0.864   0.261  -0.6026  -69.74%    12  rocq-stdlib/theories/MSets/MSets.v.html                                    │
│   9.37    8.99  -0.3810   -4.07%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                         │
│   36.9    36.5  -0.3786   -1.03%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html               │
│  0.544   0.171  -0.3731  -68.62%   731  rocq-stdlib/theories/MSets/MSetRBT.v.html                                  │
│ 41.093  40.728  -0.3650   -0.89%   834  coq-vst/veric/binop_lemmas4.v.html                                         │
│   1.65    1.30  -0.3460  -20.98%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                  │
│   8.64    8.33  -0.3092   -3.58%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                          │
│  0.400   0.107  -0.2931  -73.29%    12  rocq-stdlib/theories/Reals/Abstract/ConstructiveAbs.v.html                 │
│  0.460   0.183  -0.2764  -60.12%   586  rocq-stdlib/theories/Strings/Byte.v.html                                   │
│  0.620   0.359  -0.2606  -42.05%    13  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                           │
│   21.7    21.4  -0.2436   -1.13%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                  │
│   3.13    2.89  -0.2336   -7.47%  1447  rocq-metarocq-erasure/erasure/theories/ErasureFunction.v.html              │
│   24.0    23.8  -0.2320   -0.97%    12  coq-fourcolor/theories/proof/job486to489.v.html                            │
│  0.446   0.227  -0.2185  -49.03%   719  rocq-stdlib/theories/MSets/MSetRBT.v.html                                  │
│  0.593   0.375  -0.2180  -36.79%    21  rocq-stdlib/theories/FSets/FMapAVL.v.html                                  │
│   3.80    3.59  -0.2132   -5.61%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html       │
│  0.516   0.309  -0.2070  -40.12%    45  rocq-stdlib/theories/Logic/Diaconescu.v.html                               │
│   8.57    8.37  -0.2011   -2.35%   925  coq-mathcomp-odd-order/theories/PFsection4.v.html                          │
│   28.3    28.1  -0.1948   -0.69%    12  coq-fourcolor/theories/proof/job563to588.v.html                            │
│  0.454   0.259  -0.1942  -42.80%  1652  rocq-stdlib/theories/FSets/FMapAVL.v.html                                  │
│ 10.726  10.535  -0.1910   -1.78%   985  coq-vst/floyd/closed_lemmas.v.html                                         │
│  7.651   7.462  -0.1890   -2.47%  1220  coq-vst/floyd/Component.v.html                                             │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ppedrot
Copy link
Member
ppedrot commented Jun 28, 2025

So it is actually observable, at least in the stdlib.

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

@ppedrot ppedrot

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. needs: independent fix The PR reveals an independent bug.
Projects
None yet
Milestone
9.2+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@TheoWinterhalter @ppedrot
0