README.installer

This README belongs to the installer for the Hets
"The Heterogeneous Tool  Set"

Information not contained here can be found in the Hets user guide
(doc/UserGuide.pdf) or on the Hets web page (www.dfki.de/sks/hets).

The installer supplies an executable "hets" that is able to analyse
heterogeneous and in particular CASL specifications together with many
additional tools needed for proving.

This Installer will put all tools and a library of
specification (Hets-lib) into a single directory (`Hets' in this
example) with the following layout:

  Hets/bin          ---  contains the hets startup script and links to
                      	 some tools; you may put this directory into
                      	 your PATH environment variable

  Hets/doc          ---  useful documentation on hets and the LaTeX
  		    	 style file for processing of pp.tex files
  		    	 generated by hets

  Hets/Hets-lib     ---  the library of CASL specifications; also obtained
  		      	 from http://www.cofi.info/Libraries

  Hets/lib          ---  all the installed tools needed to run hets

  Hets/src          ---  if you request to install the hets sources, they
  		      	 reside here

  Hets/Uninstaller  ---  use the uninstaller with
  		    	 "java -jar Hets/Uninstaller/uninstaller.jar"
			 if you really want to uninstall hets (-;

A typical call of hets within the directory Hets/Hets-lib/ is:
   ../bin/hets -v2 -g Calculi/Space/RCCVerification.het

After "Edit" -> "Proofs" -> "Automatic" you may try to prove the red
nodes using SPASS or Isabelle. Isabelle is only needed for the single
red node that is not supported by other provers. The used Isabelle
example proof is stored in the file
RCCVerification_RCC_FO_in_MetricSpace_T.thy

If you install the emacs casl-mode you can also run hets from within
emacs on a specification file with C-c C-r or C-c C-g (to get the
graphical interface).

MacOS users: in Hets/bin/hets you may uncomment or modify the line
containing "Aquamacs" in order to use Isabelle with a proper emacs
window.

Solaris users: hets uses the "patch" program before calling
Isabelle. Under Solaris this must be the "gpatch" program, so you may
somehow make sure (by a link or an alias) that "patch" executes
"gpatch".

x86_64 users: We only create 32bit binaries and rely on gmp and
readline libraries. These must be installed as 32bit libraries,
i.e. rpm package gmp-32bit-4.1.4.

The heterogeneous tool set (Hets) is mainly maintained by
Christian Maeder (Christian.Maeder@dfki.de) and
Till Mossakowski(Till.Mossakowski@dfki.de).
The mailing list is hets-devel@informatik.uni-bremen.de.