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 c1db1aeb87dcd65331ec722c659ac1739834ca69 Author: Hendrik Tews <hend...@askra.de> Date: Tue Oct 24 22:10:35 2017 +0200 new upstream version 20170917 and related changes * Imported upstream version 20170917 with git hash 4c464bee35551ce3db2ef42b51bc19f5bf638e78 * 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 * minor change in control file - Flyspeck is completed * update copyright file - a number of files have unclear license --- debian/changelog | 12 +++++++++ debian/compat | 2 +- debian/control | 6 ++--- debian/copyright | 35 ++++++++++--------------- debian/patches/camlp5-7.patch | 23 ---------------- debian/patches/holtest-no-proof-recording.patch | 2 +- debian/patches/series | 1 - debian/rules | 2 +- 8 files changed, 32 insertions(+), 51 deletions(-) diff --git a/debian/changelog b/debian/changelog index f6978d5..9c76245 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,15 @@ +hol-light (20170917-1) unstable; urgency=medium + + * Imported upstream version 20170917 + with git hash 4c464bee35551ce3db2ef42b51bc19f5bf638e78 + * 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 + * minor change in control file - Flyspeck is completed + * update copyright file - a number of files have unclear license + + -- Hendrik Tews <hend...@askra.de> Tue, 24 Oct 2017 22:08:25 +0200 + hol-light (20170109-2) unstable; urgency=medium [ Hendrik Tews ] diff --git a/debian/compat b/debian/compat index ec63514..f599e28 100644 --- a/debian/compat +++ b/debian/compat @@ -1 +1 @@ -9 +10 diff --git a/debian/control b/debian/control index ee0d6bb..3afc9f0 100644 --- a/debian/control +++ b/debian/control @@ -8,8 +8,8 @@ Build-Depends: camlp5 (>= 7.01), ocaml-base-nox, dh-ocaml (>= 0.9~), - debhelper (>= 9.0.0) -Standards-Version: 3.9.8 + debhelper (>= 10.0.0) +Standards-Version: 4.1.0 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 @@ -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 Flyspeck project, which aims at the + arithmetic as well as for the Flyspeck project, which aimed at the formalization of Tom Hales' proof of the Kepler conjecture. diff --git a/debian/copyright b/debian/copyright index a39d387..0aa3642 100644 --- a/debian/copyright +++ b/debian/copyright @@ -6,7 +6,7 @@ Source: git repository at https://github.com/jrh13/hol-light Files: * Copyright: 1998 University of Cambridge - 1998-2012 John Harrison <jo...@ichips.intel.com> and others + 1998-2017 John Harrison <jo...@ichips.intel.com> and others License: BSD-2-clause @@ -63,30 +63,13 @@ 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 +Copyright: 2012-2014 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 + Formal_ineqs/README.md 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 @@ -103,6 +86,13 @@ 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: IsabelleLight/* +Copyright: 2009-2015, Petros Papapanagiotou, Jacques Fleuriot, + University of Edinburgh +License: missing/unclear + + Files: Library/q.ml Copyright: 2012-2013 Vincent Aravantinos, Hardware Verification Group, Concordia University @@ -120,7 +110,7 @@ Comment: There is no license in Multivariate/cvectors.ml, but the file Files: Quaternions/* -Copyright: 2014 Marco Maggesi +Copyright: 2014-2016 Marco Maggesi License: BSD-2-clause Comment: See License in Quaternionic/COPYING. @@ -142,6 +132,7 @@ Comment: There is no license in metis.ml, but the file states that Files: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml Copyright: 2002-2006 INRIA + 1998-2017 John Harrison <jo...@ichips.intel.com> and others License: LGPL-2 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Library General Public @@ -169,7 +160,9 @@ Comment: These files do not contain a license. They do contain Files: pa_j_3.1* + pa_j_4.xx_7.xx.ml Copyright: 2007-2010 INRIA + 1998-2017 John Harrison <jo...@ichips.intel.com> and others License: BSD-3-clause Copyright (c) 2007-2012, INRIA (Institut National de Recherches en Informatique et Automatique). All rights reserved. diff --git a/debian/patches/camlp5-7.patch b/debian/patches/camlp5-7.patch deleted file mode 100644 index 03bfe11..0000000 --- a/debian/patches/camlp5-7.patch +++ /dev/null @@ -1,23 +0,0 @@ -Description: quick fix for camlp5-7.01 -Author: Hendrik Tews <hend...@askra.de> ---- a/pa_j_3.1x_6.11.ml -+++ b/pa_j_3.1x_6.11.ml -@@ -320,6 +320,9 @@ - | ExLmd loc x1 x2 x3 → - let loc = floc loc in - ExLmd loc x1 (reloc_module_expr floc sh x2) (self x3) -+ | ExLop loc x1 x2 → -+ let loc = floc loc in -+ ExLop loc (reloc_module_expr floc sh x1) (self x2) - | ExMat loc x1 x2 → - let loc = floc loc in - ExMat loc (self x1) -@@ -356,7 +359,7 @@ - | ExRpl loc x1 x2 → - let loc = floc loc in - ExRpl loc (vala_map (option_map self) x1) -- ((fun (loc, x1) → (floc loc, x1)) x2) -+ ((vala_map (fun (loc, x1) → (floc loc, x1))) x2) - | ExSeq loc x1 → - let loc = floc loc in - ExSeq loc (vala_map (List.map self) x1) diff --git a/debian/patches/holtest-no-proof-recording.patch b/debian/patches/holtest-no-proof-recording.patch index 4aea1b1..6641c4b 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 <hend...@askra.de> --- a/holtest +++ b/holtest -@@ -195,7 +195,7 @@ +@@ -197,7 +197,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 7c5871b..023f6f5 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,4 +1,3 @@ default-hollight-dir holtest-no-proof-recording.patch cd-holtest-parallel.patch -camlp5-7.patch diff --git a/debian/rules b/debian/rules index 2b692ac..f641860 100755 --- a/debian/rules +++ b/debian/rules @@ -28,7 +28,7 @@ override_dh_auto_clean: .PHONY: override_dh_auto_build override_dh_auto_build: - cp pa_j_3.1x_6.11.ml pa_j.ml + cp pa_j_4.xx_7.xx.ml pa_j.ml make INSTDIR:=debian/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