sudo aptitude install build-essential ledit wget
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.
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
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
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).
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
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`;;
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