Glad to hear Nix might be working out for you. It is a very nice package
management idea.
I actually meant to refer you to the HOL Light Workbench (see
http://www.mail-archive.com/hol-info@lists.sourceforge.net/msg01558.html)
which you might have missed since it was several clicks away from the link
I originally sent.
On Wed, Sep 17, 2014 at 1:14 PM, Nela Cicmil <nela.cic...@dpag.ox.ac.uk>
wrote:
> 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
>
------------------------------------------------------------------------------
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
