HIP/SLEEK

Build

You will need opam and OCaml 4.14.1.

# Install opam dependencies
OPAMYES=true rake dependencies:install

# Build everything
rake

# Build only some targets
rake hip
rake sleek

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

./hip examples/working/hip/ll.ss
./sleek examples/working/sleek/sleek2.slk

To run tests,

# Tested on Perl 5.34
cpanm File::NCopy Spreadsheet::WriteExcel Spreadsheet::ParseExcel

cd examples/working
./run-fast-tests.pl sleek # around 4 mins
./run-fast-tests.pl hip # around 40 mins

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 examples/working/hip/ll.ss
./sleek -tp mona examples/working/sleek/sleek2.slk

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)