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
