The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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