From 1f53d207fc9702240d30d9c8fef1de78f3008775 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Wed, 10 Jan 2024 15:49:15 -0600 Subject: [PATCH] Update descriptions about checkpointing tools and other minor details 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. --- Makefile | 9 ++--- README | 115 ++++++++++++++++++++++--------------------------------- 2 files changed, 49 insertions(+), 75 deletions(-) diff --git a/Makefile b/Makefile index e55039d6..118c8810 100644 --- a/Makefile +++ b/Makefile @@ -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. # # # @@ -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; \ diff --git a/README b/README index a1b67e99..8e4379ae 100644 --- a/README +++ b/README @@ -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 @@ -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: @@ -94,7 +95,7 @@ too difficult, depending on the platform. or - opam install camlp5 + opam pin add camlp5 However, you may get a version in "transitional" instead of "strict" mode (do "camlp5 -pmode" to check which you have). @@ -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 --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.