Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

2014-09-17 Thread Marco Maggesi
Hi Nela, I use the Nix package manager (http://nixos.org/nix/) and it works well for me. I use Nix both on Max and on Linux. It is nice because it makes the installation of HOL Light completely independent from the versions of ocaml, camlp5 (or any other software indeed) installed in your

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

2014-09-17 Thread Nela Cicmil
Thanks very much to Marco, Mark and Ramana for your replies. I may have made some progress using Nix: @ Marco: Following your suggestion I installed Nix and HOL Light with the following commands on terminal (after creating a /nix directory under my user account): $ bash (curl

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

2014-09-17 Thread Mark Adams
Nela, These versions should definitely work together. Just realised - what you presumably did is first try the HOL Light 'make' using other versions of OCaml or Camlp5. So what you needed to do was first do make clean before doing make I would be very surprised if this doesn't work.

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

2014-09-17 Thread Marco Maggesi
2014-09-17 14:14 GMT+02:00 Nela Cicmil nela.cic...@dpag.ox.ac.uk: and all seemed to complete without errors. My question is, if HOL Light is now installed on my machine, what's the best way to run it? ​Sorry, I forgot to say. As you already found yourself, you have to use the command