cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3
> -d'.' | cut -c1-6` = "6.11" ; \
>the
mlp4 -where` pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \
fi
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
but an expres
Dear hol-info,
I'd just like to reinforce Marco's suggestion of using nix as a package
manager. In my opinion, it is packaging done right (although there are
various things that can be improved, and the package description language
can be a bit off-putting until you get used to it).
I use nix on
amlp4 -where` pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I `camlp5 -where` pa_j.ml; \
fi
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
but an expression w
2014-09-17 14:14 GMT+02:00 Nela Cicmil :
> 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?
​Sorry, I forgot to say. As you already found yourself, you have to use
the command
hol_light
which starts ocaml
_
> 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
__
> 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 Ocam
rom: 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 Nel
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 machin
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 other
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
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
12 matches
Mail list logo
