HOL Light with check pointing

　HOL LightはOcamlのToplevel Loop上のプログラムですから，Ocamlが動くならOSは問いませんが，周辺プログラムとの連携という観点に立つなら何といってもUnixです．
　それはMaximaやPARI/GPを呼ぶmlファイル内のシステムコマンドによるものだけではなく，一般的なHOL Lightユーザーにとって必須の機能であるcheck pointing http://checkpointing.org プログラムが実装されているのはUnixのみだからです．
　中でもHOL Lightとの相性が良いのが，ckpt http://www.cs.wisc.edu/~zandy/ckpt/ です．これをインストールしておくと，HOL Light附属のMakefileにより，例えば，make holとすればコアバイナリーが生成され，引数として，hol.multivariate， hol.sosa，hol.card，hol.complexを用いると，ロードにそれなりの時間を要する各パッケージをロードした状態のバイナリーが生成されます．各バイナリーをまとめて生成，インストールするには，make all，make installが便利です（ただし，BINDIR=${HOME}/bin は，BINDIR=/usr/local/bin に書き換えておくのが普通でしょう）．また，セッションの途中でバイナリー化するには
self_destruct "startup_bannerの次に表示させたいcomment";;
とすれば，カレントディレクトリにREDUCE likeな名前 hol.snapshot で実行ファイルが生成されます．