The Coq mailing list

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

Hi, 

Indeed, the FSet library has evolved quite a bit between 8.1 and 8.2,
and this leads to a few incompatibilities, like this Set/Type issue,
and some others (e.g. eq_dec required in OrderedType). Sorry for the
inconvenience, I really only do such incompatible changes when it's
clear to me that the long-term gain in usability will outbalance the
cost of transition.

Concerning Compcert, let me add that there already exist compcert
versions compatible with either coq 8.2 or coq trunk :

 svn://scm.gforge.inria.fr/svn/coq-contribs/trunk/Rocq/CompCert

or

 svn://scm.gforge.inria.fr/svn/coq-contribs/branches/v8.2/Rocq/CompCert

By looking at the changelog of these repositories, you can easily get
a list of my changes with respect to the "official" compcert.

Best regards,

Pierre Letouzey


On Mon, Feb 09, 2009 at 02:08:55PM +0100, Stéphane Lescuyer wrote:
> Hi Cedric,
> 
> OrderedType.t and FSetInterface.S.t used to be of type Set. This
> prevented (for no reason) developers to build finite sets whose
> elements were in Type and not in Set. For that reason they have both
> been changed to Type which is a very wishable update indeed, but leads
> to some incompatibilities with earlier developments. It should be
> fairly straightforward to fix your files, by changing the appropriate
> occurrences of Set to Type.
> 
> Cheers,
> Stéphane
> 
> On Mon, Feb 9, 2009 at 1:32 PM, Cedric Auger 
>Â <Cedric.Auger AT lri.fr>
>  wrote:
> > Hello, I tried to recompile compcert using the trunk version 11850, and
> > found:
> >
> > COQC lib/Lattice.v
> > File "/users/demons/cauger/Documents/compcert-1.3/lib/Lattice.v",
> > line 325, characters 0-10:
> > Error: Signature components for label t do not match.
> > make: *** [lib/Lattice.vo] Erreur 1
> >
> > I tried to understand what happened:
> > it seems that in contrary to
> > http://coq.inria.fr/library/Coq.FSets.FSetInterface.html ;,
> > S.t is no longer of type Set but of type Type.
> >
> > I think, that there has been a non wishable correction in some update; am 
> > I
> > wrong?
> > Is it an old bug that has been corrected since?
> >
> > --
> > Cédric AUGER
> >
> > Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >         http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >