Skip to content

Commit

Permalink
Update descriptions about checkpointing tools and other minor details
Browse files Browse the repository at this point in the history 
This patch updates README to explain three checkpointing tools that are working
as of 2024: DMTCP, CRIU and selfie.
Also, minor details of README are updated and a comment saying that ckpt does not
work is added to Makefile.
  • Loading branch information
@aqjune
aqjune committed Jan 11, 2024
1 parent c7ffffb commit 1f53d20
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 75 deletions.
9 changes: 4 additions & 5 deletions Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
###############################################################################
# Makefile for HOL Light #
# #
# Simple "make" just builds the camlp4 syntax extension "pa_j.cmo", which is #
# necessary to load the HOL Light core into the OCaml toplevel. #
# #
# The later options such as "make hol" create standalone images, but only #
# work under Linux when the "ckpt" checkpointing program is installed. #
# Simple "make" just builds the camlp4/camlp5 syntax extension "pa_j.cmo", #
# which is necessary to load the HOL Light core into the OCaml toplevel. #
# #
# See the README file for more detailed information about the build process. #
# #
Expand Down Expand Up @@ -88,6 +85,8 @@ pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx
else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \
fi

# TODO: update this and hol.* commands to use one of checkpointing tools
# other than ckpt.
# Build a standalone hol image called "hol" (needs Linux and ckpt program)

hol: pa_j.cmo ${HOLSRC} update_database.ml; \
Expand Down
115 changes: 45 additions & 70 deletions README
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ too difficult, depending on the platform.

http://caml.inria.fr/ocaml/index.en.html

The HOL Light system uses the OCaml "Num" library for rational
2. num: The HOL Light system uses the OCaml "Num" library for rational
arithmetic. As of OCaml 4.06, this is no longer included in
the core system and will need to be added separately. You can
do this using the OCaml package manager "opam" if you use it by
Expand All @@ -73,12 +73,13 @@ too difficult, depending on the platform.
make all
sudo make install [assuming no earlier errors]

2. camlp5: this is needed to run HOL Light under any OCaml >= 3.10.
3. camlp5: this is needed to run HOL Light under any OCaml >= 3.10.
Somtimes you need a recent version of camlp5 to be compatible with
your OCaml. I recommend downloading the sources for a recent
version from
your OCaml. For example, OCaml 4.05 is compatible with camlp5 7.10 and
OCaml 4.14 is compatible with camlp5 8.02. I recommend downloading
the sources for a recent version from

https://camlp5.github.io/
https://github.com/camlp5/camlp5/releases ('tags' tab has full series)

and building it in "strict" mode before installing it, thus:

Expand All @@ -94,7 +95,7 @@ too difficult, depending on the platform.

or

opam install camlp5
opam pin add camlp5 <version (e.g., 7.10 for ocaml 4.05)>

However, you may get a version in "transitional" instead of
"strict" mode (do "camlp5 -pmode" to check which you have).
Expand Down Expand Up @@ -185,95 +186,69 @@ be available for some platforms. First the basic approach:

Now for the alternative approach of building a standalone image.
The level of convenience depends on the checkpointing program you
have installed. The earlier checkpointing programs in this list
are more convenient to use but seem less easy to get going on
recent Linux kernel/libc combinations.
have installed. As of 2024, there are three programs you can use.

(1) If you have the 'ckpt' program installed, then the Makefile will
conveniently create a HOL Light binary. You can get 'ckpt' here:
(1) DMTCP: you can download from here:

http://www.cs.wisc.edu/~zandy/ckpt/
https://github.com/dmtcp/dmtcp/releases

Once 'ckpt' is installed, simply type
To build DMTCP, please refer to
https://github.com/dmtcp/dmtcp/blob/master/INSTALL.md .
HOL Light does not have convenient commands or scripts to exploit DMTCP,
but you can proceed as follows:

make hol
1. Start ocaml running under the DMTCP coordinator:

in the 'hol-light' directory, and a standalone HOL Light image
called 'hol' should be created. If desired you can move or copy
this to some other place such as '~/bin' or '/usr/local/bin'. You
then simply type 'hol' (or './hol') to start the system up and
start proving theorems.
dmtcp_launch ocaml

Note that although the HOL binary will work on its own, it
does not pre-load all the source files. You will probably want
to keep the sources available to be loaded later as needed (if
you need additional mathematical theories or tools), so it's
better to unpack the HOL distribution somewhere permanent
before doing 'make hol'.
2. Use ocaml to load HOL Light as usual, for example:

If you later develop a large body of proofs or tools, you can
save the augmented system using the command "self_destruct"
(this is the same approach as in the Makefile) rather than
re-load each time. For example, the following will create a
HOL Light binary (always called 'hol.snapshot'):
#use "hol.ml";;

self_destruct "My version of HOL Light";;
3. From another terminal, issue the checkpoint command:

(2) Another checkpointing option is CryoPID, which you can get
here:
dmtcp_command -kc

http://cryopid.berlios.de/
This will kill the ocaml process once checkpointing is done.

In this case, the Makefile doesn't have a convenient way of
making HOL binaries, but you can make one yourself once HOL
Light is loaded and you are sitting in its toplevel loop.
(This also works if you have your own extensions loaded, and
indeed this is when it's most useful.) Instead of the
'self_destruct' command, use 'checkpoint', which is similar
except that the current process is not terminated once the
binary (again called hol.snapshot) is created:
4. Step 3 created a checkpoint of the OCaml process and
a shell script to invoke it, both in the directory in
which ocaml was started. Running that should restore
the OCaml process with all your state and bindings:

checkpoint "My version of HOL Light";;
./dmtcp_restart_script.sh

(3) A third option which seems to work with recent Linuxes is
DMTCP, which you can download from here:
(2) CRIU: CRIU is similar to DMTCP but faster. However, it requires sudo
priviledge depending on your environment (e.g., WSL2).
you can download from here:

http://dmtcp.sourceforge.net/
https://criu.org/Download/criu

You may try installing from the packages (e.g.
'sudo dpkg -i dmtcp.deb'), but I found it was better to
compile from source. HOL Light does not have convenient
commands or scripts to exploit DMTCP, but you can proceed
as follows:
To build CRIU, please refer to https://criu.org/Installation .
To checkpoint,

1. Start ocaml running under the DMTCP coordinator:
1. Start ocaml process and load HOL Light.

dmtcp_checkpoint -n ocaml
2. From another terminal, run

2. Use ocaml to load HOL Light as usual, for example:

#use "hol.ml";;
criu dump -o dump.log -t <ocaml process id> --shell-job

3. From another terminal, issue the checkpoint command:
3. To restore, run

dmtcp_command --checkpoint
criu restore -o restore.log --shell-job

4. (Don't forget this!) Kill the original ocaml process,
e.g. by just typing control-d to the Ocaml prompt.
Please refer to https://criu.org/Simple_loop for details.

5. Step 3 created a checkpoint of the OCaml process and
a shell script to invoke it, both in the directory in
which ocaml was started. Running that should restore
the OCaml process with all your state and bindings:
(3) selfie: This is a convenient OCaml checkpointing tool developed by
Quentin Carbonneaux. Please git clone git://c9x.me/selfie.git and
run `make selfie.cma` from the directory.
Open ocaml and run

./dmtcp_restart_script.sh
# #load "selfie.cma";;
# #use "selfie.ml";;

(4) If none of these options work, you may find some others on the
following Web page. Unfortunately I don't know of any such
checkpointing program for either Windows or Mac OS X; I would
be glad to hear of one.
Now you can use `snap "output.img";;` to checkpoint the process.

http://checkpointing.org

The directories "Library" and "Examples" may give an idea of the
kind of thing that might be done, or may be useful in further work.
Expand Down

0 comments on commit 1f53d20

Please sign in to comment.