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 <[email protected]> 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 <[email protected]>, Fri, 17 May 2013 13:54:06 +0200 + -- Hendrik Tews <[email protected]>, 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 <[email protected]> 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 <[email protected]> -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 <[email protected]> +--- 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 <[email protected]> --- 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 _______________________________________________ Pkg-ocaml-maint-commits mailing list [email protected] http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
