coq 8.4 +coqide

[joerg@…]

There seems to be a problem installing coq +coqide. The compile breaks due to:

:info:build Error: /opt/local/lib/ocaml/site-lib/lablgtk2/gdk.cmi
:info:build is not a compiled interface

Probably this is due to a mix of ocaml3 and ocaml4. Installing coq +coqide results in both versions of ocaml being installed.

Any help is appreciated.

Greetings, Joerg

[jmroot (Joshua Root)]

Please remember to Cc the maintainer.

[benedikt.huber@…]

I can confirm this bug. Probably this is because the lablgtk2 port is built with ocaml (version 4), but coq still depends on caml3. I guess the best thing is to drop the dependency on caml3; this should be possible now [1].

I managed to build coq +coqide using a local Portfile: I switched to ocaml and camlp5, and applied a simple patch to two ML files in the IDE (this is necessary, as the definition of Gdk.Tags.modifier changed in newer versions of lablgtk2). So far, it seems the IDE works well.

Kind Regards, Benedikt

[1] ​http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/8977

[ecronin (Eric Cronin)]

Has duplicate: #37487

[pmetzger (Perry E. Metzger)]

So far as I know, Coq hasn't depended on ocaml3 in a very long time. If someone is still having trouble, please let me know.

[pmetzger (Perry E. Metzger)]

Okay, this seems to be an instance of a more general problem, which I am tracking in #56376