was hoping to use HETS to experiment with CASL and Isabelle as described on this page.
The easiest way to install HETS is under Ubuntu (even supports daily updates). However I am using openSUSE 12.2 (x86_64) so here is my attempt to install and run on an openSUSE system.
HETS can also be run as an online interactive service using a web browser, just link to here.
Installing HETS
Since I'm not using Ubuntu I used the java installer (Its only the installer that is java, not the program itself). Unfortunately the java installer only contains a old hets version 0.98 and this does not seem to be compatible with some of the Linux libraries so I then had to modify the installation as shown below.
Download hets java installer from here.
The file I downloaded is called: hets-0.98-installer-linux64.jar
From the command line type: java -jar hets-0.98-installer-linux64.jar
This brings up the java install screens: Click on 'Next' |
 |
This screen just contains general information. Click on 'Next' |
 |
Accept the terms of the licence (if you do). Click on 'Next' |
 |
On my system Tk 8.5 was already installed but uDrawGraph, isabelle and SPASS were not. The program detected that. Click on 'Next' |
 |
| Click on 'Next' to confirm uDrawGraph is to be installed. |  |
| Click on 'Next' to confirm isabelle is to be installed. |  |
| Click on 'Next' to confirm SPASS is to be installed. |  |
Enter directory where the programs are to be installed (I left it on the default). Click on 'Next' |
 |
Conformation of what is to be installed. Click on 'Next' |
 |
Conformation of details. Click on 'Next' |
 |
The installation happened here, when complete, click on 'Next' |
 |
Click on 'Done' The files have now been installed in the specified directory. |
 |
HETS should then be installed but if I try to run it I get the following error:
martin@linux-gye4:~/proofAssist/bin> ./hets Chapter3.casl /home/martin/proofAssist/lib/proofAssist/hets: error while loading shared libraries: libgmp.so.3: cannot open shared object file: No such file or directory
I seem to have libgmp.so.10 installed in /usr/lib64/ but HETS seems to be looking for libgmp.so.3.
I asked about this on the HETS mail list and Christian Maeder suggested I went to here download the hets-2013-03-26.bz2.
I unzipped this to a 'hets-2013-03-26' file and copied it
to replace Home/proofAssist/bin/hets
I then set the execute enable bit on the file.
Now the program appears to run:
martin@linux-gye4:~/proofAssist/bin> ./hets Chapter3.casl ### file name 'Chapter3.casl' does not match library name 'UserManual/Chapter3' Analyzing library UserManual/Chapter3 Analyzing spec UserManual/Chapter3#Strict_Partial_Order Analyzing spec UserManual/Chapter3#Total_Order Analyzing spec UserManual/Chapter3#Total_Order_With_MinMax Analyzing spec UserManual/Chapter3#Variant_Of_Total_Order_With_MinMax Analyzing spec UserManual/Chapter3#Partial_Order Analyzing spec UserManual/Chapter3#Partial_Order_1 Analyzing spec UserManual/Chapter3#Implies_Does_Not_Hold Analyzing spec UserManual/Chapter3#Monoid Analyzing spec UserManual/Chapter3#Generic_Monoid Analyzing spec UserManual/Chapter3#Non_Generic_Monoid Analyzing spec UserManual/Chapter3#Generic_Commutative_Monoid Analyzing spec UserManual/Chapter3#Generic_Commutative_Monoid_1 Analyzing spec UserManual/Chapter3#Container Analyzing spec UserManual/Chapter3#Marking_Container Analyzing spec UserManual/Chapter3#Generated_Container Analyzing spec UserManual/Chapter3#Generated_Container_Merge Analyzing spec UserManual/Chapter3#Generated_Set Analyzing spec UserManual/Chapter3#Natural Analyzing spec UserManual/Chapter3#Color Analyzing spec UserManual/Chapter3#Integer Analyzing spec UserManual/Chapter3#Natural_Order Analyzing spec UserManual/Chapter3#Natural_Arithmetic Analyzing spec UserManual/Chapter3#Integer_Arithmetic Analyzing spec UserManual/Chapter3#Integer_Arithmetic_Order Analyzing spec UserManual/Chapter3#List Analyzing spec UserManual/Chapter3#Set Analyzing spec UserManual/Chapter3#Transitive_Closure Analyzing spec UserManual/Chapter3#Natural_With_Bound Analyzing spec UserManual/Chapter3#Set_Choose Analyzing spec UserManual/Chapter3#Set_Generated Analyzing spec UserManual/Chapter3#Set_Union Analyzing spec UserManual/Chapter3#Set_Union_1 Analyzing spec UserManual/Chapter3#UnNatural
I now need to read the user manual to find out how to use it.
