[eauto] do not eagerly evaluate extern hints #16289

mrhaandi · 2022-07-05T17:41:15Z

Instead of eagerly evaluate every extern hint for success (which can be arbitrarily slow), approximate the subgoal cost by hint priority.
This forces eauto to respect priorities of Extern hints.
Also, this is more coherent with auto and typeclasses eauto behavior (see regression tests).

Fixes #5163
Fixes #16282 (and #15558)

Added / updated test-suite.
Added changelog.
Opened overlay pull requests.
- metacoq prepare for https://github.com/coq/coq/pull/16289 MetaCoq/metacoq#734
- stdpp (merged) https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/385

SkySkimmer · 2022-07-05T18:45:01Z

@coqbot bench

Alizter · 2022-07-05T19:01:59Z

@Zimmi48 Could you add @mrhaandi to the contributors team?

Zimmi48 · 2022-07-05T21:30:50Z

I'll do this when I get in front of a computer. We should add a feature to coqbot to support adding new members to the contributors, and even maintainer teams.

mrhaandi · 2022-07-06T04:59:21Z

I'll do this when I get in front of a computer.

@Zimmi48 If possible, it would be great if I also could manually abort/rerun tests in the GitLab CI pipeline.

Zimmi48 · 2022-07-06T07:29:12Z

@mrhaandi I have invited you to the GitHub and GitLab organization. Be mindful that you now have write access to the repository, which means that you can triage issues and pull requests (label, close, edit comments, etc.), but also (because GitHub doesn't allow us to control this) that you can push new branches and should not do it. So be careful where you push and do not use the Edit button on a file in the main repository because this would create a branch in the main repository and not on your fork. To restart GitLab pipelines, you can use the Retry button directly in the GitHub checks tab. To cancel one, I think the only option is going to GitLab to do so.

coqbot-app · 2022-07-06T09:46:14Z

🏁 Bench results:

┌──────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬───────────────────┐
│                              │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │    mem faults     │
│                              │                         │                                       │                                       │                         │                   │
│         package_name         │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │ NEW  OLD   PDIFF  │
├──────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤
│                 coq-compcert │  351.95   358.13  -1.73 │  1476954607822   1498164547937  -1.42 │  2057185211207   2058062497566  -0.04 │ 1121852  1121404   0.04 │   0   38  -100.00 │
│          coq-category-theory │ 1206.30  1212.03  -0.47 │  5062414521728   5087768190384  -0.50 │  7752628466267   7752023641961   0.01 │ 1316528  1316492   0.00 │   0    0      nan │
│               coq-coquelicot │   42.24    42.41  -0.40 │   175868784759    175230818652   0.36 │   221177373036    221243196568  -0.03 │  748508   754420  -0.78 │  49    0      nan │
│                 coq-bedrock2 │  491.48   492.15  -0.14 │  2087030833178   2086811736275   0.01 │  3308107853876   3310871175279  -0.08 │ 1830864  1830788   0.00 │   9    0      nan │
│                   coq-stdlib │  531.25   531.97  -0.14 │  1718646741325   1712550570498   0.36 │  1513776624013   1513863085778  -0.01 │  702736   698564   0.60 │   0    0      nan │
│                    coq-verdi │   58.19    58.25  -0.10 │   243128402383    242988330992   0.06 │   337340121793    337618836181  -0.08 │  775972   779416  -0.44 │  10    0      nan │
│                coq-fiat-core │   68.11    68.17  -0.09 │   273722297039    273052044764   0.25 │   361210864207    361384507078  -0.05 │  477660   477392   0.06 │   3    0      nan │
│                     coq-corn │  959.59   959.86  -0.03 │  4033634167740   4037918178118  -0.11 │  5793511371269   5794293995401  -0.01 │  922884   924608  -0.19 │   0    0      nan │
│       coq-mathcomp-character │   81.83    81.82   0.01 │   344043638973    343829020330   0.06 │   480703761317    480688893359   0.00 │  716324   719652  -0.46 │   0    0      nan │
│                     coq-hott │  196.78   196.72   0.03 │   822944253156    821375301562   0.19 │  1205190629783   1204781643618   0.03 │  582484   583312  -0.14 │   0    0      nan │
│         coq-mathcomp-algebra │   72.97    72.85   0.16 │   307821200516    307046154819   0.25 │   394814881311    394714505132   0.03 │  553460   553364   0.02 │   0    0      nan │
│             coq-math-classes │  113.72   113.51   0.19 │   476168597802    474974037027   0.25 │   634184676178    634542575694  -0.06 │  507616   505324   0.45 │   0    0      nan │
│   coq-performance-tests-lite │  991.81   989.86   0.20 │  4188897644128   4182103794942   0.16 │  6385824857208   6395344529758  -0.15 │ 2326804  2326568   0.01 │   2    0      nan │
│         coq-metacoq-template │  167.45   167.12   0.20 │   697842939672    695071904550   0.40 │  1024689227832   1025216076100  -0.05 │ 1204436  1193840   0.89 │   1    0      nan │
│           coq-mathcomp-field │  119.52   119.27   0.21 │   502600671134    501434533577   0.23 │   744652992115    744773034141  -0.02 │  637892   639016  -0.18 │   0    0      nan │
│                   coq-geocoq │  877.34   875.44   0.22 │  3693510331845   3682456516197   0.30 │  5235828609962   5236221254106  -0.01 │  978884   978832   0.01 │   0    0      nan │
│  coq-rewriter-perf-SuperFast │ 1109.10  1105.68   0.31 │  4690760026290   4684148035348   0.14 │  7198401671987   7195631531202   0.04 │ 1125896  1125840   0.00 │  26    0      nan │
│                    coq-color │  274.86   274.01   0.31 │  1148314249958   1144274171280   0.35 │  1504173116719   1504136221150   0.00 │ 1134340  1134192   0.01 │   1    1     0.00 │
│                 coq-rewriter │  408.53   407.16   0.34 │  1718147936147   1715454793155   0.16 │  2530043891123   2530418023302  -0.01 │ 1018828   969032   5.14 │   4    0      nan │
│                  coq-unimath │ 6251.77  6229.10   0.36 │ 26183048057492  26093535952643   0.34 │ 46038833284881  46029051488729   0.02 │ 3861636  3861476   0.00 │   1    0      nan │
│                   coq-flocq3 │   90.21    89.86   0.39 │   376827754438    374915527641   0.51 │   466372007414    466476764873  -0.02 │  990820   990916  -0.01 │   0    0      nan │
│             coq-fiat-parsers │  423.58   421.86   0.41 │  1778899708087   1770721075207   0.46 │  2580203302341   2577691747492   0.10 │ 3440676  3440868  -0.01 │   0    0      nan │
│        coq-engine-bench-lite │  216.43   215.37   0.49 │   906626431368    901694672499   0.55 │  1404185209691   1398677570000   0.39 │ 1229624  1099348  11.85 │   0    0      nan │
│                coq-fourcolor │ 1759.96  1750.04   0.57 │  7537783250608   7487780448264   0.67 │ 12224311823114  12224666909336  -0.00 │  724508   723964   0.08 │   0    0      nan │
│        coq-mathcomp-solvable │   99.55    98.98   0.58 │   417502931453    415668421969   0.44 │   586148339161    586117536745   0.01 │  650536   648516   0.31 │   0    0      nan │
│                 coq-coqprime │   52.98    52.66   0.61 │   221295702107    220437703365   0.39 │   303538557447    302952133515   0.19 │  753804   753664   0.02 │   0    0      nan │
│                  coq-coqutil │   42.75    42.48   0.64 │   176677974076    176042473965   0.36 │   232215494978    232165292550   0.02 │  586144   586224  -0.01 │   0    0      nan │
│                     coq-core │  146.79   145.85   0.64 │   461395281205    458222641006   0.69 │   483753290216    483470529164   0.06 │  286512   286136   0.13 │   0    0      nan │
│        coq-mathcomp-fingroup │   26.68    26.50   0.68 │   112225419219    111805407625   0.38 │   151843025769    151800251219   0.03 │  489568   487392   0.45 │   0    0      nan │
│                  coq-bignums │   33.74    33.38   1.08 │   141791497999    140753986593   0.74 │   183617219612    183568478399   0.03 │  467592   468832  -0.26 │   0    0      nan │
│       coq-mathcomp-odd-order │  612.10   605.04   1.17 │  2566929795471   2540047456040   1.06 │  4052690790794   4053062820770  -0.01 │  864512   863808   0.08 │   0    0      nan │
│       coq-mathcomp-ssreflect │   30.93    30.54   1.28 │   130022866779    128998304445   0.79 │   154905305448    154804901131   0.06 │  536456   532148   0.81 │   0    0      nan │
│ coq-fiat-crypto-with-bedrock │ 7025.48  6917.81   1.56 │ 29217191212644  28793185804890   1.47 │ 47146399347237  46678174273951   1.00 │ 3836912  3836896   0.00 │  84   83     1.20 │
│     coq-metacoq-translations │   18.18    17.87   1.73 │    76253771266     75863738155   0.51 │   105272400666    105265458755   0.01 │  770520   770404   0.02 │  20    0      nan │
│               coq-verdi-raft │  712.84   671.92   6.09 │  2984920561294   2811529253237   6.17 │  4258451550715   4023293782499   5.84 │ 1199516  1201040  -0.13 │   0    0      nan │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SLOW DOWNS                                                                   │
│                                                                                                                                                      │
│   OLD       NEW      DIFF      %DIFF      Ln                      FILE                                                                               │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.0400   82.6380  82.5980  206495.00%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                   │
│   0.0910   20.3390  20.2480   22250.55%   417  coq-verdi-raft/raft-proofs/LeaderLogsLogMatchingProof.v.html                                          │
│   0.0080   12.5140  12.5060  156325.00%  1270  coq-verdi-raft/raft/CommonTheorems.v.html                                                             │
│   0.0050    6.5520   6.5470  130940.00%   575  coq-verdi-raft/raft/CommonTheorems.v.html                                                             │
│  19.7400   21.3990   1.6590       8.40%    29  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                             │
│  47.7700   48.8410   1.0710       2.24%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                        │
│  81.6210   82.6400   1.0190       1.25%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                          │
│  63.9600   64.9210   0.9610       1.50%   543  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                      │
│ 230.5170  231.4280   0.9110       0.40%   139  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                            │
│  49.6130   50.3840   0.7710       1.55%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                            │
│  73.9020   74.6470   0.7450       1.01%   641  coq-unimath/UniMath/SubstitutionSystems/LiftingInitial_alt.v.html                                     │
│  26.3830   27.1070   0.7240       2.74%    15  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p256_64.v.html                      │
│  25.3510   26.0500   0.6990       2.76%    15  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p256_64.v.html                      │
│  15.8920   16.5890   0.6970       4.39%   158  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│ 135.6490  136.3340   0.6850       0.50%  1104  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v.html     │
│   9.4380   10.0990   0.6610       7.00%  3259  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                                   │
│  18.1020   18.7450   0.6430       3.55%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html                                      │
│  30.4730   31.1080   0.6350       2.08%    19  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/X25519_64.v.html                    │
│  37.5720   38.1340   0.5620       1.50%   352  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                    │
│  33.8960   34.4540   0.5580       1.65%  1157  coq-unimath/UniMath/Bicategories/DisplayedBicats/Cartesians.v.html                                    │
│  34.0350   34.5580   0.5230       1.54%    10  coq-fourcolor/theories/job611to617.v.html                                                             │
│  99.5350  100.0420   0.5070       0.51%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                           │
│ 116.3880  116.8910   0.5030       0.43%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                │
│  33.8280   34.3230   0.4950       1.46%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │
│  28.7130   29.2050   0.4920       1.71%    10  coq-fourcolor/theories/job303to306.v.html                                                             │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                │
│                                                                                                                                                │
│   OLD       NEW      DIFF     %DIFF     Ln                     FILE                                                                            │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  21.7490   20.2000  -1.5490    -7.12%    30  coq-performance-tests-lite/src/pattern.v.html                                                     │
│ 163.6270  162.2500  -1.3770    -0.84%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│ 163.5580  162.6460  -0.9120    -0.56%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│ 182.1140  181.5570  -0.5570    -0.31%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│  30.6690   30.1200  -0.5490    -1.79%   310  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveProducts.v.html  │
│   5.3900    4.8910  -0.4990    -9.26%   239  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html  │
│   1.3010    0.8420  -0.4590   -35.28%   221  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/Spilling.v.html              │
│  16.5710   16.1340  -0.4370    -2.64%    52  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/Field25519.v.html                         │
│  20.3430   19.9430  -0.4000    -1.97%  1286  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v.html │
│  15.4730   15.1070  -0.3660    -2.37%  1552  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                       │
│   2.8900    2.5240  -0.3660   -12.66%   748  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│  19.8480   19.5300  -0.3180    -1.60%    10  coq-fourcolor/theories/job215to218.v.html                                                         │
│  49.6630   49.3570  -0.3060    -0.62%   633  coq-unimath/UniMath/SubstitutionSystems/Signatures.v.html                                         │
│   0.2950    0.0000  -0.2950  -100.00%   727  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v.html      │
│  13.9790   13.7160  -0.2630    -1.88%  1518  coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html                │
│  68.4520   68.2270  -0.2250    -0.33%   857  coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html                │
│   4.2400    4.0220  -0.2180    -5.14%  1891  coq-bedrock2/bedrock2/src/bedrock2Examples/LiveVerif/swap.v.html                                  │
│   0.7840    0.5720  -0.2120   -27.04%   216  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                               │
│  10.1190    9.9070  -0.2120    -2.10%  1668  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│   9.8740    9.6660  -0.2080    -2.11%    84  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                             │
│  16.2390   16.0370  -0.2020    -1.24%    93  coq-category-theory/Functor/Construction/Product/Monoidal.v.html                                  │
│   8.5490    8.3510  -0.1980    -2.32%   498  coq-unimath/UniMath/Bicategories/Limits/InserterEquivalences.v.html                               │
│  33.0330   32.8380  -0.1950    -0.59%    10  coq-fourcolor/theories/job223to226.v.html                                                         │
│  16.2150   16.0250  -0.1900    -1.17%   604  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html           │
│  17.7560   17.5690  -0.1870    -1.05%   187  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                          │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

mrhaandi · 2022-07-06T10:05:35Z

The ci issues are easy to fix (use auto when eauto would leave shelved goals).
The bench results are mixed. Essentially this PR makes eauto respect the cost of extern hints whereas before it eagerly applied them, disregarding the cost. This eagerness can be faster (basically partial bfs).

mrhaandi · 2022-07-07T13:14:12Z

stdpp breaks at exactly one position (commit): in list.v.
The reason is: before this PR eauto neglected the cost of the extern hint lia (and applied it first).
However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof.
Changing eauto to auto at the specific position would avoid the evar issue.

@RalfJung Since there is no good overlay mechanism for stdpp, I would just file a PR for stdpp.

mrhaandi · 2022-07-08T06:02:08Z

@RalfJung as soon as ci-perennial gets an stdpp and iris bump, then it also will compile correctly with this PR.

mrhaandi · 2022-07-08T07:26:40Z

@ppedrot with this PR the module UnsafeRepr in engine/proofview.ml is not used by Coq anymore (so there is potential for removal/simplification).

ppedrot · 2022-07-08T09:52:38Z

Don't remove UnsafeRepr, it's potentially useful for plugins that want to hack around. It was there before eauto used it, actually.

RalfJung · 2022-07-08T21:00:07Z

@RalfJung as soon as ci-perennial gets an stdpp and iris bump, then it also will compile correctly with this PR.

I have bumped them there.

mrhaandi · 2022-07-08T22:05:29Z

I have bumped them there.

Possibly, it is the coq/tested branch in perennial which is used by ci and needs a bump.

RalfJung · 2022-07-09T01:41:54Z

I think there's a nightly CI job doing that, or so... Cc @tchajed

tchajed · 2022-07-09T02:28:01Z

Yes, the coq/tested branch gets forwarded to match master automatically every night (Eastern time). It'll still take some time in this particular case because we need to wait for our own CI to finish.

coqbot-app · 2022-07-09T05:37:57Z

🔴 CI failure at commit b7b5a27 without any failure in the test-suite

✔️ Corresponding job for the base commit 672b144 succeeded

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

🏃 @coqbot ci minimize will minimize the following target: ci-vst

You can also pass me a specific list of targets to minimize as arguments.

mrhaandi · 2022-07-18T12:32:04Z

All overlays are merged into their respective projects, so I do not include an user-overlay script anymore.
Also now rebased and squashed.

doc/changelog/04-tactics/16289-eauto-cost.rst

ppedrot · 2022-07-19T21:22:14Z

The category-theory CI failure is unrelated, it's also happening in master. @Zimmi48 if you're fine with the current doc, I can merge.

mrhaandi · 2022-07-20T08:28:58Z

Rebased and squashed for merge.

ppedrot · 2022-07-21T16:33:10Z

@coqbot merge now

mrhaandi mentioned this pull request Jul 7, 2022

[eauto] consider shelf in cost_subgoals #16286

Closed

3 tasks

mrhaandi added a commit to mrhaandi/metacoq that referenced this pull request Jul 7, 2022

prepare for coq/coq#16289

3a38f3f

mrhaandi marked this pull request as ready for review July 7, 2022 13:23

mrhaandi requested a review from a team as a code owner July 7, 2022 13:23

mrhaandi force-pushed the eauto-cost branch from c889d09 to 7372d76 Compare July 7, 2022 15:51

mrhaandi force-pushed the eauto-cost branch from 5ac1581 to b7b5a27 Compare July 8, 2022 07:42

coq deleted a comment from coqbot-app bot Jul 9, 2022

ppedrot self-assigned this Jul 9, 2022

mrhaandi force-pushed the eauto-cost branch from b7b5a27 to e6a2437 Compare July 12, 2022 04:40

mrhaandi mentioned this pull request Jul 13, 2022

[eauto] goal loop detection #16317

Closed

mrhaandi added this to In Progress in auto and eauto based on typeclasses eauto Jul 18, 2022

yforster pushed a commit to MetaCoq/metacoq that referenced this pull request Jul 18, 2022

prepare for coq/coq#16289 (#734)

bc3a9a8

mrhaandi force-pushed the eauto-cost branch from e6a2437 to 874543f Compare July 18, 2022 12:29

ppedrot reviewed Jul 18, 2022

View reviewed changes

doc/changelog/04-tactics/16289-eauto-cost.rst Show resolved Hide resolved

ppedrot approved these changes Jul 19, 2022

View reviewed changes

ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Jul 19, 2022

ppedrot added this to the 8.17+rc1 milestone Jul 19, 2022

Zimmi48 approved these changes Jul 20, 2022

View reviewed changes

in eauto do not eagerly evaluate extern hints

b759db3

mrhaandi force-pushed the eauto-cost branch from 2901e22 to b759db3 Compare July 20, 2022 08:28

coqbot-app bot merged commit d627f2d into coq:master Jul 21, 2022

auto and eauto based on typeclasses eauto automation moved this from In Progress to Done Jul 21, 2022

mattam82 pushed a commit to MetaCoq/metacoq that referenced this pull request Apr 13, 2023

prepare for coq/coq#16289 (#734)

7d1b643

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[eauto] do not eagerly evaluate extern hints #16289

[eauto] do not eagerly evaluate extern hints #16289

mrhaandi commented Jul 5, 2022 •

edited

SkySkimmer commented Jul 5, 2022

Alizter commented Jul 5, 2022

Zimmi48 commented Jul 5, 2022 •

edited

mrhaandi commented Jul 6, 2022

Zimmi48 commented Jul 6, 2022

coqbot-app bot commented Jul 6, 2022

mrhaandi commented Jul 6, 2022

mrhaandi commented Jul 7, 2022

mrhaandi commented Jul 8, 2022

mrhaandi commented Jul 8, 2022

ppedrot commented Jul 8, 2022

RalfJung commented Jul 8, 2022

mrhaandi commented Jul 8, 2022

RalfJung commented Jul 9, 2022

tchajed commented Jul 9, 2022

coqbot-app bot commented Jul 9, 2022

mrhaandi commented Jul 18, 2022

ppedrot commented Jul 19, 2022

mrhaandi commented Jul 20, 2022

ppedrot commented Jul 21, 2022

[eauto] do not eagerly evaluate extern hints #16289

[eauto] do not eagerly evaluate extern hints #16289

Conversation

mrhaandi commented Jul 5, 2022 • edited

SkySkimmer commented Jul 5, 2022

Alizter commented Jul 5, 2022

Zimmi48 commented Jul 5, 2022 • edited

mrhaandi commented Jul 6, 2022

Zimmi48 commented Jul 6, 2022

coqbot-app bot commented Jul 6, 2022

mrhaandi commented Jul 6, 2022

mrhaandi commented Jul 7, 2022

mrhaandi commented Jul 8, 2022

mrhaandi commented Jul 8, 2022

ppedrot commented Jul 8, 2022

RalfJung commented Jul 8, 2022

mrhaandi commented Jul 8, 2022

RalfJung commented Jul 9, 2022

tchajed commented Jul 9, 2022

coqbot-app bot commented Jul 9, 2022

mrhaandi commented Jul 18, 2022

ppedrot commented Jul 19, 2022

mrhaandi commented Jul 20, 2022

ppedrot commented Jul 21, 2022

mrhaandi commented Jul 5, 2022 •

edited

Zimmi48 commented Jul 5, 2022 •

edited