coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Incorrect camlp5o config for OS X .dmg

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Incorrect camlp5o config for OS X .dmg
Date: Mon, 14 Sep 2015 10:16:08 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wi0-f170.google.com
Ironport-phdr: 9a23:FN5GNBV7dJ8DA8Q5zoRvedtjz23V8LGtZVwlr6E/grcLSJyIuqrYZheBt8tkgFKBZ4jH8fUM07OQ6PC8HzZcqsze+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8GVOVkD3mX1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDtxNUHwjE4QyyZZDjvyLn/r540TWGNMjeSLkoRT2nqaBxR0m72288Kzcl/TSP2YRLh6VBrUf5qg==

Hi Eddy,

this is indeed a bug in the way we build the coqide packages, could you please report it on https://coq.inria.fr/bugs/ ?

Best,

-- Matthieu

On Sat, Sep 12, 2015 at 2:03 AM Eddy Westbrook <westbrook AT kestrel.edu> wrote:

All,

When I download the OS X disk image CoqIDE_8.5beta2.dmg from the website and run coqtop -config, I get output that contains a number of references to the directory /Users/mat/gtk, which does not exist on my system. Additionally, the CAMLP4O variable is set to a path containing /Volumes/Macintosh HD/Users/mat/gtk, which is even worse because the Makefiles generated by coq_makefile seem to try to run the command “/Volumes/Macintosh”, parsing the space as a separator between command and arguments.

Note that the COQLIB variable does seem to get set correctly, so the problem mainly comes when I try to compile OCaml plugins.

Could someone please take a look at this?

Thanks,
-Eddy

[Coq-Club] Incorrect camlp5o config for OS X .dmg, Eddy Westbrook, 09/12/2015
- Re: [Coq-Club] Incorrect camlp5o config for OS X .dmg, Matthieu Sozeau, 09/14/2015