The Heterogeneous Tool Set
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
ATC
Adl
CASL
CASL_DL
CMDL
COL
CSL
CSMOF
CoCASL
Common
CommonLogic
Comorphisms
ConstraintCASL
CspCASL
CspCASLProver
DFOL
DMU
Driver
ExtModal
Fpl
Framework
FreeCAD
GMP
GUI
HasCASL
Haskell
HolLight
Hybrid
Interfaces
Isabelle
LF
Logic
MMT
Maude
Modal
Modifications
OMDoc
OWL2
Omega
PGIP
PLpatt
Persistence
Proofs
Propositional
QBF
QVTR
RDF
RelationalScheme
SoftFOL
Static
Syntax
THF
TPTP
Taxonomy
Temporal
ToHaskell
TopHybrid
VSE
atermlib
debian
doc
magic
mini
pretty
test
utils
.gitignore
.travis.yml
ATC.hs
CASL.hs
CASL_DL.hs
CMDL.hs
COL.hs
CoCASL.hs
Common.hs
Comorphisms.hs
CspCASL.hs
CspCASLProver.hs
Driver.hs
ExtModal.hs
Framework.hs
GUI.hs
HasCASL.hs
Haskell.hs
Hets-Haddock-Prologue.txt
Hets.cabal
Hybrid.hs
Isabelle.hs
LICENSE.txt
LIZENZ.txt
Logic.hs
MMT.hs
Makefile
Modal.hs
OMDoc.hs
OWL2.hs
Proofs.hs
Propositional.hs
README
README.md
RelationalScheme.hs
Scratch.hs
SoftFOL.hs
Static.hs
Syntax.hs
Taxonomy.hs
TopHybrid.hs
_parameters
hets.hs
ideas
sample-ghci-script
stack.yaml
todo
var.mk

README.md

Hets (The heterogeneous tool set)

Hets is a parsing, static analysis and proof management tool incorporating various provers and different specification languages, thus providing a tool for heterogeneous specifications. Logic translations are first-class citizens.

Supported languages

The following provers have been connected to Hets:

The structuring constructs of the heterogeneous specification language are those of the OMG-standardised Distributed Ontology, Model and Specification Language (DOL), extending those of CASL. However, Hets can also read other structuring constructs, like those of Haskell, Maude or OWL. All these are mapped to so-called development graphs and processed with a proof calculus for heterogeneous development graphs that allows to decompose global proof obligations into local ones (during this, Hets also needs to compute colimits of theories over the involved logics).

Hets is based on a graph of logics and logic translations. The overall architecture is depicted below. Adding new logics and logic translations to Hets can be done with moderate effort by adding some Haskell code to the Hets source. With the Latin project, this becomes much easier: logics (and in the near future also logic translations) can be declaratively specified in LF.

Architecture of the heterogeneous tool set Hets

Using Hets

You can try out Hets using the Web-based interface

The best way to use hets is under Ubuntu. Possibly run this OS in a virtual box.

A compressed (1.2G, uncompressed 4.2G) virtual box image can be downloaded from here. username/password is ubuntu/reverse.

Installing Hets under Ubuntu

The basic system

sudo apt-get install software-properties-common
sudo dpkg --add-architecture i386			# not needed for hets-server
sudo apt-add-repository ppa:hets/hets
sudo apt-get update
sudo apt-get install hets-desktop
  • for the full system including all provers etc., use hets-desktop-all instead of hets-desktop
  • for using Hets as a server providing a RESTful interface, use hets-server or hets-server-all. This is a smaller version without GUI dependencies. Note that also hets-desktop can be used as as server.

Hets development

For Hets development additionally type in

sudo apt-add-repository -s "deb http://ppa.launchpad.net/hets/hets/ubuntu xenial main"
sudo apt-get update
sudo apt-get build-dep hets-desktop

Replace 'xenial' with the Ubuntu version that you use. The Hets sources should be obtained from the git repository (see the end of this page).

Installing Hets under Archlinux

We provide the AUR-packages hets-desktop-bin and hets-server-bin to install 64 bit binaries of Hets/Hets-server. If you would like to compile Hets yourself, you can install one of the AUR-packages hets-desktop and hets-server.

Installing Hets under OS X/macOS (10.9 (Mavericks) and greater)

  • Install Homebrew: See https://brew.sh
  • Install Java: brew cask install java
  • Install the Hets-Repository to Homebrew: brew tap spechub/hets
  • Only for Hets-Desktop, install X11: brew cask install xquartz
  • Either install hets-desktop: brew install spechub/hets/hets-desktop
  • Or install hets-server: brew install spechub/hets/hets-server

This installs Hets along with all its dependencies. Some of the dependencies are optional, but recommended, especially the provers. You can install Hets without these by adding a flag --without-* where * is one of these recommended dependencies. For instance, you can run brew install spechub/hets/hets-desktop --without-leo2 to skip the installation of Leo2. For a list of these flags, run brew info hets-desktop.

Hets binaries

(these are usually not needed but may replace the binaries from above)

How to use a hets binary?

Just download the binary and put it somewhere in the $PATH.

  • Our current linux binaries also rely on gtk-2 and glade-2 libraries for more and better menus. Thus you may need to install additional libraries. Use ldd (or "otools -L hets" on Macs) to see which libraries are missing.)
  • For displaying development graphs (with the -g option), you need to install uDraw(Graph) (formerly known as daVinci) that relies on Tcl/Tk (version 8.4 or 8.5) (which probably has been already installed on your computer anyway). Make sure uDrawGraph and wish are in your $PATH.

Download the CASL libraries and set $HETS_LIB to the folder containing these.

Quickstart

Hets is called with

hets filename

or

hets -g filename

For entering the command line mode, just call

hets -I

For a short description of the options, call

hets --help

Restful Interface

See RESTful Interface

User Documentation

A good starting point is the Hets user guide and the Hets user guide for Common Logic users. Furthermore two vidoes showing a heterogeneous proof are available:

For a formal introduction to hets see the introductory paper The Heterogeneous Tool Set by Till Mossakowski, Christian Maeder, Klaus Lüttich and Stefan Wölfl. For more in-depth information about Hets see the thesis Heterogeneous specification and the heterogeneous tool set by Till Mossakowski.

For questions related to hets there is a mailing list.

Emacs Mode for CASL specifications

To support writing CASL specifications we have an emacs mode

Including specifications in LaTeX documents

With the option "-o pp.tex" hets can produce nice LaTeX output from your specifictions that can be embedded in your publications using the hetcasl.sty style file.

Development

A good starting point is the code documentation for Hets - the Heterogeneous Tool Set.

Since Hets is rather large and complex we recommend following the interactive session in Debugging and Testing Hets to get familiar with the central datastructures of Hets.

The formal background and the general structure of Hets is described in chapter 7 of Heterogeneous specification and the heterogeneous tool set.

Haskell

Hets is written in Haskell, and is compiled using GHC using a couple of language extensions. Among the Haskell books and tutorials we recommend Real World Haskell. The language definition covers the Haskell98 standard which we are supposed to stick to in most cases. Make sure that you are familiar with at least the most common library functions of the Prelude. For searching or looking up any library functions you may also try Hoogle.

Also look into programming guidelines and things to avoid in Haskell.

Dependencies

Dependencies can be installed as specified in Hets Development

Contributing changes

Before committing haskell source files you may check compliance to the programming guidelines:

  • Use scan which can be installed by cabal install scan.
  • The comments in your haskell sources should not cause haddock to fail. After make (for re-compiling changed sources) make doc will call haddock.
  • Also check your source with hlint which you may install by cabal install hlint.

Also have a look at the current Release Notes, Debugging and Testing Hets,Code Review and Branching.

If you want to participate in the Hets development feel free to tell us via our mailing list for Hets developers. This mailing list can also be read via http://news.gmane.org/gmane.comp.lang.hets.devel.

If you wish to make larger changes we generally recommend forking this repository. You can however request access to this repository if you plan on contributing regularly.

Build Hets using Stack

  • Get the git repository and its submodules
    git clone https://github.com/spechub/Hets.git
    git submodule update --init --recursive
    
  • Install Stack (use the generic Linux option if you are on Ubuntu).
  • Install build- and GUI-dependencies
    • Ubuntu:
      sudo apt install libglib2.0-dev libcairo2-dev libpango1.0-dev libgtk2.0-dev libglade2-dev libncurses-dev
      sudo apt install postgresql postgresql-server-dev-9.5 mysql-server libmysqlclient-dev
      
    • macOS:
      brew cask install xquartz
      brew install binutils glib libglade cairo gtk fontconfig freetype gettext spechub/hets/udrawgraph
      
  • Setup Stack for Hets (this needs to be done only once after every time the stack.yaml has changed):
    stack setup
    make restack
    
    When you invoke make for the first time, this will give you warnings about not having found a compiler ("No compiler found, expected minor version match with ghc-..."). Don't let this discourage you - it's normal. Running make stack will take care of it and install the compiler. Running make restack does the same thing, as make stack, but needs to be run every time the dependencies (stack.yaml) change.
  • Build Hets with one of the following:
      make
      make hets
      make hets_server
    
    This uses Stack to build the Hets[-Server] binary. During this process, the specified version of GHC is installed in the user directory, all dependencies are built and finally, the Hets[-Server] binary is compiled.
  • If you want to clean the extra-dependencies of Stack that are put into the Hets working directory, run
    make clean_stack
    

Troubleshooting & Useful Tools

Hints for contributors switching from svn to git

License

The Hets source code is licensed under the GPLv2 or higher