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

[Hendrik Tews]

The following commit has been merged in the master branch:
commit 2e9954744c4e1a49eb9d156750eb72b771f3a7ec
Author: Hendrik Tews <hendrik at askra.de>
Date:   Thu Mar 22 14:42:08 2012 +0100

    tests and other changes
    - invoke some of the holtest tests in debian/test-hol-light
    - build and install the Mizarlight syntax extension
    - put external tools into Suggests:

diff --git a/debian/control b/debian/control
index beb481e..182fd58 100644
--- a/debian/control
+++ b/debian/control
@@ -24,6 +24,10 @@ Depends:
  ${misc:Depends}
 Suggests:
  readline-editor,
+ prover9,
+ coinor-csdp,
+ pari-gp,
+ maxima,
  dmtcp
 Description: HOL Light theorem prover
  HOL Light is an interactive theorem prover for Higher-Order Logic
diff --git a/debian/rules b/debian/rules
index b49bc3a..5ece79f 100755
--- a/debian/rules
+++ b/debian/rules
@@ -27,6 +27,7 @@ export DH_OPTIONS
 override_dh_auto_build:
 	cp pa_j_3.1x_6.02.2.ml pa_j.ml
 	make
+	make -C Mizarlight
 
 INSTDIR:=debian/hol-light
 .PHONY: override_dh_auto_install
@@ -39,6 +40,10 @@ override_dh_auto_install:
 	install -d $(INSTDIR)/usr/bin
 	install debian/hol-light.sh $(INSTDIR)/usr/bin/hol-light
 
+.PHONY: override_dh_auto_test
+override_dh_auto_test:
+	debian/test-hol-light
+
 .PHONY: override_dh_ocaml
 override_dh_ocaml:
 	dh_ocaml --runtime-map hol-light
diff --git a/debian/test-hol-light b/debian/test-hol-light
new file mode 100755
index 0000000..e300beb
--- /dev/null
+++ b/debian/test-hol-light
@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -e
+
+function hol_light () {
+    /usr/bin/ocaml -init hol.ml
+}
+
+function holtest() {
+    echo "######################## HOL Light test $1 ###################"
+    echo "loadt \"$1\";;" | hol_light 2>&1 | tee /tmp/hol-light-test-log
+    if egrep -i 'error|not_found' /tmp/hol-light-test-log ; then
+	echo 
+	echo Error in $1, test failed
+	false
+    fi
+}
+
+holtest Library/agm.ml
+holtest Library/binary.ml
+holtest Library/binomial.ml
+holtest Library/card.ml
+
+# The prover9 example fails in a clean build environment, because
+# prover9 is not installed there. If you want to test whether error
+# detection works in this script, uncomment the next holtest line.
+
+#holtest Examples/prover9.ml

-- 
hol-light packaging