The following commit has been merged in the master branch:
commit 2e9954744c4e1a49eb9d156750eb72b771f3a7ec
Author: Hendrik Tews <hend...@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
_______________________________________________
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
