[Coq-Club] Moving away from putting hints in the core hintdb

[Armaël Guéneau]

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

[Gaëtan Gilbert]

I think currently there is no better way than manual "with mybase".

Maybe we could add an option "Set Default HintBase mybase", then you
could use regular option scoping.

ie either put "Set" at the top of every file or module you want it in,
or "Export Set" in FooOptions.v (where Foo is your project) and import
that everywhere you want it in.


Gaëtan Gilbert

Post by Armaël Guéneau
Dear coq-club,
I just finished a Coq development, which I now want to publish, and I'm
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

[Armaël Guéneau]

Thanks for the answer!

Post by Gaëtan Gilbert
Maybe we could add an option "Set Default HintBase mybase", then you
could use regular option scoping.
ie either put "Set" at the top of every file or module you want it in,
or "Export Set" in FooOptions.v (where Foo is your project) and import
that everywhere you want it in.

I think that would be very nice indeed -- maybe generalized to allow
providing a list of default bases? (e.g. Set Default HintBase mybase,
core, arith)

(alternatively, if there was a way to merge databases / import hints
from one in another, it would be enough for the option to take one base;
but there isn't at the moment AFAIK)

[Jason -Zhong Sheng- Hu]

This is a very interesting discussion, because core database is too polluted whenever working with others' modules. The situation is getting worse when different projects cross together and produce weird interactions.

I'm wondering if there's some plan to introduce modularity in hint databases? It would be very helpful if hints can be grouped as modules and can be opened, closed and injected from one database to another.

Thanks,
Jason Hu


-------- Original message --------
From: Armaël Guéneau <***@ens-lyon.fr>
Date: 11/14/18 15:10 (GMT-05:00)
To: coq-***@inria.fr, Gaëtan Gilbert <***@skyskimmer.net>
Subject: Re: [Coq-Club] Moving away from putting hints in the core hintdb

Thanks for the answer!

Post by Gaëtan Gilbert
Maybe we could add an option "Set Default HintBase mybase", then you
could use regular option scoping.
ie either put "Set" at the top of every file or module you want it in,
or "Export Set" in FooOptions.v (where Foo is your project) and import
that everywhere you want it in.

I think that would be very nice indeed -- maybe generalized to allow
providing a list of default bases? (e.g. Set Default HintBase mybase,
core, arith)

(alternatively, if there was a way to merge databases / import hints
from one in another, it would be enough for the option to take one base;
but there isn't at the moment AFAIK)

[Vadim Zaliva]

One approach would be is scope-like. "Open HindDB" which could be nested.

Vadim

--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone]



On Wed, Nov 14, 2018 at 12:59 PM Jason -Zhong Sheng- Hu <

Post by Jason -Zhong Sheng- Hu
This is a very interesting discussion, because core database is too
polluted whenever working with others' modules. The situation is getting
worse when different projects cross together and produce weird
interactions.
I'm wondering if there's some plan to introduce modularity in hint
databases? It would be very helpful if hints can be grouped as modules and
can be opened, closed and injected from one database to another.
Thanks,
Jason Hu
-------- Original message --------
Date: 11/14/18 15:10 (GMT-05:00)
Subject: Re: [Coq-Club] Moving away from putting hints in the core hintdb
Thanks for the answer!

Post by Gaëtan Gilbert
Maybe we could add an option "Set Default HintBase mybase", then you
could use regular option scoping.
ie either put "Set" at the top of every file or module you want it in,
or "Export Set" in FooOptions.v (where Foo is your project) and import
that everywhere you want it in.

I think that would be very nice indeed -- maybe generalized to allow
providing a list of default bases? (e.g. Set Default HintBase mybase,
core, arith)
(alternatively, if there was a way to merge databases / import hints
from one in another, it would be enough for the option to take one base;
but there isn't at the moment AFAIK)

[Jacques-Henri Jourdan]

I think it is generally not bad to put things in the core database, as
long as they are keyed with some local definition. That is, the head
symbol of the conclusion of the lemma should be one of yours, and made
opaque for eauto.

This way (modulo bugs in eauto), nobody should suffer from importing
your hints, since they only apply to goals that correspond to your library.

Post by Vadim Zaliva
One approach would be is scope-like. "Open HindDB" which could be nested.
Vadim
--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone]
On Wed, Nov 14, 2018 at 12:59 PM Jason -Zhong Sheng- Hu
This is a very interesting discussion, because core database is too
polluted whenever working with others' modules. The situation is
getting worse when different projects cross together and produce
weird interactions. 
I'm wondering if there's some plan to introduce modularity in hint
databases? It would be very helpful if hints can be grouped as
modules and can be opened, closed and injected from one database to
another.
Thanks,
Jason Hu
-------- Original message --------
Date: 11/14/18 15:10 (GMT-05:00)
Subject: Re: [Coq-Club] Moving away from putting hints in the core hintdb
Thanks for the answer!

Post by Gaëtan Gilbert
Maybe we could add an option "Set Default HintBase mybase", then you
could use regular option scoping.
ie either put "Set" at the top of every file or module you want it in,
or "Export Set" in FooOptions.v (where Foo is your project) and import
that everywhere you want it in.

I think that would be very nice indeed -- maybe generalized to allow
providing a list of default bases? (e.g. Set Default HintBase mybase,
core, arith)
(alternatively, if there was a way to merge databases / import hints
from one in another, it would be enough for the option to take one base;
but there isn't at the moment AFAIK)

[Soegtrop, Michael]

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-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of Armaël Guéneau
Sent: Wednesday, November 14, 2018 8:28 PM
To: coq-***@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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgeric

[Jim Fehrle]

Hi Michael,

 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.

Logs meaning the console output from Set Debug Auto/Set Debug Eauto?  By the branching factor, you just mean paying attention to the output (e.g. 1.2.3.1 is depth 4) and each digit counts the branches at it's level?

 the core hint database includes hints which can loop to the search depth limit on some goals.

How helpful would it be if auto/eauto detected and avoided looping?  Either by a) detecting that the proof state has already been seen in the current search (e.g. there is a tactic for a commutative property) and/or b) using a queue that ranks various proof states by a size metric and processing the smaller proof states first.  This might give better performance and allow for a higher depth limit.
Thanks,
Jim

count_rev_tree < Set Debug Eauto.

count_rev_tree < eauto.Debug: (* debug eauto: *)Debug: 1 depth=5Debug: 1.1 depth=4 simple apply f_equal_natDebug: 1.1.1 depth=3 simple apply f_equal2_natDebug: 1.2 depth=4 simple apply f_equal2_natDebug: 1.2.1 depth=4 simple apply @eq_reflDebug: 1.2.1.1 depth=3 simple apply f_equal2_natDebug: 1.2.2 depth=4 simple apply eq_add_S ; trivialDebug: 1.2.2.1 depth=3 simple apply f_equal2_natDebug: 1.2.3 depth=4 simple apply eq_sym ; trivialDebug: 1.2.3.1 depth=3 simple apply f_equal2_nat

From: "Soegtrop, Michael" <***@intel.com>
To: "coq-***@inria.fr" <coq-***@inria.fr>
Sent: Thursday, November 15, 2018 2:22 AM
Subject: RE: [Coq-Club] Moving away from putting hints in the core hintdb

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

[Soegtrop, Michael]

Dear Jim,

Logs meaning the console output from Set Debug Auto/Set Debug Eauto? By the branching factor, you just mean paying attention to the output (e.g. 1.2.3.1 is depth 4) and each digit counts the branches at it's level?

Yes, I do regular profiling runs with coqc running on the command line and output redirected to a file. I tend to generate statistics over the number of applictions/tactics tried vs. the final proof depth (I can provide a python script for this, if you are interested). Usually I can manage to keep this between 2 and 3 on average by proper hint database engineering, so that overall I have linear search time. This means the branching factor is in most cases one and only in some cases a small number. To make the log analysis easier I have in my eauto wrappers also a tactic which first prints the current goal.

How helpful would it be if auto/eauto detected and avoided looping? Either by a) detecting that the proof state has already been seen in the current search (e.g. there is a tactic for a commutative property) and/or b) using a queue that ranks various proof states by a size metric and processing the smaller proof states first. This might give better performance and allow for a higher depth limit.

I think you would in many cases still have exponential search time, because it usually takes 2..3 steps for a loop. So you would detect the loop only after 3 steps and it is not unlikely that in each step of the loop you can also do something else. But yes, it would be helpful to hash the proof state and detect that you have been here before for complicated cases. I have some tactics which do this manually to a certain extent (record the set of seen goals in a proof state variable). But I would first try to eliminate the loop by managing my hint databases and especially proper gating tactics and resort to hashing only in cases where it gets complicated otherwise.

I think what would really help is to build up some pattern matching based database which learns by “trial and error eauto proofs” which things make sense in which context. Best would likely be to couple eauto with a neural network. I have some idea on how to approach this, but didn’t have time to try it as yet. It might also be that something in the back of my mind is slightly scared about this. But I have some of our (Intel) neuromorphic chips in my drawer 


Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], 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