Documentation

=============

Information not contained in this file can usually be found in the

Hets user guide (doc/UserGuide.pdf), on the Hets web page http://hets.eu/

or within the source itself.

Installation

============

Unless you know what you are doing you should always install the prepared

system packages for your OS, instead of compiling it by yourself:

Ubuntu:

# add the hets PPA site to your system unless already done

apt-add-repository ppa:hets/hets

apt-add-repository -s \

"deb http://ppa.launchpad.net/hets/hets/ubuntu xenial main"

# update the system's package catalog and install hets incl. dependencies

apt-get update

apt-get install hets-desktop

# to update your installation to a recent version do from time to time:

apt-get update

apt-get upgrade [hets-desktop]

Solaris 11+:

# add the package publisher info of the Uni Magedeburg to your system

# if not already done (see "pkg publisher" output)

pkg set-publisher --add-origin http://pkg.cs.ovgu.de/lnf lnf

# install hets incl. dependencies

pkg install hets-desktop

# to update your installation to a recent version do from time to time:

pkg update [hets-desktop]

To get optional TeX/PDF support, you also need to install the related pdflatex

packages (Ubuntu: texlive-latex-base, texlive-latex-extra, texlive-pictures,

texlive-fonts-recommended; Solaris 11+: tl-latex, tl-fonts, tl-utils).

Adding packages to the system usually requires additional privileges.

So sudo, pfexec or similar tools might be needed to be able to execute the

commands mentioned above successfully.

In non-desktop environments like servers, where no GUI is needed or hets is

running as a service, you may prefer to install the package 'hets-server'

instead. This one gets compiled without GTK+/Glade/TclTk support and thus

reduces the number of dependencies and required ressources noteworthy.

For your convenience there are also the hets-server-all and hets-desktop-all

packages: these are meta packages, which bundle hets-server and hets-desktop

with other hets related tools (e.g. misc. provers) repectively.

All mentioned packages can be installed side-by-side. The GUI version gets

usually started using the hets(1) command, a server instance can be started

using the hets-server(1) command.

Building from source

====================

hets sources can be obtained using the following command:

git clone https://github.com/spechub/Hets

For compilation we use the Glasgow Haskell Compiler "ghc" version 7.6.x and

above as well as Java for some helper tools. So you need to install these tools

as well as all haskell modules required by hets.

Having a look at utils/installHetsPkgs.sh as well as var.mk may help to find

out, what is missing on your system. On debianized systems the following

command may automatically install all dependencies:

DISTRO=`lsb_release -cs`

apt-add-repository \

-s "deb http://ppa.launchpad.net/hets/hets/ubuntu ${DISTRO} main"

apt-get update

apt-get build-dep hets-src

For Solaris 11+ have a look at http://pkg.cs.ovgu.de/lnf/en/catalog.shtml or

the output of e.g. "pkg list -a 'library/haskell/*'".

For anything else have a look at the file 'debian/control' - watch out for

'Build-Depends:'.

To build the un-optimized versions of hets and the hets server, use:

make all

To build the optimized versions incl. everything else needed for our debian

packages, use:

make build

This is basically the same as 'make hets-opt hets_server-opt docs'.

Omitting the suffix '-opt' from a target creates the un-optimized versions of

the related binary. For more details study the Makefile (GNU style, so on

Solaris use 'gmake' instead of 'make').

NOTE that since version 0.99.10 programatica support is disabled by default.

If you want programatica support you need to extract the sources first into

programatica/tools (this folder should than contain the Setup.hs file). One

may try 'make get-programatica' as an alternative - it tries to fetch the

source[s] defined in var.mk and extract them to the right place. On Ubuntu you

should also install the package 'libghc-programatica-dev'. To compile

without programatica support again, just rename or delete ./programatica/

and do a 'make distclean' before building the new binaries. 'make realclean'

is almost the same, but it leaves the derived aka generated sources untouched

and thus may cause problems. For more information wrt. programatica see

http://programatica.cs.pdx.edu/.

On debian based system one may even use the following or similar command, to

create the all *.deb packages out of the box in the parent directory of Hets:

export DEB_BUILD_ARCH=1

fakeroot make binary

For more details consult the Makefile. The resulting packages can be installed

as usual using something like 'dpkg -i ../hets-*.deb'. But make sure, you have

read and understood the 'Package-Versioning:' section below first!

On other systems, when the desired targets were made, you may install the

binary/docs into your own local directory by setting the PREFIX environment

variable to a corresponding value first and calling the appropriate target

(default is /usr). E.g.:

PREFIX=/home/foo/bar/hets make install

Instead of 'install' one may use the targets 'install-common', 'install-hets'

and 'install-hets_server' as well. Installing to a system directory like /usr

or /local/usr is strongly discouraged. Only Distro conform packages should be

installed there (and can thus can be removed in a clean and easy way)!

To install to a virtual root, one may set the environment variable DESTDIR to

the desired directory. Per default it is unset and thus equivalent to / .

Last but not least one may set the environment variable DEB_BUILD_ARCH to a

non-null value (as dpkg-buildpackage automatically does). In this case the

PREFIX gets effectively prefixed packagewise by another one, which makes

packageing easier and uniform across different OS.

NOTES:

One should NEVER make _any_ target as user 'root' or as a user with

additional privileges, which allow one to overwrite/delete system files!

When you want to create debian binary packages, use the fakeroot variant

shown above instead.

On MacOSX building the GUI supporting binaries may not work because of missing

GTK2/Glade and Tcl/Tk support.

Testing the build

=================

To run all available tests against the hets binary, simply type:

make check

It is recommended to have 'spass' and 'darwin' installed to avoid skipping

related tests.

Running Hets

============

Examples for testing can be obtained from

Example specifications can be found under:

If you have installed hets using the packaging system of your OS distribution,

it should already be installed (package name hets-libs or something like that).

Hets assumes that it has a copy in ../lib/hets/hets-lib relative to the bin/

directory with the hets/het-server script or the HETS_LIB is set to the folder,

which contains it.

Try out e.g. "hets -g Basic/Numbers.casl" to see if the graphical interface

pops up. If this does not work, maybe "uDrawGraph" (Version 3.1.1) from

http://www.informatik.uni-bremen.de/uDrawGraph is not properly installed. Make

sure "uDrawGraph" can be found in your PATH.

hets and het-server usually installed in the bin/ folder are shell script

wrappers around the corresponding binaries in lib/hets/, which just set certain

environment variables to more or less meaningful values, if not yet done and

needed. So have a look at it, if you need to know where hets is looking for

its libraries and helpers by default.

Prover related environment variables are:

PELLET_PATH

HETS_OWL_TOOLS

HETS_APROVE

HETS_ISABELLE_LIB

In addition, proving users may set HETS_ISABELLE, if "isabelle emacs" is

not the right call for their system. Isabelle version 2014 is supported.

Another typical call is 'hets -v2 -g -A Calculi/Space/RCCVerification.het'.

You may then 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

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).

Note that hets uses the "patch" program before calling Isabelle. It assumes,

that this is the GNU version of it. So especially on Solaris 11+ make sure,

that the 'gnu-patch' package is installed.

Misc

====

For convenience you may use 'make archive' to export the HEAD of your _local_

hets repository to an xz compressed tar archive (see git-archive(1) for more

information). HEAD refers usually to the last commited version of your current

branch (see "git branch"). Such an archive is e.g. needed for uploading a

source package to an Ubuntu Personal Package Archive (PPA). For this in

addition some minor things get pre-compiled/build, minimal git infos exported

to related files, redundant or unneeded data get deleted and programatica gets

bundled as is, because Ubuntu PPAs do not allow to download required

pre-requisites on-the-fly. But remember, the Ubuntu PPA is really picky about

archive names, so for each release one should choose a different filename,

otherwise be prepared for getting it rejected. Therefore you may set the

environment variable ARC_NAME to get out of the box you need, e.g.:

ARC_NAME=/tmp/foobar-1.2.3.tar.xz make archive

If there is already an archive with the same name, it will be overwritten

unconditionally!

The make targets 'clean', 'build', 'build-arch', 'build-indep' as well as

'binary', 'binary-arch' and 'binary-indep' are reserved in the sense of

https://www.debian.org/doc/debian-policy/ch-source.html#s-debianrules

and basically do, what the document says they should do.

Package-Versioning: A.B.C[.D.E]-n.m.r[.c]*

==========================================

Actually for each intended package publication on the PPA, the related commit

should be either propperly tagged OR `Driver/Version.hs` should be updated using

a number tripple with no leading zero[s] (see semantic versioning). For now it

is a twin pack only and thus we always add a '.1' and get "A.B.1" as our first

part (in debian terms the "upstream_version").

The optional .D.E part is used for unreleased versions/current builds of

the master branch. For D the numbers 0..5 are reserved for us (hets maintainer),

and might be used to express e.g. nightly, alpha, beta, RC, or FCS builts.

All other numbers can be used as needed by people/organizations/etc., which

build their own hets packages. This way they are always able to let their own

packages supersede packages built by hets developers/PPA without violating the

version semantics and still get next releases (A.B.C+1) w/o having to do

anything. On [new] releases we set .D.E back to .0.0 and thus gets ommitted

(more than 3 numbers: trailing zero pairs get deleted).

The second part (in debian terms the "debian_revision") is made of the string

n.m.r[.c] whereby n denotes number of pkg build modification count wrt. the

upstream_version. With each new upstream_version it starts again with 1 and

gets increased, if the source didn't change, but the way, how the package gets

build/structured. m.r is the LSB_RELEASE of the intended OS.

The last optional part [.c]* is used (simply incremented by 1 on demand), if

neither source nor pkg build procedure has been changed, but a new version is

needed to be able to overwrite old stuff, e.g. if the PPA goes mad again.

So e.g. to be able to overwrite the current installed hets packages with your

own version without getting into trouble, and getting this in turn automatically

replaced on e.g. 'apt-get update; apt-get upgrade' when a new version arrived,

one should just set FULL_DEBVERS to the same of the latest or installed package,

append a '.1' and increment it on demand. If it is not set, make deduces it from

the running system.

We use neither the debian epoch nonsense, nor lsb release names or other

questionable stuff - just A.B.C-n.m.r[.c]* and none of them zero padded!

If you have any problems, please ask via our mailing list

hets-devel@informatik.uni-bremen.de or file an issue on

https://github.com/spechub/Hets/issues/.

The heterogeneous tool set (Hets) is mainly maintained by

Christian Maeder (Christian.Maeder@dfki.de) and

Till Mossakowski (mossakow@iws.cs.uni-magdeburg.de).

# 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

* general-purpose logics: [Propositional](http://en.wikipedia.org/wiki/Propositional_calculus), [QBF](http://en.wikipedia.org/wiki/QBF), [TPTP](http://www.tptp.org/)/SoftFOL, [CASL](http://www.informatik.uni-bremen.de/cofi/index.php/CASL) (FOL), [HasCASL](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HasCASL/) (HOL)

* logical frameworks: [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/), [LF](http://en.wikipedia.org/wiki/LF_%28logical_framework%29), DFOL

* modeling languages: [Meta-Object Facility (MOF)](https://en.wikipedia.org/wiki/Meta-Object_Facility), [Query/View/Transformation (QVT)](https://en.wikipedia.org/wiki/QVT)

* ontologies and constraint languages: [OWL](http://www.w3.org/TR/owl2-overview/), [CommonLogic](http://cl.tamu.edu/), [RelScheme](http://en.wikipedia.org/wiki/Database_schema), ConstraintCASL

* reactive systems: CspCASL, [CoCASL](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/CoCASL/), ModalCASL, [Maude](http://maude.cs.uiuc.edu/)

* programming languages: [Haskell](http://www.haskell.org/), [VSE](http://www.dfki.de/vse/systems/vse/)

* logics of specific tools: Reduce, DMU ([CATIA](http://en.wikipedia.org/wiki/CATIA))

### The following provers have been connected to Hets:

* [minisat](http://minisat.se/) and [zChaff](http://www.princeton.edu/~chaff/zchaff.html), which are SAT solvers,

* [SPASS](http://www.spass-prover.org/), [Vampire](http://en.wikipedia.org/wiki/Vampire_(theorem_prover)), [Darwin](http://combination.cs.uiowa.edu/Darwin/), [Hyper](http://userpages.uni-koblenz.de/~bpelzer/hyper/) and MathServe, which are automatic first-order theorem provers,

* [Pellet](http://clarkparsia.com/pellet/) and [Fact++](http://owl.man.ac.uk/factplusplus/), description logic tableau provers,

* [Leo-II](http://page.mi.fu-berlin.de/cbenzmueller/leo/) and [Satallax](http://www.ps.uni-saarland.de/~cebrown/satallax/), automated higher-order provers,

* [Isabelle](http://www.cl.cam.ac.uk/Research/HVG/Isabelle/), an interactive higher-order theorem prover,

* [CSPCASL-prover](http://dx.doi.org/10.1016/j.entcs.2009.08.018), an Isabelle-based prover for CspCASL,

* [VSE](http://www.dfki.de/vse/systems/vse/), an interactive prover for dynamic logic.

The structuring constructs of the heterogeneous specification language are those of the [OMG](http://www.omg.org)-standardised [Distributed Ontology, Model and Specification Language (DOL)](http://dol-omg.org), extending those of [CASL](http://www.informatik.uni-bremen.de/cofi/index.php/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](http://en.wikipedia.org/wiki/Limit_%28category_theory%29#Colimits_2) 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](https://trac.omdoc.org/LATIN/) project, this becomes much easier: logics (and in the near future also logic translations) can be declaratively specified in [LF](http://twelf.plparty.org/wiki/Bibliography_of_LF).


## Using Hets

You can try out Hets using the [Web-based interface](http://rest.hets.eu/)

#### 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](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/vbox-x86-linux). username/password is ubuntu/reverse.

### Installing Hets under Ubuntu

#### The basic system

```

sudo apt-get install software-properties-common

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`](https://aur.archlinux.org/packages/hets-desktop-bin/) and [`hets-server-bin`](https://aur.archlinux.org/packages/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`](https://aur.archlinux.org/packages/hets-desktop/) and [`hets-server`](https://aur.archlinux.org/packages/hets-server/).

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

* Install Homebrew: See [https://brew.sh](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)

* Linux x86

* [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/daily/)

* [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/releasedhets.bz2)

* [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux/versions/)

* Linux x86_64

* [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/daily/)

* [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/releasedhets.bz2)

* [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/linux64/versions/)

* Solaris

* [Daily snapshot](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/daily/)

* [Latest release](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/releasedhets.bz2)

* [All versions](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/pc-solaris/versions/)

#### 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)](http://www.informatik.uni-bremen.de/uDrawGraph/en/) (formerly known as daVinci) that relies on [Tcl/Tk (version 8.4 or 8.5)](http://www.tcl.tk/software/tcltk/8.4.html) (which probably has been already installed on your computer anyway). Make sure uDrawGraph and wish are in your $PATH.

Download the [CASL libraries](http://www.informatik.uni-bremen.de/cofi/index.php/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](https://github.com/spechub/Hets/wiki/RESTful-Interface)

### User Documentation

A good starting point is the [Hets user guide](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf) and the [Hets user guide for Common Logic users](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/UserGuideCommonLogic.pdf). Furthermore two vidoes showing a heterogeneous proof are available:

* [A small video showing a heterogeneous proof](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/hets.m2v)

* [A new video (H.264-Codec) showing a heterogeneous proof](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/Hets.mov)

For a formal introduction to hets see the introductory paper [The Heterogeneous Tool Set](http://www.informatik.uni-bremen.de/~till/papers/hets-paper.pdf) 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](http://www.informatik.uni-bremen.de/~till/papers/habil.pdf) by Till Mossakowski.

For questions related to hets there is a [mailing list](http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users).

### Emacs Mode for CASL specifications

To support writing CASL specifications we have an [emacs mode](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/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](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/hetcasl.sty) style file.

## Development

A good starting point is the code documentation for [Hets - the Heterogeneous Tool Set](http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/src-distribution/versions/Hets/docs/).

Since Hets is rather large and complex we recommend following the interactive session in [Debugging and Testing Hets](https://github.com/spechub/Hets/wiki/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](http://www.informatik.uni-bremen.de/~till/papers/habil.pdf).

### Haskell

Hets is written in [Haskell](http://www.haskell.org), and is compiled using [GHC](http://www.haskell.org/ghc) using a couple of [language extensions](http://www.haskell.org/ghc/docs/latest/html/users_guide/ghc-language-features.html). Among the Haskell [books and tutorials](http://www.haskell.org/haskellwiki/Books_and_tutorials) we recommend [Real World Haskell](http://book.realworldhaskell.org/).

The [language definition](http://www.haskell.org/onlinereport) 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](http://www.haskell.org/onlinereport/prelude-index.html).

For searching or looking up any [library functions](http://www.haskell.org/ghc/docs/latest/html/libraries) you may also try [Hoogle](http://www.haskell.org/hoogle).

Also look into [programming guidelines](http://www.haskell.org/haskellwiki/Programming_guidelines) and [things to avoid in Haskell](http://www.haskell.org/haskellwiki/Things_to_avoid).

### Dependencies

Dependencies can be installed as specified in [Hets Development](#hets-development)

### Contributing changes

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

* Use [scan](http://projects.haskell.org/style-scanner/) 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](http://community.haskell.org/~ndm/hlint/) which you may install by `cabal install hlint`.

Also have a look at the current [Release Notes](https://github.com/spechub/Hets/releases/latest), [Debugging and Testing Hets](https://github.com/spechub/Hets/wiki/Debugging-and-Testing-Hets),[Code Review](https://github.com/spechub/Hets/wiki/Code-Review) and [Branching](https://github.com/spechub/Hets/wiki/Branching).

If you want to participate in the Hets development feel free to tell us via our [mailing list](http://www.informatik.uni-bremen.de/mailman/listinfo/hets-devel) 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](https://help.github.com/articles/fork-a-repo) 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](https://docs.haskellstack.org/en/stable/install_and_upgrade) (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

* We recommend the [Git - SVN Crash Course](http://git-scm.com/course/svn.html).

* For github specific info on checking out this repository see [Fetching a remote](https://help.github.com/articles/fetching-a-remote).

## License

The Hets source code is licensed under the GPLv2 or higher