The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

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.

Le 14/11/2018 à 22:24, Vadim Zaliva a écrit :
> One approach would be is scope-like. "Open HindDB" which could be nested.
> 
> Vadim
> 
> --
> CMU ECE Ph.D. candidate
> Mobile/Signal/WhatsApp: +1(510)220-1060
> 
> 
> 
> On Wed, Nov 14, 2018 at 12:59 PM Jason -Zhong Sheng- Hu
> <fdhzs2010 AT hotmail.com
>  
> <mailto:fdhzs2010 AT hotmail.com>>
>  wrote:
> 
>     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 
> <armael.gueneau AT ens-lyon.fr
>     
> <mailto:armael.gueneau AT ens-lyon.fr>>
>     Date: 11/14/18 15:10 (GMT-05:00)
>     To: 
> coq-club AT inria.fr
>  
> <mailto:coq-club AT inria.fr>,
>  Gaëtan Gilbert
>     
> <gaetan.gilbert AT skyskimmer.net
>  
> <mailto:gaetan.gilbert AT skyskimmer.net>>
>     Subject: Re: [Coq-Club] Moving away from putting hints in the core
>     hintdb
> 
>     Thanks for the answer!
> 
>     > 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)
>

Attachment: signature.asc
Description: OpenPGP digital signature