coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Is eauto behavior desirable?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Is eauto behavior desirable?
Date: Thu, 15 Sep 2016 14:42:33 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:3QB+UBM27JdqC7pOuBUl6mtUPXoX/o7sNwtQ0KIMzox0KPz9rarrMEGX3/hxlliBBdydsKMdzbWL+P+/ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJH93OervpbXfg9ghTynYLo0Ig/85VHasdBTio9/II4wzAHIqz1GYbIF63lvIAfZpBHx6duq+4YnuwFRsPIo+soKGfH/fq84RLFcSi8hPm8p/srznRjFUQaLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu78l1Q==

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.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
  - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
    - Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
      - Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/19/2016
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/20/2016
        
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016
      - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016