The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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