The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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> 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>

Date: 11/14/18 15:10 (GMT-05:00)

To: coq-club AT inria.fr, Gaëtan Gilbert <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)