Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

[Tom R. <tom...@go...>]

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 top of ubuntu. It works well, but I also have a list of
packages I install  using apt. These tend to be packages such as virtualbox
which somehow needs a tight integration with the underlying system. I also
confess to using an apt-supplied latex installation because this seems
non-trivial to get working properly in nix.

T

On 17 September 2014 14:34, Marco Maggesi <mar...@gm...> wrote:

> 2014-09-17 14:14 GMT+02:00 Nela Cicmil <nel...@dp...>:
>
>> 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 and loads hol.ml automatically.
>
> You have to wait a few minutes while the full system loads (people use
> checkpointing precisely to avoid this step).  Don't care about the long
> list of messages and warnings, all should be OK.  At the end you get
> something like:
>
> File
> "/nix/store/0cgxqn0x9nz0i6l5ysnf9ak0rqkh0v7y-hol_light-189/lib/hol_light/
> help.ml", line 116, characters 25-57:
>
> Warning 3: deprecated feature: operator (&); you should use (&&) instead
>
> Camlp5 parsing version 6.11
>
>
> #
>
> then you can type our commands: e.g.
>
> # ARITH_RULE `1 + 1 = 2`;;
> val it : thm =
>
> |- 1 + 1 = 2
>
>
> Small suggestion: since the ocaml toplevel do not have line editing
> features, you may want to use rlwrap:
>
>
> nix-env -i rlwrap
>
>
> then invoke hol as
>
>
> rlwrap hol_light
>
>
> Hope it helps and keep asking if all this is not clear,
>
> Marco
>
>
> ------------------------------------------------------------------------------
> 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...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>