#!/bin/sh

# assuming Debian or Ubuntu:
sudo apt install opam wget sagemath -y

# Ubuntu 22.04 needs the --disable-sandboxing
time opam init -a --disable-sandboxing
time opam switch create 4.05.0
eval `opam env`
time opam pin add camlp5 7.10 -y
time opam install num camlp-streams ocamlfind -y

cd
git clone https://github.com/jrh13/hol-light
cd hol-light
make

# takes about 10 minutes
wget https://cr.yp.to/2023/hull-light-20230416.sage
time sage hull-light-20230416.sage > hull-light.ml
time ocaml -I `camlp5 -where` camlp5o.cma -init hol.ml \
< hull-light.ml > hull-light.out

# stronger internal lemmas (optional), takes about 5 hours:
time sage hull-light-20230416.sage exact > hull-light-exact.ml
time ocaml -I `camlp5 -where` camlp5o.cma -init hol.ml \
< hull-light-exact.ml > hull-light-exact.out