[Pkg-ocaml-maint-commits] [SCM] hol-light packaging branch, master, updated. upstream/20120322-17-gacba4c3

Tue Apr 24 21:45:04 UTC 2012

The following commit has been merged in the master branch:
commit acba4c3a41c04c0067e1616b92d6a3c82c698843
Author: Hendrik Tews <hendrik at askra.de>
Date:   Tue Apr 24 23:20:48 2012 +0200

    fix copyright file
    - also add a patch to fix the broken Makefile

diff --git a/.pc/applied-patches b/.pc/applied-patches
index cd58477..54d37bf 100644
--- a/.pc/applied-patches
+++ b/.pc/applied-patches
@@ -1,3 +1,4 @@
 default-hollight-dir
 adapt-holtest-for-debian.patch
 holtest-no-proof-recording.patch
+pa-j-makefile-fix.patch
diff --git a/.pc/adapt-holtest-for-debian.patch/.timestamp b/.pc/pa-j-makefile-fix.patch/.timestamp
similarity index 100%
copy from .pc/adapt-holtest-for-debian.patch/.timestamp
copy to .pc/pa-j-makefile-fix.patch/.timestamp
diff --git a/Makefile b/.pc/pa-j-makefile-fix.patch/Makefile
similarity index 100%
copy from Makefile
copy to .pc/pa-j-makefile-fix.patch/Makefile
diff --git a/Makefile b/Makefile
index cff489d..97035f9 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,7 @@ OCAML_BINARY_VERSION=`ocamlc -version | cut -c3`
 CAMLP5_BINARY_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`
 CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6`
 
-pa_j.ml: pa_j_3.04.ml pa_j_3.06.ml pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx.ml; \
+pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx.ml; \
         if test ${OCAML_BINARY_VERSION} = "0" ; \
         then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \
         else if test ${CAMLP5_VERSION} = "6.02.1" ; \
diff --git a/debian/changelog b/debian/changelog
index 786ac24..ddc0bf9 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,5 +1,5 @@
-hol-light (20120322-1) unstable; urgency=low
+hol-light (20120423-1) unstable; urgency=low
 
   * Initial release (Closes: #663754)
 
- -- Hendrik Tews <hendrik at askra.de>  Fri, 16 Mar 2012 10:24:24 +0100
+ -- Hendrik Tews <hendrik at askra.de>  Tue, 24 Apr 2012 20:40:39 +0200
diff --git a/debian/copyright b/debian/copyright
index 628d9f5..c939b00 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -3,72 +3,89 @@ Upstream-Name: hol-light
 Upstream-Contact: John Harrison <johnh at ichips.intel.com>
 Source: svn repository at http://hol-light.googlecode.com/svn/trunk
 
+
 Files: *
 Copyright: 1998 University of Cambridge
            1998-2012 John Harrison <johnh at ichips.intel.com> and others
 License: BSD-2-clause
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are
- met:
- .
-  o Redistributions of source code must retain the above copyright
-    notice, this list of conditions and the following disclaimer.
- .
-  o Redistributions in binary form must reproduce the above copyright
-    notice, this list of conditions and the following disclaimer in the
-    documentation and/or other materials provided with the
-    distribution.
- .
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
- "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
- LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
- A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
- HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
- SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
- LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 
 Files: Permutation/*
 Copyright: 2005-2007 Marco Maggesi <maggesi at math.unifi.it>
 License: BSD-2-clause
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are
- met:
- .
-  o Redistributions of source code must retain the above copyright
-    notice, this list of conditions and the following disclaimer.
- .
-  o Redistributions in binary form must reproduce the above copyright
-    notice, this list of conditions and the following disclaimer in the
-    documentation and/or other materials provided with the
-    distribution.
- .
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
- "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
- LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
- A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
- HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
- SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
- LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 Comment: There is no license in subdirectory Permutation, but
- Permutation/DOC.txt states that all files under the same license terms
- as HOL Light.
+ Permutation/DOC.txt states that all files are distributed under the
+ same license terms as HOL Light.
+
 
 Files: Unity/*
 Copyright: 1989-2008 by Flemming Andersen
-License: ??
+License: BSD-2-clause
+Comment: There is no license in subdirectory Unity, but Unity/README
+ 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
+ This library is free software; you can redistribute it and/or
+ modify it under the terms of the GNU Library General Public
+ License as published by the Free Software Foundation; either
+ version 2 of the License, or (at your option) any later version.
+ .
+ This library is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ Library General Public License for more details.
+ .
+ You should have received a copy of the GNU Library General Public
+ License along with this library; if not, write to the Free Software
+ Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301,
+ USA.
+ .
+ On Debian systems, the full text of the GNU Library General Public
+ License version 2 can be found in the file
+ `/usr/share/common-licenses/LGPL-2'.
+Comment: These files do not contain a license. They do contain
+ significant portions of original camlp4 code, copied from the
+ indicated OCaml release. Since OCaml 3.07, camlp4 is part of "the
+ Library" and distributed under LGPL-2, therefore also these files
+ fall under LGPL-2.
+
+
+Files: pa_j_3.1*
+Copyright: 2007-2010 INRIA
+License: BSD-3-clause
+ Copyright (c) 2007-2012, INRIA (Institut National de Recherches en
+ Informatique et Automatique). All rights reserved.
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions are met:
+ .
+     * Redistributions of source code must retain the above copyright
+       notice, this list of conditions and the following disclaimer.
+     * Redistributions in binary form must reproduce the above copyright
+       notice, this list of conditions and the following disclaimer in the
+       documentation and/or other materials provided with the distribution.
+     * Neither the name of INRIA, nor the names of its contributors may be
+       used to endorse or promote products derived from this software without
+       specific prior written permission.
+ .
+ THIS SOFTWARE IS PROVIDED BY INRIA AND CONTRIBUTORS ``AS IS'' AND
+ ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
+ THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL INRIA AND
+ CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
+ USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
+ OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ SUCH DAMAGE.
+Comment: These files do not contain a license. They do contain a
+ significant portion of orginial Camlp5 source code, which is
+ distributed under the BSD-3-clause license.
 
-Files: pa_j*
-Copyright: 2007-2010 INRIA 
-License: no?
 
 Files: Jordan/float.ml
 Copyright: Thomas C. Hales
@@ -117,6 +134,8 @@ License: Expat
 Files: debian/*
 Copyright: 2012 Hendrik Tews <hendrik at askra.de>
 License: BSD-2-clause
+
+License: BSD-2-clause
  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions are
  met:
diff --git a/debian/patches/pa-j-makefile-fix.patch b/debian/patches/pa-j-makefile-fix.patch
new file mode 100644
index 0000000..a195604
--- /dev/null
+++ b/debian/patches/pa-j-makefile-fix.patch
@@ -0,0 +1,13 @@
+Description: fix dependency on non-present pa_j files
+Author: Hendrik Tews <hendrik at askra.de>
+--- a/Makefile
++++ b/Makefile
+@@ -51,7 +51,7 @@
+ CAMLP5_BINARY_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`
+ CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6`
+ 
+-pa_j.ml: pa_j_3.04.ml pa_j_3.06.ml pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx.ml; \
++pa_j.ml: pa_j_3.07.ml pa_j_3.08.ml pa_j_3.09.ml pa_j_3.1x_5.xx.ml pa_j_3.1x_6.xx.ml; \
+         if test ${OCAML_BINARY_VERSION} = "0" ; \
+         then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \
+         else if test ${CAMLP5_VERSION} = "6.02.1" ; \
diff --git a/debian/patches/series b/debian/patches/series
index cd58477..54d37bf 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1,4 @@
 default-hollight-dir
 adapt-holtest-for-debian.patch
 holtest-no-proof-recording.patch
+pa-j-makefile-fix.patch
diff --git a/debian/rules b/debian/rules
index f0a42b2..bba8111 100755
--- a/debian/rules
+++ b/debian/rules
@@ -23,6 +23,11 @@ export DH_OPTIONS
 %:
 	dh $@ --with ocaml
 
+.PHONY: override_dh_auto_clean
+override_dh_auto_clean:
+	dh_auto_clean
+	make -C Mizarlight clean
+
 .PHONY: override_dh_auto_build
 override_dh_auto_build:
 	cp pa_j_3.1x_6.02.2.ml pa_j.ml

-- 
hol-light packaging

