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

[Hendrik Tews]

The following commit has been merged in the master branch:
commit c82df05722dfeebff899ae1d4b0a6f5bdc15054b
Author: Hendrik Tews <hendrik at askra.de>
Date:   Sun Mar 25 22:28:35 2012 +0200

    Adapt README.Debian and holtest

diff --git a/.pc/applied-patches b/.pc/applied-patches
index 25ddc84..cd58477 100644
--- a/.pc/applied-patches
+++ b/.pc/applied-patches
@@ -1,2 +1,3 @@
 default-hollight-dir
 adapt-holtest-for-debian.patch
+holtest-no-proof-recording.patch
diff --git a/.pc/adapt-holtest-for-debian.patch/.timestamp b/.pc/holtest-no-proof-recording.patch/.timestamp
similarity index 100%
copy from .pc/adapt-holtest-for-debian.patch/.timestamp
copy to .pc/holtest-no-proof-recording.patch/.timestamp
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/README.Debian b/debian/README.Debian
index b01e6bd..79e92e4 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -9,7 +9,16 @@ website at http://www.cl.cam.ac.uk/~jrh13/hol-light/
 
 HOL Light runs inside an OCaml toplevel. On every session start, the
 logical core and all auxilary theorems are loaded as sources into the
-OCaml toplevel. On modern hardware this takes about 2 minutes.
+OCaml toplevel. On modern hardware this takes about 90 seconds.
+
+HOL Light can use several external tools. Prover9, csdp, pari-gp and
+Maxima are available in Debian as packages prover9, coinor-csdp,
+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/ .
 
 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
@@ -40,4 +49,20 @@ libraries. You should therefore regenerate your snapshots after
 installing security updates.
 
 
- -- Hendrik Tews <hendrik at askra.de>, Wed, 21 Mar 2012 21:48:26 +0100
+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
+
+    /usr/share/hol-light/holtest 2>&1 | tee holtest.log | egrep -i '###|error|not.found' 
+
+With this command you can watch all HOL Light messages flying by with
+"tail -f holtest.log". 
+
+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.
+
+
+ -- Hendrik Tews <hendrik at askra.de>, Sun, 25 Mar 2012 22:28:24 +0200
diff --git a/debian/patches/holtest-no-proof-recording.patch b/debian/patches/holtest-no-proof-recording.patch
new file mode 100644
index 0000000..5e557bc
--- /dev/null
+++ b/debian/patches/holtest-no-proof-recording.patch
@@ -0,0 +1,16 @@
+Description: don't build the proof-recording version as part of the test suite
+Author: Hendrik Tews <hendrik at askra.de>
+--- a/holtest
++++ b/holtest
+@@ -155,7 +155,7 @@
+ echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time $hollight)
+ 
+ # Build the proof-recording version of HOL
+-
+-echo '### Building proof-recording version';
+-cd Proofrecording/hol_light
+-make clean; make hol
++# ... not on Debian
++# echo '### Building proof-recording version';
++# cd Proofrecording/hol_light
++# make clean; make hol
diff --git a/debian/patches/series b/debian/patches/series
index 25ddc84..cd58477 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
 default-hollight-dir
 adapt-holtest-for-debian.patch
+holtest-no-proof-recording.patch
diff --git a/holtest b/holtest
index 09ce73f..6753d66 100755
--- a/holtest
+++ b/holtest
@@ -155,7 +155,7 @@ echo '### Loading 100/two_squares.ml'; echo 'loadt "100/two_squares.ml";;' | (ti
 echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time $hollight)
 
 # Build the proof-recording version of HOL
-
-echo '### Building proof-recording version';
-cd Proofrecording/hol_light
-make clean; make hol
+# ... not on Debian
+# echo '### Building proof-recording version';
+# cd Proofrecording/hol_light
+# make clean; make hol

-- 
hol-light packaging