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 <marco.magg...@gmail.com> wrote:
> 2014-09-17 14:14 GMT+02:00 Nela Cicmil <nela.cic...@dpag.ox.ac.uk>:
>
>> 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-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Slashdot TV. Video for Nerds. Stuff that Matters.
http://pubads.g.doubleclick.net/gampad/clk?id=160591471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
