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