Hi Nela,
I've written about this before, you might find the following message (and
the links inside it) useful:
http://www.mail-archive.com/hol-info@lists.sourceforge.net/msg02358.html
For HOL Light developers, I would like to issue a request: would it be so
difficult to remove the dependence on Camlp5, since it is now no longer
supported by Ocaml, and use ppx or something else (ideally nothing!)
instead? Keeping HOL Light up to date with OCaml development looks to be
quite a task.
Some people (including myself) are working (very slowly) on building a
version of HOL Light written in CakeML and automatically translating the
existing substantial developments in HOL Light over, so maybe this problem
will one day go away. (And maybe be replaced by new ones.)
Cheers,
Ramana
On Tue, Sep 16, 2014 at 3:31 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
