The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 10/15/2015 10:04 PM, Jason Gross wrote:
> I'm not sure.  You can test it, or comment on the bug, or look for the
> relevant commit and see what it changed?

Tested it and commented.

-- Jonathan

> 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