Queste note spiegano come installare HOL Light su di un sistama Linux. Questi appunti sono stati scritti durante un’installazione di marzo 2010 usando Ubuntu 9.10 (Karmic Koala). Con poche varianti dovrebbero adattarsi facilmente ad altri sistemi, escluso quello che riguarda la parte di "checkpointing" che dipende in maniera pesante dalla versione del software adottata.

Avvertimento: Queste note sono state scritte in maniera distratta e caotica per uso puramente personale. Sono certamente inesatte, incomplete e potenzialmente pericolose.

2. Configurazione iniziale

Installare i pacchetti indispensabili per il resto.

sudo aptitude install build-essential ledit wget

Creare una directory "software".

mkdir software
cd software

Aggiungere le seguenti righe a .bashrc (gedit ~/.bashrc).

export PATH=~/software/bin:$PATH
export MANPATH=~/software/man:$MANPATH

Caricare la nuova impostazione.

source ~/.bashrc

3. Installare OCaml

Scaricare, compilare, installare OCaml.

cd ~/software
wget http://caml.inria.fr/pub/distrib/ocaml-3.09/ocaml-3.09.3.tar.bz2
tar xjf ocaml-3.09.3.tar.bz2
cd ocaml-3.09.3
./configure -prefix ~/software/
make world.opt
make install

4. Installare HOL Light

Scaricare, compilare HOL Light.

cd ~/software
wget http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.tgz
tar xzf hol_light_100110.tgz
cd hol_light
make

Adesso HOL Light è installato e lo si può avviare nel modo seguente:

ledit ocaml
#use "hol.ml";;

Tuttavia, è consigliabile usare un software di "checkpointing" per non dover aspettare ogni volta che il sistema venga ricaricato. (Questo è particolarmente importante se si intende lavorare con alcune librerie particolarmente pesanti come l’analisi reale di più variabili).

5. Installare DMTCP

Questo metodo funziona soltanto su Linux e soltanto su certe distribuzioni. Ad esempio non funziona su Ubuntu 9.04.

cd ~/software
wget http://downloads.sourceforge.net/project/dmtcp/dmtcp/1.1.4/dmtcp_1.1.4.tar.gz?use_mirror=garr
tar xzf ../dmtcp_1.1.4.tar.gz
cd dmtcp_1.1.4
./configure --prefix=$HOME/software
make
make install

6. Checkpointing di HOL Light con dmtcp

Aggiungere le seguenti righe al file ~/software/hol_light/make.ml

(* ------------------------------------------------------------------------- *)
(* Destructive checkpoint using DMTCP.                                       *)
(* ------------------------------------------------------------------------- *)

let dmtcp_checkpoint bannerstring =
  let longer_banner = startup_banner ^ " with DMTCP" in
  let complete_banner =
    if bannerstring = "" then longer_banner
    else longer_banner^"\n        "^bannerstring in
  (Gc.compact();
   loadt "Examples/update_database.ml";
   print_newline ();
   Unix.sleep 1;
   try ignore(Unix.system ("dmtcp_command -bc -k")) with _ -> ();
   Format.print_string complete_banner;
   Format.print_newline(); Format.print_newline());;

Checkpoint del nucleo di HOL Light (senza nessuna libreria addizionale).

cd ~/software/hol_light
dmtcp_coordinator --background
dmtcp_checkpoint ocaml
#use "make.ml";;
dmtcp_checkpoint "";;
dmtcp_command -q
cd ~/software/bin
ln -s ../hol_light/dmtcp_restart_script.sh hol_light

Provare se tutto funziona.

ledit hol_light
ARITH_RULE `1+1=2`;;

7. Checkpointing di HOL Light con analisi reale e complessa precaricata

A seconda del modello del vostro computer il caricamento dei queste librerie potrebbe richiedere alcune ore.

cd ~/software/hol_light
dmtcp_coordinator --background
dmtcp_checkpoint ocaml
#use "make.ml";;
loadt "Multivariate/make.ml";;
loadt "Multivariate/make_complex.ml";;
dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;
dmtcp_command -q
cd ~/software/bin
ln -s ../hol_light/dmtcp_restart_script.sh hol_light