Skip to content


Repository files navigation

Index of this directory

The core library

File Description
make.hl Top-level load file
streams.hl Library for streams
misc.hl Miscellanea
tunify.hl Unification helper functions
solvers.hl Basic solvers and HO solvers
list_solvers.hl Solvers for lists

Additional library and examples

File Description
itaut.hl Our ITAUT solver
lisp.hl A lisp like language and quine generator
lock.hl Examples from The Mystery of the Monte Carlo Lock
ski.hl Experiments with SKI combinators (incomplete)
lambda.hl Experiments with lambda-calculus (incomplete)

Support material

File Description
sexp.hl Datatype and syntax for sexps

Test files

File Description
solvers_test.hl Tests for basic solvers
list_solvers_test.hl Tests for lists solvers

How to load this code using Nix

nix-shell -p hol_light
rlwrap hol_light
loads "";;
load_path := "/Users/maggesi/Devel/HOL" :: !load_path;;
loadt "kanren-light/make.hl";;

How to build and the Docker image

Build the image:

docker build -t kanren-light Docker


docker build --pull --no-cache -t kanren-light Docker

then start the container:

docker run --rm -it -v "$PWD:/home/opam/work" kanren-light

ocaml is started automatically.

Then, load HOL Light:

#use "";;
load_path := "/home/opam/work" :: !load_path;;
loadt "kanren-light/make.hl";;

Build a docker container with the checkpointed HOL images

docker container rm kanren-light

docker run -it -h kanren-light --name kanren-light \
  -v "$PWD:/home/opam/work" \
  kanren-light screen

In one screen terminal

dmtcp_coordinator -q -p 7779

In another screen terminal (C-a c)

dmtcp_launch -q -j -p 7779 ocaml -I `camlp5 -where` -init

Once finished loading (before checkpoint)

load_path := "/home/opam/work" :: !load_path;;
loads "";;

Back into the first terminal (C-a n to cycle between screen terminals)


Commit the docker container:

docker commit -m "With checkpointed HOL" kanren-light kanren-light-ckpt
docker container rm kanren-light-ckpt

docker create -it -h kanren-light --name kanren-light-ckpt \
  --entrypoint "/home/opam/hol-light/" \
  -v "$PWD:/home/opam/work" \

docker start -i kanren-light-ckpt

Then load kanren light:

loadt "kanren-light/make.hl";;