The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,                                                                           
                                

A new patch level version of 8.2 named 8.2pl3 fixing a couple of
important bugs has just been released. In particular, it compiles with
camlp5 6.02.3 (and probably 6.02.2 too). It is available at
http://coq.inria.fr/distrib/V8.2pl3/files/.

Actually, a patch level version of 8.3 named 8.3pl3 has been released
too (pre-compiled packages to arrive soon).

Hugo
   
On Wed, Dec 21, 2011 at 03:06:09PM -0500, Catalin Hritcu wrote:
> On Mon, Nov 7, 2011 at 7:21 AM, Daniel de Rauglaudre
>Â <daniel.de_rauglaudre AT inria.fr>
>  wrote:
> > Hi,
> >
> > On Mon, Nov 07, 2011 at 11:14:44AM +0100, Gyesik Lee wrote:
> >
> >> OCAMLC4   parsing/pcoq.ml4
> >> File "parsing/pcoq.ml4", line 749, characters 8-300:
> >> Error: The constructor Gramext.Slist1sep expects 3 argument(s),
> >>        but is applied here to 2 argument(s)
> >
> > Perhaps a problem of version of Camlp5. Which version do you have ?
> > (type "camlp5 -v"). Perhaps its version is not compatible with this
> > version of Coq, because too old or too new.
> >
> Sorry to bring back a not so recent thread, but this information
> should be useful for other people having trouble compiling Coq 8.2pl2
> with new versions of Camlp5.
> 
> I had the same problem on Ubuntu 11.10 with Ocaml version 3.12.0 and
> Camlp5 version 6.02.2. There is, however, a patch by Stéphane Glondu
> in the Debian repository targeted exactly at this problem:
> 
> You can get it by clicking the "raw" link on this page:
> wget 
> http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq.git;a=blob_plain;f=debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch;hb=6b3bd571d555c4db91ab210da9a302b2f2181e23
> 
> And apply it in your coq-8.2pl2 dir like this:
> patch -p1 < debian_patches_0003-Fix-build-with-camlp5-6.02.1.patch
> 
> This did the job for me, hope it works for others as well.
> 
> Regards,
> Catalin
>