PVSのこと（12） - ATPとCASのこと

今更ですが，PVS (Allegro Versions)，Yices1，NASA PVS Library，Hypatheon 各最新版のインストールスクリプトです．

sudo apt-get -y install sqlite3

echo "export PVS_LIBRARY_PATH=~/CAS/pvs6/nasalib" >> ~/.bashrc
source ~/.bashrc
mkdir ~/CAS
cd ~/CAS

ここで
http://yices.csl.sri.com/cgi-bin/yices-newlicense.cgi?file=yices-1.0.39-x86_64-pc-linux-gnu-static-gmp.tar.gz
を開いて，I accept をクリック，~/CAS に保存して

tar zxvf ./yices-1.0.38-x86_64-pc-linux-gnu-static-gmp.tar.gz
mkdir ./pvs6
cd ./pvs6

ここで
http://pvs.csl.sri.com/cgi-bin/downloadlic.cgi?file=pvs-6.0-ix86_64-Linux-allegro.tgz
を開いて，I accept をクリック，~/CAS/pvs6 に保存して

tar zxvf ./pvs-6.0-ix86_64-Linux-allegro.tgz
./bin/relocate
sudo ln -s ~/CAS/pvs6/pvs /usr/local/bin/pvs
wget http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/nasalib-6.0.6-full.tgz
tar xvfz ./nasalib-6.0.6-full.tgz
cd ./nasalib/
wget http://shemesh.larc.nasa.gov/people/bld/ftp/hyp-nasalib-6.0.4.sdb.gz
cd ..
pvs

ここで emacs が起動するので

M-x shell

とし

cd ./nasalib/Hypatheon-1.1
./build/quick_install

の後，Hypatheon が起動し，プロンプトが戻ったら

sed -i "s/;(s/(s/" ~/.pvsemacs

とすれば完了です．

なお，RedHat 系の Fedora には次のようなパッケージがあります．
http://rpm.pbone.net/index.php3/stat/4/idpl/21599251/dir/fedora_19/com/pvs-sbcl-6.0-3.fc19.x86_64.rpm.html