The Coq mailing list

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

Hi,

Compilation with camlp4 is broken in 8.4 and 8.4pl1. You should apply
revision 16122 from the v8.4 bug-fix branch [1] or use camlp5 instead
(even if Coq generally works with camlp4 as well as it does with
camlp5, strange things happen sometimes in the parser: in particular
the compilation of the reference manual might loop when using camlp4).

Hugo Herbelin

[1] 
https://gforge.inria.fr/scm/viewvc.php/branches/v8.4/scripts/coqmktop.ml?root=coq&r1=16015&r2=16122&pathrev=16122)

On Wed, Jan 16, 2013 at 09:12:04PM +0000, Gregory Malecha wrote:
>    Hello --
>    I have a fresh download of 8.4pl1 which I ran ./configure with no
>    arguments and then make, things go along great for a little while and 
> then
>    I get this error:
>    make[1]: Entering directory `/home/gmalecha/devel/coq/coq-8.4pl1'
>    CHECK revision
>    COQMKTOP -o bin/coqtop.byte
>    File "/tmp/coqmain4a488c.ml", line 1:
>    Error: Cannot find file q_coqast.cmo
>    make[1]: *** [bin/coqtop.byte] Error 2
>    make[1]: Leaving directory `/home/gmalecha/devel/coq/coq-8.4pl1'
>    make: *** [world] Error 2
>    Find does report that it exists:
>    $ find . -iname q_coqast.cmo
>    ./parsing/q_coqast.cmo
>    Any idea what is going wrong or how to fix it? I'm running ocaml 4.00.1
>    $ ocamlc -v
>    The OCaml compiler, version 4.00.1
>    Standard library directory: /usr/lib64/ocaml
>    Thanks.
>    --
>    gregory malecha
>    http://www.people.fas.harvard.edu/~gmalecha/