Dear all,
Some time ago (in the times of Debian Stretch :-)) I made
a Dockerfile for HOL Light, see the attachment.
The commands I used for building the image and running
it are:
docker build -t hol-light .
docker run -i -v /home/freek:/home/freek --name hol-light hol-light
You need to run the build command in the directory (".") that
has the Dockerfile in it. Of course, the directory you
want to mount in the container in your case probably will
not be /home/freek :-)
Then at the ocaml prompt ("# ") when running the image,
I input some ocaml commands:
#use "hol.ml";;
loads "update_database.ml";;
#load "unix.cma";;
let cd path = Unix.chdir path;;
let pwd () = Unix.getcwd ();;
let ls () = Unix.system "/bin/ls -C";;
cd "/home/freek";;
ls ();;
I have Docker checkpointing enabled
in my /etc/docker/daemon.json, see
https://docs.docker.com/engine/reference/commandline/checkpoint/,
so in a different window I then gave the command:
docker checkpoint create hol-light hol
This creates the checkpoint. Finally, I then run HOL Light
every time using:
docker start -i --checkpoint hol hol-light
It still takes some time to start, but you don't have
to go through the initialisation of the system with #use
"hol.ml";; every time...
Unfortunately, you cannot have two instances of this running
at the same time. If someone can tell me how to do that
(I'm not really a Docker user), I would appreciate that.
Even if you don't want to use docker, the Dockerfile shows
commands to install the system in a way that works :-) I
_think_ I even tested that the SOS stuff works in this setup.
Hope this is useful to someone.
Freek
FROM debian:stretch-slim
RUN \
apt update && \
DEBIAN_FRONTEND=noninteractive apt-get -yq install \
ocaml camlp5 git make coinor-csdp && \
cd /usr/src && \
git clone https://github.com/jrh13/hol-light.git && \
cd hol-light && \
make
WORKDIR /usr/src/hol-light
CMD /usr/bin/ocaml
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
