Hi Nela, There have been various problems over the years, but I get no problems with recent versions of HOL Light (downloaded since May 2014, including SVN version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11 running on Fedora 17.
Do you know the HOL Light SVN version (or otherwise, what date did you download)? And can you please check your OCaml and Camlp5 versions by executing the following from the same terminal window from which you are trying the HOL Light make?: ocaml -version camlp5 -v Mark. on 16/9/14 4:45 PM, Nela Cicmil <nela.cic...@dpag.ox.ac.uk> wrote: > 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 > > > ---------------------------------------------------------------------------- > -- > Want excitement? > Manually upgrade your production database. > When you want reliability, choose Perforce. > Perforce version control. Predictably reliable. > http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ Want excitement? Manually upgrade your production database. When you want reliability, choose Perforce Perforce version control. Predictably reliable. http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
