README revision dce6436c6ad1863558c14e15b0ff2d5a0bdd45b4
This README belongs to a "The heterogeneous tool set" (Hets) source
release created by "make release" from the original svn repository.
(for svn see http://subversion.tigris.org/)
The original svn sources can be obtained by:
svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk Hets
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 subject of this source release is to create a binary "hets" that
is able to analyse heterogeneous and in particular CASL
specifications.
The sources need to be compiled using ghc Glasgow Haskell Compiler
(www.haskell.org/ghc) version 6.12.1, 6.12.3 or 7.0.2!
Version 6.10.x does not support the wai-extra-0.2.4.2 package for hets as
server. Version 6.12.2 is broken for gtk, see
http://hackage.haskell.org/trac/ghc/ticket/4038. Version 7.0.1 loops for
programatica, see http://hackage.haskell.org/trac/ghc/ticket/4527.
Haskell as a logic is an optional part of Hets via "Programatica"
(http://programatica.cs.pdx.edu/).
Beside output written to the console (stdout) or to files, hets can
display graphs using "uDraw(Graph)" www.informatik.uni-bremen.de/uDrawGraph.
The binary uDrawGraph should be in your PATH.
Some dialogs depend on Gtk and Glade that require a couple of further
libraries. Mac users are expected to install gtk2 from macports
A typical call of hets is then: hets -g Basic/Numbers.casl
Example specifications can be found under:
https://svn-agbkb.informatik.uni-bremen.de/Hets-lib/trunk
For proving users may set HETS_ISABELLE, if "isabelle emacs" is not the right
call for their system. Isabelle versions 2009 and 2011 are supported.
Further environment variables for provers are:
PELLET_PATH
HETS_OWL_TOOLS
HETS_APROVE
If you need to build the hets binary follow the instructions in
INSTALL, alternatively try to get a binary or a complete installer from:
www.dfki.de/sks/hets/installation_e.htm
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.