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>:
> 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
>
------------------------------------------------------------------------------
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
