The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

I also saw that recently. Maybye you can try downgrading you camlp5 by
one version (5-5.09)...

Sorry for not being more sure about this.

Benjamin

Le 12 janv. 09 à 13:19, Yves Bertot a écrit :

> Ashish Darbari wrote:
> > Hi Fellows,
> >
> > I tried building Coq-8.2 and it fails. Any clue?
> > I've a Mac OSX Darwin, ocaml-3.10.2 and camlp5-5.10
> > both successfully installed from sources.
> >
> > Thanks
> > Ashish
> >
> > Prayag:/usr/local/coq-8.2beta4 root# make world
> > *****************************************************
> > *****************************************************
> > ****************** Entering stage1 ******************
> > *****************************************************
> > *****************************************************
> > make -f Makefile.stage1 "stage1"
> > make[1]: Entering directory `/usr/local/coq-8.2beta4'
> > OCAMLC4   lib/compat.ml4
> > File "lib/compat.ml4", line 17, characters 11-25:
> > Unbound type constructor Stdpp.location
> > make[1]: *** [lib/compat.cmo] Error 2
> > make[1]: Leaving directory `/usr/local/coq-8.2beta4'
> > make: *** [stage1] Error 2
> I remember having a similar problem, but I don't remember how I  
> fixed it.  I believe that somehow, your compiler is using camlp4  
> instead of camlp5.  Can you send us (or me) the
> text produced by the "configure" command in the coq root directory.
>
> The following command should not fail:
>
> ls $(ocamlc -where)/camlp5/stdpp.*
>
> should succeed and find three files (.cmi .cmx .mli)
>
> Yves
>
>
> --------------------------------------------------------
> 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