Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update descriptions about checkpointing tools and other minor details #87

Merged
merged 1 commit into from
Jan 12, 2024
Merged

Update descriptions about checkpointing tools and other minor details #87

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions Makefile
View file
Open in desktop
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
Open in desktop
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";;
Copy link
Contributor

@mpu mpu Jan 11, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need for this #use "selfie.ml";;, rather you just do Selfie.snap "output.img";; below.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Umm, on my ocaml instance I am seeing this error message without #use "selfie.ml";;:

        Camlp5 parsing version 7.10

# #load "selfie.cma";;       
# Selfie.snap "test";;       
File "help.ml" already loaded
Characters 0-11:             
  Selfie.snap "test";;       
  ^^^^^^^^^^^                
Error: Unbound module Selfie

Would it require additional settings?


(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
Loading