The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm not sure.  You can test it, or comment on the bug, or look for the relevant commit and see what it changed?

On Thu, Oct 15, 2015 at 9:54 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Yes - it does actually look like the cost is not taken into account at all, and the hints are just used in reverse declaration order (last declared first used).

But, it says that the bug is fixed.  I'm using a fairly recent 8.5 build (db80daa).  Is this a regression?  Or, was it fixed for eauto but not for auto?

-- Jonathan

On 10/15/2015 09:15 PM, Jason Gross wrote:

I think you may be looking for bug 3199
<https://coq.inria.fr/bugs/show_bug.cgi?id=3199>?

On Thu, Oct 15, 2015 at 7:10 PM, Jonathan Leivent <jonikelee AT gmail.com>
wrote:

Is it the case that auto is supposed to try all (pattern applicable) hints
in ascending cost order, regardless of hint declaration order?  That seems
to be what the refman implies - although it says very little about cost.
However, there appear to be cases where auto will try a higher cost hint
that was declared later before a lower cost hint declared earlier.  Is that
a bug?

Interestingly, it looks like using auto with nocore and a small db can
outperform combining the hints from that small db into a single recursive
match-based tactic.  However, I'm finding it difficult to use hint cost to
control the order in which hints are tried.

-- Jonathan