[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120423-1-7-g452b483

[Hendrik Tews]

The following commit has been merged in the master branch:
commit 452b483ad50ec27ab0ed4602e8c2dfbee3a9d24a
Author: Hendrik Tews <hendrik at askra.de>
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 <hendrik at askra.de>, Wed,  4 Apr 2012 20:55:23 +0200
+
+ -- Hendrik Tews <hendrik at askra.de>, 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 <hendrik at askra.de>  Wed, 30 May 2012 16:54:15 +0200
+ -- Hendrik Tews <hendrik at askra.de>  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 0000000..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 <hendrik at askra.de>
+--- 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-dependency-hint.patch
diff --git a/holtest b/holtest
index de3d4ff..671113e 100755
--- 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
 #
 #######################################################################
 

-- 
hol-light packaging