The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

Dear Coq users,

When trying to compile Coq trunk rev. 12704 I am getting the following error:

OCAMLDEP4 parsing/g_constr.ml4
Error: don't know what to do with pa_extend.cmo

A similar message with different .cmo files is printed after every
call to OCAMLDEP4. Eventually, I get the following error:

OCAMLOPT  parsing/egrammar.ml
make[1]: *** Pas de règle pour fabriquer la cible «
parsing/g_xml.ml4.ml.d », nécessaire pour « parsing/g_xml.cmx ».
Arrêt.

I am able to compile trunk rev. 12007, and configure works fine for
both versions. Its output is included below.

Any help is appreciated.

Evgeny Makarov

~/coq/trunk> ./configure -opt -local
You have GNU Make 3.81. Good!
You have Objective-Caml 3.10.1. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available.
pngtopnm was not found; documentation will not be available

  Coq top directory                 : /home/emakarov/coq/trunk
  Architecture                      : Linux
  Coq VM bytecode link flags        : -dllib -lcoqrun -dllpath
'/home/emakarov/coq/trunk'/kernel/byterun
  Coq tools bytecode link flags     :
  OS dependent libraries            : -cclib -lunix
  Objective-Caml/Camlp4 version     : 3.10.1
  Objective-Caml/Camlp4 binaries in : /usr/local/bin
  Objective-Caml library in         : /usr/local/lib/ocaml
  Camlp4 library in                 : +camlp5
  Native dynamic link support       : false
  Lablgtk2 library in               : +lablgtk2
  Documentation                     : None
  CoqIde                            : opt
  Web browser                       : firefox -remote
"OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                      : http://coq.inria.fr/