Installation - The HIP/SLEEK system

Building HIP and SLEEK

You will need opam and a recent OCaml compiler (tested on 4.14.1).

opam install . --deps-only
dune build @hipsleek

# To use ocamldebug
rake debug:hip debug:sleek

Try verifying some small programs. You will need Z3 (from opam, pip, or a system package manager) and Omega (below) on the PATH.

dune exec ./hip.exe dune-tests/hip/ll.t/ll.ss
dune exec ./sleek.exe dune-tests/sleek/sleek2.t/sleek2.ss

Installing SLEEK as a library

opam install .

Running tests

dune test

Installing external provers

Other external provers HIP/SLEEK uses can be built from source. They will be installed in their respective directories and should be made available on the PATH.

Here is an example .envrc file which makes all the provers available, after following the steps below to build each one:

eval "$(opam env --switch=4.14.1 --set-switch)"
PATH_add omega_modified/omega_calc/obj
PATH_add mona-1.4/bin
PATH_add fixcalc_src

Omega

(cd omega_modified; make oc)

Mona

tar -xvf mona-1.4-modif.tar.gz
cd mona-1.4
./configure --prefix=$(pwd)
make install
cp mona_predicates.mona ..
cd -

Try some tests:

./hip -tp mona dune-tests/hip/ll.t/ll.ss
./sleek -tp mona dune-tests/sleek/sleek2.t/sleek2.ss

Fixcalc

You will need GHC 9.4.8.

cabal install --lib regex-compat old-time
cabal install happy

Build Omega first. Then, in the hipsleek project directory,

git clone https://github.com/hipsleek/omega_stub.git
(cd omega_stub; make)

git clone https://github.com/hipsleek/fixcalc.git fixcalc_src
(cd fixcalc_src; make fixcalc)