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 https://nixos.org/nix/install) $ source /Users/nc/.nix-profile/etc/profile.d/nix.sh $ nix-channel --add http://nixos.org/channels/nixpkgs-unstable $ nix-channel --update $ nix-env -i hol_light 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? The standard way through ocaml doesn't seem to be able to find the hol.ml file… should I fix some path, or is there another way to run the program when installed via nix? $ ocaml OCaml version 4.01.0 # #use "hol.ml";; Cannot find file hol.ml. (NB. If I just type "hol_light" onto the command line, it spews a seemingly never-ending list of warnings and errors… not sure why.) @ Mark: I used the svn download command only this week so probably it has the most recent version of HOL Light. On svn download, I get the output "Checked out revision 198", and the CHANGES document inside the hol_light directory is dated 9th Sept 2014. Here are my ocaml and camlp5 versions: hol_light nc$ ocaml -version The OCaml toplevel, version 4.01.0 hol_light nc$ camlp5 -v Camlp5 version 6.11 (ocaml 4.01.0) @ Ramana: I'm looking into the pa_j*.ml files, but it's not clear to me how to write one to work with the ocaml version 4.01.0/camlp5 v 6.11 combo. Thanks! Best wishes, Nela ---- Nela Cicmil, D.Phil Dept. Physiology, Anatomy & Genetics, University of Oxford ________________________________________ From: marco.magg...@gmail.com [marco.magg...@gmail.com] on behalf of Marco Maggesi [magg...@math.unifi.it] Sent: 17 September 2014 08:15 To: Mark Adams Cc: Nela Cicmil; hol-info@lists.sourceforge.net Subject: Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5? 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 machine. If you want to try, here is what you have to do: 1. Install Nix. Follow the instructions from the nix manual (http://nixos.org/nix/manual). Basically you have to type the following four commands in a terminal: $ bash <(curl https://nixos.org/nix/install) source /usr/local/etc/profile.d/nix.sh nix-channel --add http://nixos.org/channels/nixpkgs-unstable nix-channel --update 2 . Then you can install HOL Light with a single command (no need to install OCaml or Camlp5) nix-env -i hol_light For more serious work you probably need to use checkpointing which is available only on Linux. For this I use a NixOS (http://nixos.org) VirtualBox appliance. Do not esitate to ask for more details if you are interested. Best, Marco 2014-09-17 5:50 GMT+02:00 "Mark Adams" <m...@proof-technologies.com<mailto:m...@proof-technologies.com>>: 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<mailto: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<http://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<mailto: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<mailto: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
