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.
From: firstname.lastname@example.org [mailto:email@example.com] On Behalf Of Armaël Guéneau
Sent: Wednesday, November 14, 2018 8:28 PM
Subject: [Coq-Club] Moving away from putting hints in the core hintdb
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?
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: Amtsgeric