The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi list,

I have the following issue that is driving me nuts. I have two Ubuntu boxes with practically the same setup. I have a plugin for Coq 8.5 beta 2. However, I can compile it in one machine but not on the other. In the machine where it works, I have OCaml installed in the system (as in /usr/bin), while on the other is in .opam.  The error in the second machine is:

File "src/myfile.ml4", line 92, characters 13-14:
Parse error: [global] or [entry] expected after uppercase identifier (in
  [gextend_body])
File "src/myfile.ml4", line 1:
Error: Error while running external preprocessor

That line is:
GEXTEND Pcoq.Gram
GLOBAL: myproof_instr;
  myproof_instr :
    [[ c=Pcoq.Constr.operconstr ; "." -> MyInstr.my_constr c ]];
END

When compiling Coq, the ./configure -local script outputs the text below, where XXX is replaced by specific locations for OCaml: /usr/bin (or lib) for one machine, and .opam in the other.

Any ideas?

Thanks!

Beta

---
You have GNU Make 3.81. Good!
You have OCaml 4.02.3. Good!
You have Camlp5 6.14. Good!
You have native-code compilation. Good!
No such directory '/home/beta/.opam/4.02.3/lib/ocaml/lablgtk2' (in OCaml library).
LablGtk2 not found:
=> no CoqIde will be built.

  Architecture                : Linux
  Coq VM bytecode link flags  : -dllib -lcoqrun -dllpath /home/beta/coq/coq8.5b2/coq-8.5beta2/kernel/byterun
  Other bytecode link flags   :
  OS dependent libraries      : -cclib -lunix
  OCaml version               : 4.02.3
  OCaml binaries in           : XXX
  OCaml library in            : XXX
  Camlp5 version              : 6.14
  Camlp5 binaries in          : /home/beta/.opam/4.02.3/bin
  Camlp5 library in           : /home/beta/.opam/4.02.3/lib/camlp5
  Native dynamic link support : true
  CoqIde                      : no
  Documentation               : None
  Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                : http://coq.inria.fr/