This README belongs to a Hets release (and does not apply to

sources directly obtained via cvs).

The subject of this release is a binary "hets" that is able to analyse

heterogeneous and in particular CASL specifications.

The sources need to be compiled with ghc Glasgow Haskell Compiler

(www.haskell.org/ghc).

The output of hets, if the input is successfully accepted, can be

displayed by "daVinci".

daVinci is maintained by b-novative and b-novative holds all rights.

This release may be accompanied with free binary releases of daVinci

Version 2.1, but daVinci 2.1 is no longer supported or maintained!

However, you are encouraged to obtain the latest version of daVinci

Presenter (currently 3.0.5) from http://www.b-novative.com that is

free for academic purposes.

Linux: the linux binary release of daVinci 2.1 relies on the old

shlibs5 that must be installed on your system (if ./daVinci cannot be

found/executed, then shlibs5 are missing)

Solaris: the solaris binary release of daVinci 2.1 should work without

problems

Macintosh (Darwin): there is no release of daVinci for Macintosh, but

b-novative may have one in the mean time

For best quality, get the latest version of daVinci from b-novative.

For hets to find daVinci, the environment variables DAVINCIHOME and

UNIDAVINCI must be set to the installation directory of daVinci and to

the actual executable, respectively.

export DAVINCIHOME=<path>/daVinci_V2.1

export UNIDAVINCI=<path>/daVinci_V2.1/daVinci

A typical call of hets is then: <path>/hets -g Basic/Numbers.casl

If you need to rebuild the hets binary follow the instructions in INSTALL

(This README belongs a to release created by "make release", in case

that you obtained the HetCATS sources as CVS tree)

The heterogeneous tool set (Hets) is mainly maintained by

Christian Maeder (maeder@tzi.de) and Till Mossakowski

(till@tzi.de). The mailing list is hets@tzi.de.

Files in the Tools/Hets/src directory, with maintainers:

--------------------------------------------------------

LICENCE.txt Licence information (english) (Till Mossakowski)

LIZENZ.txt Licence information (german) (Till Mossakowski)

INSTALL Installation and compilation instructions (???)

Makefile GNU-Makefile to compile sources (Klaus Luettich)

README This file (Till Mossakowski)

hets.hs Top-level Haskell module for hets (Till Mossakowski)

version_nr Current version (Till Mossakowski)

ATC/ Conversion from and to ATerms (Klaus Luettich)

CASL/ Instance of Logic: CASL (Till Mossakowski/Christian Maeder)

Common/ Modules common to all logics

Common/ATerm/ Conversion from and to ATerms (Klaus Luettich)

Common/Lib/ Third-party modules

Common/Lib/Parsec/ Parsec combinator parser (Christian Maeder)

Common/PrettyPrint.hs pretty printing (Klaus Luettich)

pretty printing should get an own directory

Comorphisms/ Comorphisms of the logic graph (Till Mossakowski)

CspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)

doc/ Documentation (Till Mossakowski)

docs/ Haddock generated documentation (Klaus Luettich)

ghc/ Some ghc-specific stuff (Christian Maeder)

GUI/ GUI for displaying development graphs (Till Mossakowski/Jorina Gerken)

HasCASL/ Instance of Logic: HasCASL (Christian Maeder)

Haskell/ Instance of Logic: Haskell (Christian Maeder)

Haskell/Hatchet/ Static anaylsis of Haskell

Haskell/Language/ Haskell syntax in Haskell

haterm-1.0 ATerm library (Klaus Luettich)

hetcats/ Command line interface (Klaus Luettich)

hugs/ Some hugs-specific stuff (Christian Maeder)

Isabelle/ Instance of Logic: Isabelle

Logic/ Infrastructure for logic independence (Till Mossakowski)

Modal/ Instance of Logic: ModalCASL (Till Mossakowski)

Proofs/ Heterogeneous proof engine (Till Mossakowski)

Static/ Heterogeneous development graphs and static analysis (Till Mossakowski/Maciek Makowski)

Syntax/ Heterogeneous syntax and parsing (Christian Maeder)

ToHaskell/ translation to Haskell (Christian Maeder)

should be moved to Comorpisms

utils/ Utilities

utils/DrIFT-src/ DrIFT (for polytpyic conversion functions) (Klaus Luettich)

utils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)

utils/inlineAxioms parse inline axioms (Till Mossakowski)