The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Armaël,

in my experience including the core hint database frequently leads to bad 
proof search performance. E.g. the core hint database includes hints which 
can loop to the  search depth limit on some goals. I would generally 
recommend to apply proper engineering practices in designing hint databases 
and to not provide a substantially larger set of hints than required.

I typically use a set of tactics and/or tactic notations to wrap eauto with 
certain sets of hint databases suitable for specific problems. This wrapping 
also makes it easier to switch between eauto and typeclasses eauto, which is 
a good idea to try. Also if eauto is used, one can easily add the debug flag 
(for typeclasses eauto it is a global option). It is a good idea to have a 
look at the logs and the branching factors of the proof search.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Armaël Guéneau
Sent: Wednesday, November 14, 2018 8:28 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Moving away from putting hints in the core hintdb

Dear coq-club,

I just finished a Coq development, which I now want to publish, and I'm 
facing the following issue:

While doing my development, I added a good number of hints (mainly Hint 
Resolve and Hint Constructor) to the default database (ie "core" if I'm not 
mistaking).
This was because it's much more convenient to write "eauto" everywhere than 
"eauto with mybase" which is a lot more annoying to type(!).

But now, anyone loading my development will get its core database polluted 
with my hints, which is very bad.

How can I refactor my project to avoid this?

My project spans across several files, and I'd like to share the hints across 
the files, so delimiting them within a Section doesn't quite work I think.
I could do "Tactic Notation go := eauto with mybase" but that doesn't scale 
to [eauto using ... with ...].
Using "eauto with mybase" manually is annoying because I use the tactic in a 
lot of places.

Even if it doesn't exist currently, I wonder what would be a nice solution to 
this problem. Having a way of defining variants of (e)auto that use different 
hint bases (while supporting all the [using ..], [with ..] variants) sounds 
useful, I think?

— Armaël
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