[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. debian/20120602-1-3-g2fa3324

[Hendrik Tews]

The following commit has been merged in the master branch:
commit 2fa332419db16e74ef0a8103be5dfec9b6e3d019
Author: Hendrik Tews <hendrik at 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 <hendrik at askra.de>, Thu, 31 May 2012 09:28:43 +0200
+ -- Hendrik Tews <hendrik at 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 <hendrik at 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-maint at lists.debian.org>
 Uploaders:
  Hendrik Tews <hendrik at 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 <hendrik at 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