coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Eddy Westbrook <westbrook AT kestrel.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Incorrect camlp5o config for OS X .dmg
Date: Fri, 11 Sep 2015 17:03:26 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=westbrook AT kestrel.edu; spf=None smtp.mailfrom=westbrook AT kestrel.edu; spf=None smtp.helo=postmaster AT mail.kestrel.edu
Ironport-phdr: 9a23:2FolEh+npJRP7P9uRHKM819IXTAuvvDOBiVQ1KB90OkcTK2v8tzYMVDF4r011RmSDdmdsq4MotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EleqKsRsb7tIee6aObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+CNJ/vkl6sRoUKPgfq1+Q6YLIi4hNjUY6MH6/SbOVheF/HwbUS1CjRdTHwLf6xb5dpT8qTfgu+471SWHa56lBYsoUCivuv84ACTjjz0KYmY0

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