HOL Light入門その１ - ATPとCASのこと

新年度ということで，従来の内容に加え，これから HOL Light を始める方に向けた記事も書いていきます．

プラットフォームは，Linux（MS-Windowsの方は http://d.hatena.ne.jp/ehito/20110203/1296713729 を参考にしてください）とします．

まず，ターミナルを開き，適当なフォルダーに移動して

sudo apt-get update
sudo apt-get install -y --force-yes camlp5

と入力すると，HOL Light の実行基板の OCamle がインストールされます．

続いて，HOL Light の名を天下に轟かせたSOS proverが利用する外部プログラムcsdpを

sudo wget http://www.coin-or.org/download/binary/Csdp/csdp6.0.1linuxp4.tgz
tar zxvf csdp6.0.1linuxp4.tgz
sudo cp ./csdp6.0.1linuxp4/bin/csdp /usr/bin/

のようにインストールします．

最後に

svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
cd ./hol_light
make

と入力すると，hol_light というフォルダーが作られ，最新版がネットからコピー，必要なファイルのリネームが行われ，インストール完了です．