[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483
The following commit has been merged in the master branch: commit 452b483ad50ec27ab0ed4602e8c2dfbee3a9d24a Author: Hendrik Tews Date: Thu May 31 10:12:37 2012 +0200 add patch holtest-dependency-hint diff --git a/.pc/applied-patches b/.pc/applied-patches index 0c7a73b..c4fb8a5 100644 --- a/.pc/applied-patches +++ b/.pc/applied-patches @@ -1,2 +1,3 @@ default-hollight-dir holtest-no-proof-recording.patch +holtest-dependency-hint.patch diff --git a/.pc/default-hollight-dir/.timestamp b/.pc/holtest-dependency-hint.patch/.timestamp similarity index 100% copy from .pc/default-hollight-dir/.timestamp copy to .pc/holtest-dependency-hint.patch/.timestamp diff --git a/holtest b/.pc/holtest-dependency-hint.patch/holtest similarity index 100% copy from holtest copy to .pc/holtest-dependency-hint.patch/holtest diff --git a/debian/README.Debian b/debian/README.Debian index b2c2006..5695844 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -17,8 +17,9 @@ pari-gp and maxima. The SAT-solver interface of HOL Light requires MiniSat and zChaff. MiniSat can be installed as package minisat, but zChaff has a very restrictive license. If you are eligible you can install it from http://www.princeton.edu/~chaff/zchaff.html . HOL -Light can also make use of cddlib, which is freely available from -http://www.ifor.math.ethz.ch/~fukuda/cdd_home/ . +Light can also make use of cddlib (freely available from +http://www.ifor.math.ethz.ch/~fukuda/cdd_home/) and of squolem2 +(available at http://www.cprover.org/qbv/). 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 @@ -50,10 +51,11 @@ installing security updates. The HOL Light test suite is in /usr/share/hol-light/holtest. You -should install the packages prover9, coinor-csdp and pari-gp before -running it. The test suite will run for several hours (12 hours on -Core Duo 2.8 GHz). To check success you have to search for "Error", -"Not_found" and "not found" in the output, for example by doing +should install the packages prover9, coinor-csdp, pari-gp and +libocamlgraph-ocaml-dev before running it. The test suite will run for +several hours (15 hours on Core Duo 2.8 GHz). To check success you +have to search for "Error", "Not_found" and "not found" in the output, +for example by doing /usr/share/hol-light/holtest 2>&1 | tee holtest.log | egrep -i '###|error|not.found' @@ -62,7 +64,13 @@ With this command you can watch all HOL Light messages flying by with On Debian the test suite will produce one error "Error: skip Minisat/make.ml...", because the Minisat examples cannot -be run without zChaff, which is not available in Debian. +be run without zChaff, which is not available in Debian. Further, +there are a number of false positives, because a number of values and +exceptions contain "error" in their name. +Note that some tests pass successfully even if the functionality is +not available. For instance, "QBF/make.ml" is loaded successfully, +regardless of whether squolem2 is installed or not. - -- Hendrik Tews , Wed, 4 Apr 2012 20:55:23 +0200 + + -- Hendrik Tews , Thu, 31 May 2012 09:28:43 +0200 diff --git a/debian/changelog b/debian/changelog index 34ccd6d..8141026 100644 --- a/debian/changelog +++ b/debian/changelog @@ -5,8 +5,9 @@ hol-light (20120530-1) unstable; urgency=low adapt-holtest-for-debian and pa-j-makefile-fix * adapt debian/copyright * simplify debian/rules + * add patch holtest-dependency-hint - -- Hendrik Tews Wed, 30 May 2012 16:54:15 +0200 + -- Hendrik Tews Thu, 31 May 2012 10:12:15 +0200 hol-light (20120423-1) unstable; urgency=low diff --git a/debian/control b/debian/control index e8b7c83..d5890cf 100644 --- a/debian/control +++ b/debian/control @@ -27,7 +27,8 @@ Suggests: coinor-csdp, pari-gp, maxima, - dmtcp + dmtcp, + libocamlgraph-ocaml-dev 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/patches/holtest-dependency-hint.patch b/debian/patches/holtest-dependency-hint.patch new file mode 100644 index 000..7a97bac --- /dev/null +++ b/debian/patches/holtest-dependency-hint.patch @@ -0,0 +1,13 @@ +Description: add ocamlgraph dependency comment in holtest for QBF +Author: Hendrik Tews +--- a/holtest b/holtest +@@ -10,7 +10,7 @@ + # You might first want to install the necessary external tools, + # for instance with + # +-# aptitude install prover9 coinor-csdp pari-gp ++# aptitude install prover9 coinor-csdp pari-gp libocamlgraph-ocaml-dev + # + ### + diff --git a/debian/patches/series b/debian/patches/series index 0c7a73b..c4fb8a5 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,2 +1,3 @@ default-hollight-dir holtest-no-proof-recording.patch +holtest-d
[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483
The following commit has been merged in the master branch:
commit 074b903e7ec3efeb67abfa298a29dfdfd7fa7038
Author: Hendrik Tews
Date: Wed May 30 16:54:37 2012 +0200
don't override dh_gencontrol
diff --git a/debian/changelog b/debian/changelog
index 29f1d31..34ccd6d 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,11 +1,12 @@
hol-light (20120530-1) unstable; urgency=low
* new upstream version revision 141 from 2012-05-30
- * remove patches that have been applied upstream:
+ * remove patches that have been applied upstream:
adapt-holtest-for-debian and pa-j-makefile-fix
- * adapt debian/copyright
+ * adapt debian/copyright
+ * simplify debian/rules
- -- Hendrik Tews Wed, 30 May 2012 09:29:26 +0200
+ -- Hendrik Tews Wed, 30 May 2012 16:54:15 +0200
hol-light (20120423-1) unstable; urgency=low
diff --git a/debian/control b/debian/control
index 182fd58..e8b7c83 100644
--- a/debian/control
+++ b/debian/control
@@ -18,7 +18,6 @@ Package: hol-light
Architecture: any
Depends:
camlp5,
- ocaml-base-nox-${F:OCamlABI},
${ocaml:Depends},
${shlibs:Depends},
${misc:Depends}
diff --git a/debian/rules b/debian/rules
index bba8111..ba5cc84 100755
--- a/debian/rules
+++ b/debian/rules
@@ -11,10 +11,8 @@
# build-arch and build-indep targets by Bill Allombert 2001
# Uncomment this to turn on verbose mode.
-#export DH_VERBOSE=1
-#export DH_OPTIONS=-v
-
-include /usr/share/ocaml/ocamlvars.mk
+# export DH_VERBOSE=1
+# export DH_OPTIONS=-v
# This has to be exported to make some magic below work.
export DH_OPTIONS
@@ -50,7 +48,3 @@ override_dh_auto_test:
.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)"
--
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
[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483
The following commit has been merged in the master branch: commit 29d6ce1128b8b3bdf5cad8e88719c90d1d5f4b1c Author: Hendrik Tews Date: Wed May 30 09:35:04 2012 +0200 reapply, adapt patches delete patches adapt-holtest-for-debian, pa-j-makefile-fix diff --git a/.pc/applied-patches b/.pc/applied-patches new file mode 100644 index 000..0c7a73b --- /dev/null +++ b/.pc/applied-patches @@ -0,0 +1,2 @@ +default-hollight-dir +holtest-no-proof-recording.patch diff --git a/.pc/default-hollight-dir/.timestamp b/.pc/default-hollight-dir/.timestamp new file mode 100644 index 000..e69de29 diff --git a/hol.ml b/.pc/default-hollight-dir/hol.ml similarity index 100% copy from hol.ml copy to .pc/default-hollight-dir/hol.ml diff --git a/.pc/holtest-no-proof-recording.patch/.timestamp b/.pc/holtest-no-proof-recording.patch/.timestamp new file mode 100644 index 000..e69de29 diff --git a/holtest b/.pc/holtest-no-proof-recording.patch/holtest similarity index 100% copy from holtest copy to .pc/holtest-no-proof-recording.patch/holtest diff --git a/debian/changelog b/debian/changelog index ddc0bf9..d4e1f9c 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,11 @@ +hol-light (20120530-1) unstable; urgency=low + + * new upstream version revision 141 from 2012-05-30 + * remove patches that have been applied upstream: + adapt-holtest-for-debian and pa-j-makefile-fix + + -- Hendrik Tews Wed, 30 May 2012 09:29:26 +0200 + hol-light (20120423-1) unstable; urgency=low * Initial release (Closes: #663754) diff --git a/debian/patches/adapt-holtest-for-debian.patch b/debian/patches/adapt-holtest-for-debian.patch deleted file mode 100644 index fba2366..000 --- a/debian/patches/adapt-holtest-for-debian.patch +++ /dev/null @@ -1,276 +0,0 @@ -Description: adapt the test suite for running in a Debian installation -Author: Hendrik Tews a/holtest -+++ b/holtest -@@ -1,141 +1,158 @@ -+#!/bin/bash - ### - # Load in a bunch of examples to test HOL Light is working properly - # Try examining the output using something like - # --# egrep -i '###|error in|Not_found' nohup.out -+# egrep -i '###|error|not.found' nohup.out - # - # to see progress and whether anything has gone wrong. -+# -+# You might first want to install the necessary external tools, -+# for instance with -+# -+# aptitude install prover9 coinor-csdp pari-gp -+# - ### - --# Make sure we have an up-to-date hol, and Mizar Light extensions -+set -e - --make hol --(cd Mizarlight; make clean; make) -+if which hol-light > /dev/null ; then -+hollight=hol-light -+else -+# Make sure we have an up-to-date hol, and Mizar Light extensions -+make hol -+(cd Mizarlight; make clean; make) -+hollight=./hol -+fi - - # Standalone examples - --echo '### Loading Library/agm.ml'; echo 'loadt "Library/agm.ml";;' | (time ./hol) --echo '### Loading Library/binary.ml'; echo 'loadt "Library/binary.ml";;' | (time ./hol) --echo '### Loading Library/binomial.ml'; echo 'loadt "Library/binomial.ml";;' | (time ./hol) --echo '### Loading Examples/borsuk.ml'; echo 'loadt "Examples/borsuk.ml";;' | (time ./hol) --echo '### Loading Library/card.ml'; echo 'loadt "Library/card.ml";;' | (time ./hol) --echo '### Loading Examples/combin.ml'; echo 'loadt "Examples/combin.ml";;' | (time ./hol) --echo '### Loading Examples/cong.ml'; echo 'loadt "Examples/cong.ml";;' | (time ./hol) --echo '### Loading Examples/cooper.ml'; echo 'loadt "Examples/cooper.ml";;' | (time ./hol) --echo '### Loading Examples/dlo.ml'; echo 'loadt "Examples/dlo.ml";;' | (time ./hol) --echo '### Loading Library/floor.ml'; echo 'loadt "Library/floor.ml";;' | (time ./hol) --echo '### Loading Examples/forster.ml'; echo 'loadt "Examples/forster.ml";;' | (time ./hol) --echo '### Loading Examples/hol88.ml'; echo 'loadt "Examples/hol88.ml";;' | (time ./hol) --echo '### Loading Examples/holby.ml'; echo 'loadt "Examples/holby.ml";;' | (time ./hol) --echo '### Loading Library/integer.ml'; echo 'loadt "Library/integer.ml";;' | (time ./hol) --echo '### Loading Library/isum.ml'; echo 'loadt "Library/isum.ml";;' | (time ./hol) --echo '### Loading Examples/kb.ml'; echo 'loadt "Examples/kb.ml";;' | (time ./hol) --echo '### Loading Examples/lagrange_lemma.ml'; echo 'loadt "Examples/lagrange_lemma.ml";;' | (time ./hol) --echo '### Loading Examples/mangoldt.ml'; echo 'loadt "Examples/mangoldt.ml";;' | (time ./hol) --echo '### Loading Examples/mccarthy.ml'; echo 'loadt "Examples/mccarthy.ml";;' | (time ./hol) --echo '### Loading Examples/mizar.ml'; echo 'loadt "Examples/mizar.ml";;' | (time ./hol) --echo '### Loading Library/multiplicative.ml'; echo 'loadt "Library/multiplicative.ml";;' | (time ./hol) --echo '### Loading Examples/multiwf.ml'; echo 'loadt "Examples/multiwf.ml";;' | (time ./hol) --echo '### Loading Examples/pell.ml'; e
[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483
The following commit has been merged in the master branch: commit 35c9e74ffcb5c0d7bf8db90ad59806fd79ff6d55 Author: Hendrik Tews Date: Wed May 30 13:36:09 2012 +0200 adapt debian/copyright diff --git a/debian/changelog b/debian/changelog index d4e1f9c..29f1d31 100644 --- a/debian/changelog +++ b/debian/changelog @@ -3,6 +3,7 @@ hol-light (20120530-1) unstable; urgency=low * new upstream version revision 141 from 2012-05-30 * remove patches that have been applied upstream: adapt-holtest-for-debian and pa-j-makefile-fix + * adapt debian/copyright -- Hendrik Tews Wed, 30 May 2012 09:29:26 +0200 diff --git a/debian/copyright b/debian/copyright index c939b00..79eabdd 100644 --- a/debian/copyright +++ b/debian/copyright @@ -10,19 +10,36 @@ Copyright: 1998 University of Cambridge License: BSD-2-clause +Files: miz3/* +Copyright: 2009-2012 Freek Wiedijk +License: BSD-2-clause +Comment: There is no license in subdirectory miz3, but miz3/README + states that this directory is distributed under the same license + terms as HOL Light. + + Files: Permutation/* Copyright: 2005-2007 Marco Maggesi License: BSD-2-clause Comment: There is no license in subdirectory Permutation, but - Permutation/DOC.txt states that all files are distributed under the - same license terms as HOL Light. + Permutation/DOC.txt states that this directory is distributed under + the same license terms as HOL Light. + + +Files: QBF/* +Copyright: 2010-2011 Ondřej Kunčar +License: BSD-2-clause +Comment: There is no license in subdirectory QBF, but QBF/README + states that this directory is distributed under the same license + terms as HOL Light. Files: Unity/* Copyright: 1989-2008 by Flemming Andersen License: BSD-2-clause Comment: There is no license in subdirectory Unity, but Unity/README - states that it is distributed under the same license as HOL Light. + states that this directory is distributed under the same license as + HOL Light. Files: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml @@ -131,6 +148,13 @@ License: Expat SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +Files: Ntrie/ntrie.ml +Copyright: 2009 Clelia Lomuto and Marco Maggesi +License: BSD-2-clause +Comment: There is no license in this file, but it states that this it + distributed under the same license terms as HOL Light. + + Files: debian/* Copyright: 2012 Hendrik Tews License: BSD-2-clause -- 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
[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483
The following commit has been merged in the master branch: commit aa63fee6f172acf3f4327e21f895b498fb1367f8 Merge: 5d8b12913f8137d8f87f6a33b00b75bc702a973d d12928450baf070abf2ef01d9c90ee1d2b11b6ea Author: Hendrik Tews Date: Wed May 30 09:15:47 2012 +0200 Merge commit 'upstream/20120530' -- 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
