This README belongs to a Hets release (and does not apply to
sources directly obtained via cvs).

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

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.

Overview of source modules, with maintainers:
For more details, see the Haddock documentation in docs/
(after generation with "make doc") 
--------------------------------------------------------

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/Martin Kuehl)
CoCASL/                     Instance of Logic: CoCASL (Till Mossakowski)
CoL/                        Instance of Logic: COL (Till Mossakowski)
Common/                     Modules common to all logics
Common/ATerm/                 Conversion from and to ATerms (Christian Maeder)
Common/Lib/                   Set, Map, Graph, Rel modules (Christian Maeder)
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/                        ghc-specific "coerce" (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/              parsing, printing, analysis of Haskell
hetcats/                    Command line interface (Klaus Luettich)
hugs/                       hugs-specific "coerce" (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/Jorina Gerken)
Static/                     Heterogeneous development graphs and static analysis  (Till Mossakowski/Maciek Makowski)
Syntax/                     Heterogeneous syntax and parsing (Till Mossakowski, Christian Maeder)
ToHaskell/                  translation to Haskell (Christian Maeder)
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)