The following commit has been merged in the master branch: commit 54edc1206a675c53c40f59f5dff2ccc1cbe1a0b0 Author: Hendrik Tews <hend...@askra.de> Date: Mon Mar 19 11:40:06 2012 +0100
fix camlp5 dependencies and other small changes diff --git a/debian/README.Debian b/debian/README.Debian index b470895..f9ea4d4 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -8,5 +8,33 @@ HOL Light runs inside an OCaml toplevel. On every session start, the logical core and all auxilary theorems are loaded as sources into the OCaml toplevel. On modern hardware this takes about 2 minutes. +It is possible to save a snapshot of a running HOL Light instance to +disk by using a user-level checkpointing tool. In Debian, dmtcp is +available. To use it do: - -- Hendrik Tews <hend...@askra.de>, Thu, 15 Mar 2012 16:29:01 +0100 +1. install dmtcp: become root and do + + aptitude install + +2. run hol-light under control of dmtcp + + dmtcp_checkpoint hol-light + +3. When you reached a state that you want to save, do + + dmtcp_command --checkpoint + + in a different terminal. This creates several dmtcp* and ckpt* + files in the directory where you started hol-light. + +4. To restart your snapshop do + + ./dmtcp_restart_script.sh + + +Keep in mind that the snapshots of dmtcp contain all needed shared +libraries. You should therefore regenerate your snapshots after +installing security updates. + + + -- Hendrik Tews <hend...@askra.de>, Mon, 19 Mar 2012 11:09:15 +0100 diff --git a/debian/control b/debian/control index 239a055..beb481e 100644 --- a/debian/control +++ b/debian/control @@ -15,7 +15,7 @@ Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/hol-light.git Package: hol-light -Architecture: all +Architecture: any Depends: camlp5, ocaml-base-nox-${F:OCamlABI}, @@ -23,7 +23,8 @@ Depends: ${shlibs:Depends}, ${misc:Depends} Suggests: - readline-editor + readline-editor, + dmtcp Description: HOL Light theorem prover HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL diff --git a/debian/hol-light.sh b/debian/hol-light.sh index a467605..1bc7bd2 100755 --- a/debian/hol-light.sh +++ b/debian/hol-light.sh @@ -2,10 +2,10 @@ #set -xe -if [ -f /usr/bin/readline-edito ] ; then +if [ -f /usr/bin/readline-editor ] ; then readline=/usr/bin/readline-editor else readline= fi -$readline /usr/bin/ocaml $* -init /usr/share/hol-light/hol.ml +exec $readline /usr/bin/ocaml $* -init /usr/share/hol-light/hol.ml diff --git a/debian/rules b/debian/rules index d05b1fd..b49bc3a 100755 --- a/debian/rules +++ b/debian/rules @@ -16,8 +16,6 @@ export DH_OPTIONS=-v include /usr/share/ocaml/ocamlvars.mk -CAMLP5_ABI ?= $(shell /usr/bin/camlp5 -v 2>&1 | { read a b c d && echo $$c; }) - # This has to be exported to make some magic below work. export DH_OPTIONS @@ -41,7 +39,10 @@ override_dh_auto_install: install -d $(INSTDIR)/usr/bin install debian/hol-light.sh $(INSTDIR)/usr/bin/hol-light +.PHONY: override_dh_ocaml +override_dh_ocaml: + dh_ocaml --runtime-map hol-light + .PHONY: override_dh_gencontrol override_dh_gencontrol: - dh_gencontrol -- -VF:OCamlABI="$(OCAML_ABI)" \ - -VF:Camlp5ABI="$(CAMLP5_ABI)" + dh_gencontrol -- -VF:OCamlABI="$(OCAML_ABI)" -- hol-light packaging _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits