#37100: coq 8.4 +coqide ----------------------+----------------------- Reporter: joerg@… | Owner: reilles@… Type: defect | Status: new Priority: Normal | Milestone: Component: ports | Version: 2.1.2 Resolution: | Keywords: coqide Port: coq | ----------------------+----------------------- Comment (by 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 -- Ticket URL: <https://trac.macports.org/ticket/37100#comment:2> MacPorts <http://www.macports.org/> Ports system for Mac OS