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

[Nela C. <nel...@dp...>]

Dear HOL Light users, 

Would anyone be able to please advise me on how to install HOL Light on my Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.

My trouble is that I can't seem to get compatible versions of Ocaml, camlp5 and HOL Light installed on my system, mainly because the Ocaml version that comes with OPAM, v 4.01.0, seems to be too recent to run with the slighter older camlp5 versions compatible with HOL Light. 

Has anyone recently installed HOL Light on a Mac, and has advice on which versions of Ocaml and camlp5 to install, and which procedure to use to install them? In particular, is it possible to install an older version of Ocaml, e.g. v 3.12, using OPAM?

The specific issues I've encountered are detailed below. Any advice would be much appreciated.

Thank you, 

Best wishes, 
Nela                
----
Nela Cicmil, D.Phil
Dept. Physiology, Anatomy & Genetics,
University of Oxford
----

After various attempts to install Ocaml on the Mac, I installed (using homebrew) the latest version of OPAM, which comes with Ocaml version 4.01.0. On basic testing at the terminal, Ocaml seemed to be working fine. I then installed camlp5 version 6.11, using ./configure --transitional mode, and that seemed to be running fine as well. When I then attempted to install HOL Light, using the svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light procedure, and got the following error on "make":

File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
       but an expression was expected of type
         ('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2


- On reading various previous posts, it seemed that the latest versions of camlp5 could be at fault. I attempted to install older versions of camlp5, version 6.02.0 and 5.15, but I got the following error on ./configure --transitional: 

Sorry: the compatibility with ocaml version "4.01.0"
is not yet implemented. Please report.
Information: directory ocaml_stuff/4.01.0 is missing.
Configuration failed.

- With campl5 version 6.06 it's the following error (I'm not sure what the preprocessor is here):

>> Fatal error: OCaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[2]: *** [versdep.cmo] Error 2
make[1]: *** [core] Error 2
make: *** [world.opt] Error 2

- So then I attempted to install an earlier version of Ocaml, version 3.12.1, in the hope that it would be compatible with the earlier versions of camlp5. This did not seem possible with OPAM so I downloaded the original source distribution tar.gz from http://ocaml.org/releases/3.12.1.html. I believe my system has the necessary dependencies in the form of Xcode 5.11, gcc and gnumake running. However, the "make world" installation command exits on the following error: 

make coldstart
cd byterun; make all
gcc -DCAML_NAME_SPACE -O -fno-defer-pop -no-cpp-precomp -Wall -D_FILE_OFFSET_BITS=64 -D_REENTRANT    -c -o interp.o interp.c
clang: error: unknown argument: '-fno-defer-pop' [-Wunused-command-line-argument-hard-error-in-future]
clang: note: this will be a hard error (cannot be downgraded to a warning) in the future
make[2]: *** [interp.o] Error 1
make[1]: *** [coldstart] Error 2
make: *** [world] Error 2