The Coq mailing list

[Karen Sargsyan <karsar AT ibms.sinica.edu.tw>]

Asking Ubuntu people was a joke, as I'll compile it faster. Anyway, you 
are right and I use long-term stable Ubuntu.
I've never tried to compare how fast are developments for Coq and 
Ubuntu. It's something good to know, before
complaining. Thank you for sharing.

Karen

On 4/22/14, 9:08 PM, Adam Chlipala wrote:
> If you're using the latest long-term stable Ubuntu as of last month 
> (12.10), then it makes sense that they would include Coq 8.3, since 
> 8.4 was unfortunately released only two months before that Ubuntu 
> version, probably not allowing enough time for proper packaging & 
> testing to be included in a stable release.  Coq is still really 
> research software and changes at a pace greater than the one that 
> mainstream Linux distros are effectively assuming.
>
> On 04/22/2014 09:04 AM, Karen Sargsyan wrote:
> > Thank you. I see that it's better to ask Ubuntu people why they keep 
> > such an old version in their repository:)
> > Or just compile it myself at the end. Anyway, if someone knows what 
> > exactly happened between two versions that causes
> > such behavior, I'm curious to know.
> >
> > Karen
> >
> > On 4/22/14, 8:51 PM, Adam Chlipala wrote:
> > > Perhaps the important missing piece of information here is that 8.3 
> > > and 8.4 are effectively different "major versions" of Coq, in terms 
> > > of the extent of reorganization that is common when adding 0.1 or 
> > > more to a Coq version number. It won't surprise me if you're just 
> > > seeing the result of a big standard-library refactoring.  Coq 8.3 
> > > was first released in 2010, and it's rather out of date today, 
> > > regardless of the patch level.
> > >
> > > On 04/22/2014 08:44 AM, Karen Sargsyan wrote:
> > > > If I do the following sequence on Ubuntu with Coq 8.3pl4 (ocaml 
> > > > 3.12.1):
> > > >
> > > > Coq < Require Export ZArith.
> > > > Coq < Definition any: Z:= Z.div 2 3.
> > > >
> > > > then result is: "Error: The reference Z.div was not found in the 
> > > > current environment"
> > > >
> > > > On Mac OS X with 8.4pl2 OCaml 4.00.1 it defines "any".
> > > >
> > > > So apparently there is some incompatibility between 8.3pl4 and 
> > > > 8.4pl2 in case of ZArith (something knows).
> > > > Is it so, or it's a bug in Ubuntu Coq package?