The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael,

  Indeed, that's a difference between eauto which executes all tactics then lexicographically order them according to priority and number of subgoals created, and typeclasses eauto which trusts the priorities to execute the tactics in the order so specified. It's not such an easy fix of eauto sadly and probably an incompatible change in some cases...
Best,
-- Matthieu

On Thu, 15 Sep 2016 at 16:58, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/15/2016 10:42 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
>> It wasn't until recently in 8.5 that eauto took the hint costs into consideration at
>> all - it was previously trying hints in most-recent-first order regardless of cost.
>> Yet few noticed.
> I know, I reported the bug.
>
> I guess also taking into account that this change didn't break a lot of developments, this means that few people are using eauto for non-trivial stuff. So I wonder if one could change this behavior as well. I think it is really bad for performance.
>
>

It's not just bad for performance.  There are occasions where one has
multiple subgoals with evar interdependencies such that one cannot
accept just any arbitrary solution to one of the subgoals, as that
solution might prevent solutions in the other(s).  This was the case I
was getting into when I noticed that eauto wasn't respecting hint costs,
as I was trying to carefully arrange hints so that those that solved
subgoals without instantiating "side" evars (hence not interfering with
other subgoals) were given lower costs and so tried first.

I think that although many people are using (e)auto, few are probably
doing so in a way such that the order of hints makes a noticeable
difference.

-- Jonathan