This is an automated email from the git hooks/post-receive script.
hendrik-guest pushed a commit to branch master
in repository hol-light.
commit 1c4af310a9408011df6fcd3475d4f998e47d4196
Author: Hendrik Tews <hend...@askra.de>
Date: Fri Oct 27 22:15:41 2017 +0200
finish packaging with using various upstream fixes
---
debian/README.Debian | 25 ++++++++++++++++++-------
debian/changelog | 22 ++++++++++++++--------
debian/control | 11 ++++++-----
debian/copyright | 28 +++++++++++++++++-----------
debian/hol-light-source.exclude | 1 +
debian/rules | 5 +----
6 files changed, 57 insertions(+), 35 deletions(-)
diff --git a/debian/README.Debian b/debian/README.Debian
index 94317aa..0b8732d 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -58,6 +58,18 @@ libraries. You should therefore regenerate your snapshots
after
installing security updates.
+Native Toplevel
+---------------
+
+The upstream README hints on a 4x runtime improvement by using the
+native OCaml toplevel. The standard OCaml distribution has been
+supporting a native toplevel for a few versions already (``make
+ocamlnat''). Building the necessary camlp5 parts as native plugin is
+not as easy and requires some manual fiddling. However, when I tried
+the last time with OCaml 4.03, HOL Light was running 2 times slower in
+the native toplevel.
+
+
Hol Light test suite
--------------------
@@ -65,7 +77,7 @@ The HOL Light test suite is in /usr/share/hol-light/holtest
and in
/usr/share/hol-light/holtest_parallel. Both scripts run the same
tests, the latter one uses ``make -j $(getconf _NPROCESSORS_ONLN)'' to
run the tests in parallel on all available cores. When I last tried,
-the tests run for about 70 CPU hours (10 hours on 8 cores for the
+the tests run for about 35 CPU hours (12 hours on 8 cores for the
parallel version).
You should install the packages prover9, coinor-csdp, pari-gp and
@@ -76,7 +88,7 @@ capture with something like
/usr/share/hol-light/holtest 2>&1 | tee holtest.log
The parallel version eventually produces the file
-/tmp/hollog_<date+time>/holtest.log containing all the output.
+/tmp/hol-light-test/holtest.log containing all the output.
To check success you have to search for
"Error", "Not_found" and "not found" in the output, for example by
using
@@ -86,10 +98,9 @@ using
On Debian, the test suite will produce the error "Error: skip
Minisat/make.ml...", because the Minisat examples cannot be run
without zChaff, which is not available in Debian. Additionally, the
-tests Mizarlight/make.ml, miz3/make.ml and QBF/make.ml will fail as
-they do for the upstream version. On architecture i386 (and probably
-other 32 bit architectures as well), the test 100/pnt.ml fails because
-it runs out of memory.
+test Mizarlight/make.ml will fail as it does for the upstream version.
+On architecture i386 (and probably other 32 bit architectures as
+well), the test 100/pnt.ml fails because it runs out of memory.
Note that the above grep command produces quite a few false positives,
because a number of values and exceptions contain "error" in their
@@ -97,4 +108,4 @@ name. Note also, that some tests pass successfully even if
the
functionality is not available.
- -- Hendrik Tews <hend...@askra.de>, Mon, 9 Jan 2017 23:30:42 +0100
+ -- Hendrik Tews <hend...@askra.de>, Sun, 29 Oct 2017 20:15:43 +0100
diff --git a/debian/changelog b/debian/changelog
index 9c76245..73bb846 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,14 +1,20 @@
-hol-light (20170917-1) unstable; urgency=medium
+hol-light (20171023-1) unstable; urgency=medium
- * Imported upstream version 20170917
- with git hash 4c464bee35551ce3db2ef42b51bc19f5bf638e78
+ * Imported upstream version 20171023
+ with git hash 39d9bf8b2958a288905661f969e9ab25b5ed74aa
* delete camlp5-7 patch - was applied upstream; refresh other patches
- * compat level 10, standards version 4.1.0
- * update rules with new pa_j implementation
+ * compat level 10, standards version 4.1.1
+ * update rules with new pa_j implementation (Closes: #876533)
* minor change in control file - Flyspeck is completed
- * update copyright file - a number of files have unclear license
+ * update copyright file
+ * clear executable bit deletion in rules - has been fixed upstream
+ * change to priority optional as demanded by lintian
+ * suggests python as demanded by lintian
+ * exclude .pc directory during installation (Closes: #878615)
+ * README.Debian: hints on native toplevel and testsuite updates
+ * delete some trailing whitespace for lintian
- -- Hendrik Tews <hend...@askra.de> Tue, 24 Oct 2017 22:08:25 +0200
+ -- Hendrik Tews <hend...@askra.de> Sun, 29 Oct 2017 20:55:28 +0100
hol-light (20170109-2) unstable; urgency=medium
@@ -45,7 +51,7 @@ hol-light (20131026-1) unstable; urgency=low
* new upstream version revision 177 from 2013-10-26
* use new pa_j and adjust camlp5 dependencies
- * delete executable bit of RichterHilbertAxiomGeometry/Topology.ml
+ * delete executable bit of RichterHilbertAxiomGeometry/Topology.ml
during installation
-- Hendrik Tews <hend...@askra.de> Sun, 10 Nov 2013 20:37:21 +0100
diff --git a/debian/control b/debian/control
index 3afc9f0..2aea737 100644
--- a/debian/control
+++ b/debian/control
@@ -1,15 +1,15 @@
Source: hol-light
Section: math
-Priority: extra
+Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-ma...@lists.debian.org>
Uploaders:
Hendrik Tews <hend...@askra.de>
-Build-Depends:
+Build-Depends:
camlp5 (>= 7.01),
ocaml-base-nox,
dh-ocaml (>= 0.9~),
debhelper (>= 10.0.0)
-Standards-Version: 4.1.0
+Standards-Version: 4.1.1
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Vcs-Git: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/hol-light.git
Vcs-Browser:
https://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/hol-light.git
@@ -19,7 +19,7 @@ Architecture: any
Depends:
camlp5,
${ocaml:Depends},
- ${shlibs:Depends},
+ ${shlibs:Depends},
${misc:Depends}
Suggests:
readline-editor,
@@ -28,7 +28,8 @@ Suggests:
pari-gp,
maxima,
dmtcp,
- libocamlgraph-ocaml-dev
+ libocamlgraph-ocaml-dev,
+ python
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/copyright b/debian/copyright
index 0aa3642..ea1f002 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -10,6 +10,12 @@ Copyright: 1998 University of Cambridge
License: BSD-2-clause
+Files: Boyer_Moore/*
+Copyright: 1994 Richard Boulton, University of Edinburgh, University of
Cambridge, INRIA
+ 2007-2017 Petros Papapanagiotou & Jacques Fleuriot, University of
Edinburgh
+License: BSD-2-clause
+
+
Files: miz3/*
Copyright: 2009-2012 Freek Wiedijk
License: BSD-2-clause
@@ -59,15 +65,14 @@ Comment: There is no license in
that it is distributed under the same license as HOL Light.
-Files: Formal_ineqs/arith/* Formal_ineqs/arith_options.hl Formal_ineqs/docs/*
- Formal_ineqs/informal/* Formal_ineqs/lib/ssreflect/* Formal_ineqs/list/*
- Formal_ineqs/make.ml Formal_ineqs/misc/* Formal_ineqs/taylor/*
- Formal_ineqs/verifier/* Formal_ineqs/verifier_options.hl
-Copyright: 2012-2014 Alexey Solovyev
+Files: Formal_ineqs/*
+Copyright: 2014-2017 Alexey Solovyev
+License: BSD-2-clause
+
+
+Files: Formal_ineqs/lib/ipow.hl
+Copyright: 2014-2017 Alexey Solovyev and the University of Utah
License: BSD-2-clause
-Comment: There is no license in all these subdirectories, but
- Formal_ineqs/README.md states that this directory is distributed
- under the same license as HOL Light.
Files: Functionspaces/*
@@ -88,9 +93,10 @@ Comment: There is no license in subdirectory IEEE, but
Files: IsabelleLight/*
-Copyright: 2009-2015, Petros Papapanagiotou, Jacques Fleuriot,
- University of Edinburgh
-License: missing/unclear
+Copyright: 2009-2017, Petros Papapanagiotou, Jacques Fleuriot,
+ Centre of Intelligent Systems and their Applications,
+ University of Edinburgh
+License: BSD-2-clause
Files: Library/q.ml
diff --git a/debian/hol-light-source.exclude b/debian/hol-light-source.exclude
index 29ab059..6e2329a 100644
--- a/debian/hol-light-source.exclude
+++ b/debian/hol-light-source.exclude
@@ -1,6 +1,7 @@
./debian
./.git
./.gitignore
+./.pc
./CHANGES
./LICENSE
./Makefile
diff --git a/debian/rules b/debian/rules
index f641860..c13f39e 100755
--- a/debian/rules
+++ b/debian/rules
@@ -12,7 +12,7 @@
# Uncomment this to turn on verbose mode.
# export DH_VERBOSE=1
-# export DH_OPTIONS=-v
+# export DH_OPTIONS=-v
# This has to be exported to make some magic below work.
export DH_OPTIONS
@@ -37,9 +37,6 @@ override_dh_auto_install:
install -d $(INSTDIR)/usr/share/hol-light
tar --anchored --exclude-from=debian/hol-light-source.exclude -c . | \
tar -C $(INSTDIR)/usr/share/hol-light -x
- chmod -x $(INSTDIR)/usr/share/hol-light/Help/HYP_TAC.doc
- chmod -x
$(INSTDIR)/usr/share/hol-light/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
- chmod -x $(INSTDIR)/usr/share/hol-light/Multivariate/cvectors.ml
install -d $(INSTDIR)/usr/bin
install debian/hol-light.sh $(INSTDIR)/usr/bin/hol-light
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git
_______________________________________________
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
