The following commit has been merged in the master branch:
commit 2fa332419db16e74ef0a8103be5dfec9b6e3d019
Author: Hendrik Tews <hend...@askra.de>
Date: Thu May 16 16:34:02 2013 +0200
several fixes and OCaml 4 compatibility
diff --git a/debian/README.Debian b/debian/README.Debian
index 5695844..331d58c 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -1,5 +1,9 @@
HOL Light for Debian
---------------------
+====================
+
+
+Usage and Documentation
+-----------------------
On Debian you can use the command hol-light to run HOL Light, see the
man page hol-light(1).
@@ -21,6 +25,10 @@ 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/).
+
+Improve startup time with snapshots
+-----------------------------------
+
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
available. To use it do:
@@ -50,12 +58,15 @@ libraries. You should therefore regenerate your snapshots
after
installing security updates.
+Hol Light test suite
+--------------------
+
The HOL Light test suite is in /usr/share/hol-light/holtest. You
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
+the best part of a day. 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'
@@ -73,4 +84,4 @@ not available. For instance, "QBF/make.ml" is loaded
successfully,
regardless of whether squolem2 is installed or not.
- -- Hendrik Tews <hend...@askra.de>, Thu, 31 May 2012 09:28:43 +0200
+ -- Hendrik Tews <hend...@askra.de>, Fri, 17 May 2013 13:54:06 +0200
diff --git a/debian/changelog b/debian/changelog
index 6294e5f..d13334c 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,16 @@
+hol-light (20130511-1) unstable; urgency=low
+
+ * new upstream version revision 162 from 2013-05-11
+ * fix typo in package description (Closes: #680494)
+ * set prioity to extra
+ * omit new elc file from package
+ * adapt copyright info
+ * add new patch include-compiler-libs for OCaml 4 compatibility
+ * bump to standards version 3.9.4
+ * improve debian readme
+
+ -- Hendrik Tews <hend...@askra.de> Fri, 17 May 2013 13:54:42 +0200
+
hol-light (20120602-1) unstable; urgency=low
* new upstream version revision 146 from 2012-06-02
diff --git a/debian/control b/debian/control
index d5890cf..f69ec9f 100644
--- a/debian/control
+++ b/debian/control
@@ -1,6 +1,6 @@
Source: hol-light
Section: math
-Priority: optional
+Priority: extra
Maintainer: Debian OCaml Maintainers <debian-ocaml-ma...@lists.debian.org>
Uploaders:
Hendrik Tews <hend...@askra.de>
@@ -9,7 +9,7 @@ Build-Depends:
ocaml-base-nox,
dh-ocaml (>= 0.9~),
debhelper (>= 9.0.0)
-Standards-Version: 3.9.3
+Standards-Version: 3.9.4
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git
Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/hol-light.git
@@ -33,5 +33,5 @@ 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
Light is famous for the verification of floating-point
- arithmetic as well as for the Flyspec project, which aims at the
+ arithmetic as well as for the Flyspeck project, which aims at the
formalization of Tom Hales' proof of the Kepler conjecture.
diff --git a/debian/copyright b/debian/copyright
index 79eabdd..824a6bc 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -42,6 +42,15 @@ Comment: There is no license in subdirectory Unity, but
Unity/README
HOL Light.
+Files: RichterHilbertAxiomGeometry/*
+Copyright: 2012 by Bill Richter
+License: BSD-2-clause
+Comment: There is no license in subdirectory
+ RichterHilbertAxiomGeometry, but RichterHilbertAxiomGeometry/README
+ 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
Copyright: 2002-2006 INRIA
License: LGPL-2
diff --git a/debian/hol-light-source.exclude b/debian/hol-light-source.exclude
index 738fb05..1cdb592 100644
--- a/debian/hol-light-source.exclude
+++ b/debian/hol-light-source.exclude
@@ -9,3 +9,4 @@
./QUICK_REFERENCE.txt
./README
./VERYQUICK_REFERENCE.txt
+./RichterHilbertAxiomGeometry/hol-light-fonts.elc
diff --git a/debian/patches/include-compiler-libs.patch
b/debian/patches/include-compiler-libs.patch
new file mode 100644
index 0000000..95e4bcc
--- /dev/null
+++ b/debian/patches/include-compiler-libs.patch
@@ -0,0 +1,15 @@
+Description: include compiler-libs dir for OCaml 4
+Author: Hendrik Tews <hend...@askra.de>
+--- a/hol.ml
++++ b/hol.ml
+@@ -11,7 +11,9 @@
+
+ let hol_version = "2.20++";;
+
+-let debian_hol_light_dir = "/usr/share/hol-light"
++let debian_hol_light_dir = "/usr/share/hol-light";;
++
++#directory "+compiler-libs";;
+
+ let hol_dir = ref
+ (try Sys.getenv "HOLLIGHT_DIR"
diff --git a/debian/patches/series b/debian/patches/series
index 0c7a73b..e0623d1 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
default-hollight-dir
holtest-no-proof-recording.patch
+include-compiler-libs.patch
--
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
