The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Tue, Feb 16, 2010 at 03:04:43PM +0100, Damien Pous wrote:
> Hi,
> 
> Did some of you encountered the following situation, and did you find
> a satisfactory solution ?
> 
> 1. We prove a rather involved theorem, by heavily relying on
> FSets/FMaps (we need sets of lists of nats, sets/maps of positive, and
> sets/maps of sets of positive). However, the theorem is not about
> finite sets at all. At the end, we get a module M, that contains the
> theorem.
> 
> 2. Since we want to use this theorem, we "Require M".
> 
> 3. Now all proofs involving typeclasses become *very* slow : the hint
> databases now contain all lemmas about the various finite sets and
> finite maps we used to prove our theorem... (notably the
> typeclass_instance database grows from 110 lines to 1500 lines, and
> simple setoid_rewrites are ten times slower than before).
> 
> We will never use these hints/instances: they are specific to M's
> implementation.
> We managed to hide the hints we added by ourselves using the section
> mechanism, but we cannot hide FSets/FMaps hints.
> 
> Maybe hints should not survive to the end of modules by default, and
> be activated only when the modules are exported ?
> 
> Below is some concrete code, to be tested with the current version of
> our ATBR library
> (ad: http://sardes.inrialpes.fr/~braibant/atbr/atbr-1.1.tar.gz)
> 
> Damien and Thomas
> 

Hi, thanks for the report. I'll try to solve this issue by making
these hints local to the FSets modules, and export them only in
seperate, optional modules. I'll let you know when this is done.
I'll also check with Elie Soubiran and Matthieu Sozeau whether
we adequately avoid now registering several instances for the
same constant if it has several names for the module system.

Best,

Pierre Letouzey