HOL-4 kananaskis8

インストールスクリプトを書きました．プラットフォームは
http://d.hatena.ne.jp/ehito/20130214/1360813508
と同じです．コンパイルには４〜５時間必要です．

export CAS=/home/knoppix/CAS
cd ~
sudo mkdir ./CAS
cd $CAS
wget --no-check-certificate https://github.com/Munksgaard/mosml/archive/master.zip
unzip -x master
cd ./mosml-master/src
make world
sudo make install
cd $CAS
wget http://sourceforge.net/projects/hol/files/hol/kananaskis-8/kananaskis-8.tar.gz
tar zxvf kananaskis-8.tar.gz
cd /home/knoppix/CAS/hol-kananaskis-8
mosml < tools/smart-configure.sml
./bin/build
echo "export PATH=$PATH:/home/knoppix/CAS/hol-kananaskis-8/bin"  > /home/knoppix/.bashrc

あとは，source ~/.bashrc としてパスを通せば


のように使えます．
なお，HOL-4は，MS-Windows上でも動きます（コンパイルには半日ほど）が，毎回の /bin/hol.bat による起動（ライブラリーのロードなど），quit(); による終了（メモリーの解放）にいずれも１０分程度要し，特に終了中にはPCへの入力ができませんが，quit(); ではなく，ctrl+c で終了させ直ぐ再起動すればフリーズしません．また
http://hol.sourceforge.net/faq.html#Parsing
にある対策だけでは，helpなどでバイナリーを呼ぶとユニコードの論理記号が文字化けします．