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.

Documentation for HETS.

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'

hets install

This screen just contains general information.

Click on 'Next'

hets install

Accept the terms of the licence (if you do).

Click on 'Next'

hets install

On my system Tk 8.5 was already installed but uDrawGraph, isabelle and SPASS were not. The program detected that.

Click on 'Next'

hets install
Click on 'Next' to confirm uDrawGraph is to be installed. hets install
Click on 'Next' to confirm isabelle is to be installed. hets install
Click on 'Next' to confirm SPASS is to be installed. hets install

Enter directory where the programs are to be installed (I left it on the default).

Click on 'Next'

hets install

Conformation of what is to be installed.

Click on 'Next'

hets install

Conformation of details.

Click on 'Next'

hets install

The installation happened here, when complete, click on 'Next'

hets install

Click on 'Done'

The files have now been installed in the specified directory.

hets install

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.

Running HETS

metadata block
see also:


Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Executable UML - Covers compiler issues but no code
cover Executable UML - concentrates on patterns

cover Fast Track UML 2.0 - useful for people who know some UML but are upgrading to 2.0

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.