[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. upstream/20120312-4-g54edc12

[Hendrik Tews]

The following commit has been merged in the master branch:
commit 54edc1206a675c53c40f59f5dff2ccc1cbe1a0b0
Author: Hendrik Tews <hendrik at 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 <hendrik at 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 <hendrik at 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