[Pkg-ocaml-maint-commits] [hol-light] 03/03: update packaging for new upstream version
Hendrik Tews
hendrik-guest at moszumanska.debian.org
Thu Jan 12 08:12:53 UTC 2017
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 db54cd89ee1b59337e9583b6a327a8d94bae2abc
Author: Hendrik Tews <hendrik at askra.de>
Date: Mon Jan 9 23:32:00 2017 +0100
update packaging for new upstream version
---
debian/README.Debian | 51 ++++++++------
debian/changelog | 23 +++++++
debian/control | 6 +-
debian/copyright | 91 ++++++++++++++++++++++++-
debian/hol-light-source.exclude | 5 +-
debian/patches/cd-holtest-parallel.patch | 13 ++++
debian/patches/holtest-no-proof-recording.patch | 2 +-
debian/patches/series | 1 +
debian/rules | 5 +-
9 files changed, 169 insertions(+), 28 deletions(-)
diff --git a/debian/README.Debian b/debian/README.Debian
index 331d58c..94317aa 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -12,7 +12,7 @@ For information on how to use HOL Light, please visit the HOL Light
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
+logical core and all auxiliary theorems are loaded as sources into the
OCaml toplevel. On modern hardware this takes about 90 seconds.
HOL Light can use several external tools. Prover9, CSDP, PARI/GP and
@@ -61,27 +61,40 @@ 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
-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
+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
+parallel version).
+
+You should install the packages prover9, coinor-csdp, pari-gp and
+libocamlgraph-ocaml-dev before running the tests. The sequential
+version produces the output on standard output, which you should
+capture with something like
- /usr/share/hol-light/holtest 2>&1 | tee holtest.log | egrep -i '###|error|not.found'
+ /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.
+To check success you have to search for
+"Error", "Not_found" and "not found" in the output, for example by
+using
-With this command you can watch all HOL Light messages flying by with
-"tail -f holtest.log".
+ egrep -i 'error|not.found'
-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. Further,
-there are a number of false positives, because a number of values and
-exceptions contain "error" in their name.
+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.
-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.
+Note that the above grep command produces quite a few false positives,
+because a number of values and exceptions contain "error" in their
+name. Note also, that some tests pass successfully even if the
+functionality is not available.
- -- Hendrik Tews <hendrik at askra.de>, Fri, 17 May 2013 13:54:06 +0200
+ -- Hendrik Tews <hendrik at askra.de>, Mon, 9 Jan 2017 23:30:42 +0100
diff --git a/debian/changelog b/debian/changelog
index 52aa11a..1d6b415 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,26 @@
+hol-light (20170109-1) unstable; urgency=low
+
+ [ Mehdi Dogguy ]
+ * Update watch file
+
+ [ Hendrik Tews ]
+ * Imported Upstream version 20170109
+ with git hash f468686c09996f77ccfa98c30ba98f8db2c8cfd9
+ * update copyright, patches, README.Debian
+ * standards-version 3.9.8; update Vcs fields
+ * disable building the Mizarlight syntax extension (fails upstream with
+ OCaml 4.02 - already reported to John Harrison)
+ * clear exec bit fix on RichterHilbertAxiomGeometry/Topology.ml (fixed
+ upstream)
+ * add exec bit fixes for Help/HYP_TAC.doc,
+ RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml and
+ Multivariate/cvectors.ml
+ * don't install jar files in Proofrecording/tools
+ * add patch cd-holtest-parallel to fix current directory in parallel
+ test
+
+ -- Hendrik Tews <hendrik at askra.de> Mon, 09 Jan 2017 23:27:28 +0100
+
hol-light (20131026-1) unstable; urgency=low
* new upstream version revision 177 from 2013-10-26
diff --git a/debian/control b/debian/control
index 841b649..a917863 100644
--- a/debian/control
+++ b/debian/control
@@ -9,10 +9,10 @@ Build-Depends:
ocaml-base-nox,
dh-ocaml (>= 0.9~),
debhelper (>= 9.0.0)
-Standards-Version: 3.9.4
+Standards-Version: 3.9.8
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
-Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/hol-light.git
-Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/hol-light.git
+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
Package: hol-light
Architecture: any
diff --git a/debian/copyright b/debian/copyright
index 2602c35..a39d387 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,7 +1,7 @@
Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: hol-light
Upstream-Contact: John Harrison <johnh at ichips.intel.com>
-Source: svn repository at http://hol-light.googlecode.com/svn/trunk
+Source: git repository at https://github.com/jrh13/hol-light
Files: *
@@ -51,6 +51,95 @@ Comment: There is no license in subdirectory
HOL Light.
+Files: RichterHilbertAxiomGeometry/from_topology.ml
+Copyright: 1998-2014 John Harrison, 2010 Valentina Bruno
+License: BSD-2-clause
+Comment: There is no license in
+ RichterHilbertAxiomGeometry/from_topology.ml, but the file states
+ 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 Alexey Solovyev
+License: BSD-2-clause
+Comment: There is no license in all these subdirectories, but
+ Formal_ineqs/README.txt states that this directory is distributed
+ under the same license as HOL Light.
+
+
+Files: Formal_ineqs/jordan/*
+Copyright: 2010 Thomas C. Hales
+License: BSD-2-clause
+Comment: There is no license in subdirectory Formal_ineqs/jordan, but
+ Formal_ineqs/README.txt states that this directory is distributed
+ under the same license as HOL Light.
+
+
+Files: Formal_ineqs/verifier/interval_m/*
+Copyright: 2011, 2012 Thomas C. Hales and Alexey Solovyev
+License: BSD-2-clause
+Comment: There is no license in subdirectory
+ Formal_ineqs/verifier/interval_m, but Formal_ineqs/README.txt states
+ that this directory is distributed under the same license as HOL
+ Light.
+
+
+Files: Functionspaces/*
+Copyright: 2012-2016 Mohamed Yousri Mahmoud, Vincent Aravantinos
+ Hardware Verification Group, Concordia University
+License: BSD-2-clause
+Comment: There is no license in subdirectory Functionspaces, but
+ Functionspaces/README states that this directory is distributed under
+ the same license as HOL Light.
+
+
+Files: IEEE/*
+Copyright: 2014, Charlie Jacobsen, University of Utah
+License: BSD-2-clause
+Comment: There is no license in subdirectory IEEE, but
+ IEEE/README states that this directory is distributed
+ under the same license as HOL Light.
+
+Files: Library/q.ml
+Copyright: 2012-2013 Vincent Aravantinos, Hardware Verification Group,
+ Concordia University
+License: BSD-2-clause
+Comment: There is no license in Library/q.ml, but the file states that
+ it is distributed under the same license as HOL Light.
+
+
+Files: Multivariate/cvectors.ml
+Copyright: 2011-2013 Sanaz Khan Afshar & Vincent Aravantinos,
+ Hardware Verification Group, Concordia University
+License: BSD-2-clause
+Comment: There is no license in Multivariate/cvectors.ml, but the file
+ states that it is distributed under the same license as HOL Light.
+
+
+Files: Quaternions/*
+Copyright: 2014 Marco Maggesi
+License: BSD-2-clause
+Comment: See License in Quaternionic/COPYING.
+
+
+Files: impconv.ml
+Copyright: 2012-2013 Vincent Aravantinos, fortiss GmbH
+License: BSD-2-clause
+Comment: There is no license in impconv.ml, but the file states that
+ it is distributed under the same license as HOL Light.
+
+
+Files: metis.ml
+Copyright: 2001 Joe Hurd, 2004 Joe Leslie-Hurd,
+ 2014-2016 Michael Färber and Cezary Kaliszyk
+License: BSD-2-clause
+Comment: There is no license in metis.ml, but the file states that
+ it 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 8f6106d..29ab059 100644
--- a/debian/hol-light-source.exclude
+++ b/debian/hol-light-source.exclude
@@ -1,7 +1,6 @@
./debian
./.git
./.gitignore
-./.pc
./CHANGES
./LICENSE
./Makefile
@@ -9,4 +8,6 @@
./QUICK_REFERENCE.txt
./README
./VERYQUICK_REFERENCE.txt
-./RichterHilbertAxiomGeometry/miz3/hol-light-fonts.elc
+./Proofrecording/tools/detecteq.jar
+./Proofrecording/tools/nametheorems.jar
+./Quaternions/COPYING
diff --git a/debian/patches/cd-holtest-parallel.patch b/debian/patches/cd-holtest-parallel.patch
new file mode 100644
index 0000000..09d4d01
--- /dev/null
+++ b/debian/patches/cd-holtest-parallel.patch
@@ -0,0 +1,13 @@
+Description: cd for holtest_parallel because it works only in that directory
+Author: Hendrik Tews <hendrik at askra.de>
+--- a/holtest_parallel
++++ b/holtest_parallel
+@@ -20,6 +20,8 @@
+
+ set -e
+
++cd /usr/share/hol-light
++
+ if which hol-light > /dev/null ; then
+ hollight=hol-light
+ elif type ckpt > /dev/null; then
diff --git a/debian/patches/holtest-no-proof-recording.patch b/debian/patches/holtest-no-proof-recording.patch
index ec1361f..4aea1b1 100644
--- a/debian/patches/holtest-no-proof-recording.patch
+++ b/debian/patches/holtest-no-proof-recording.patch
@@ -2,7 +2,7 @@ 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
-@@ -172,7 +172,7 @@
+@@ -195,7 +195,7 @@
echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time $hollight)
# Build the proof-recording version of HOL
diff --git a/debian/patches/series b/debian/patches/series
index 0c7a73b..023f6f5 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
default-hollight-dir
holtest-no-proof-recording.patch
+cd-holtest-parallel.patch
diff --git a/debian/rules b/debian/rules
index 1813a08..2b692ac 100755
--- a/debian/rules
+++ b/debian/rules
@@ -30,7 +30,6 @@ override_dh_auto_clean:
override_dh_auto_build:
cp pa_j_3.1x_6.11.ml pa_j.ml
make
- make -C Mizarlight
INSTDIR:=debian/hol-light
.PHONY: override_dh_auto_install
@@ -38,7 +37,9 @@ 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/RichterHilbertAxiomGeometry/Topology.ml
+ 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
More information about the Pkg-ocaml-maint-commits
mailing list