-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
The nmudiff script fails on this package for some reason, so the NMU patch is
attached. The package has been uploaded to the DELAYED/3 queue. Please email
me if you would like the package removed from queue before it enters the
archive.
Thank you,
Tony
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAkvqNsAACgkQpdwBkPlyvgMZ9QCcDT9hJdQuF3GWI9L6RxyDc3FL
gVQAni/4pkHCYjYZodyKniVUY+mn//8S
=3E6F
-----END PGP SIGNATURE-----
diff -Nru minlog-4.0.99.20100221/debian/changelog minlog-4.0.99.20100221/debian/changelog
--- minlog-4.0.99.20100221/debian/changelog 2010-02-21 06:44:18.000000000 -0800
+++ minlog-4.0.99.20100221/debian/changelog 2010-05-11 03:36:50.000000000 -0700
@@ -1,3 +1,34 @@
+minlog (4.0.99.20100221-5.1) unstable; urgency=low
+
+ [ Jari Aalto ]
+ * Non-maintainer upload.
+ - Move to packaging format "3.0 (quilt)" due to patch.
+ * debian/compat
+ - Update to 7.
+ * debian/control
+ - Remove EOL whitespaces.
+ - (Build-Depends): Change obsolete mzscheme to plt-scheme.
+ Patch tanks to Hideki Yamane (Debian-JP) <henr...@debian.or.jp>
+ (FTBFS; Closes: #577343). Add emacs23. Remove emacs21.
+ Update to debhelper 7.1.
+ - (Depends): Add ${misc:Depends}.
+ - (Homepage): New field.
+ - (Standards-Version): Update to 3.8.4.
+ * debian/copyright
+ - Update old FSF addresses to point to URL.
+ - Point to GPL-2. Remove EOL whitespaces.
+ * debian/doc-base
+ - New file.
+ * debian/rules
+ - Remove EOL whitespaces.
+ - (install): Update dh_clean to dh_prep.
+ * debian/source/format
+ - New file.
+ * debian/watch
+ - New file.
+
+ -- Jari Aalto <jari.aa...@cante.net> Tue, 11 May 2010 13:36:50 +0300
+
minlog (4.0.99.20100221-5) unstable; urgency=low (high for users of mzsccheme)
* Closes: #570235 due to incompatibility between mzscheme and r5rs
@@ -16,31 +47,31 @@
minlog (4.0.99.20080304-4) unstable; urgency=low
* CVS snapshot
-
+
-- Freiric Barral <bar...@math.lmu.de> Tue, 04 Mar 2008 11:21:04 +0100
minlog (4.0.99-4) unstable; urgency=low
* Added missing copyright notices.
* Initial upload closes: #406186
-
+
-- Freiric Barral <bar...@math.lmu.de> Fri, 12 Oct 2007 13:55:13 +0100
minlog (4.0.99-3) unstable; urgency=low
- * XEmacs does not work with Minlog. So recommend either emacs21 or
+ * XEmacs does not work with Minlog. So recommend either emacs21 or
emacs22 (though the latter is not available yet).
-
+
-- Freiric Barral <bar...@math.lmu.de> Wed, 3 Nov 2006 19:28:10 +0100
minlog (4.0.99-2) unstable; urgency=low
* Use debhelper v4 and therefore put everything into debian/minlog
-
+
-- Freiric Barral <bar...@math.lmu.de> Wed, 2 Nov 2006 19:27:10 +0100
minlog (4.0.99-1) unstable; urgency=low
* Initial release
-
+
-- Freiric Barral <bar...@math.lmu.de> Wed, 1 Nov 2006 19:26:10 +0100
diff -Nru minlog-4.0.99.20100221/debian/compat minlog-4.0.99.20100221/debian/compat
--- minlog-4.0.99.20100221/debian/compat 2010-02-20 08:47:52.000000000 -0800
+++ minlog-4.0.99.20100221/debian/compat 2010-05-08 11:04:13.000000000 -0700
@@ -1 +1 @@
-4
+7
diff -Nru minlog-4.0.99.20100221/debian/control minlog-4.0.99.20100221/debian/control
--- minlog-4.0.99.20100221/debian/control 2010-02-20 08:47:52.000000000 -0800
+++ minlog-4.0.99.20100221/debian/control 2010-05-08 11:49:06.000000000 -0700
@@ -2,28 +2,29 @@
Section: math
Priority: optional
Maintainer: Freiric Barral <bar...@math.lmu.de>
-Build-Depends: debhelper (>= 4.0.0), mzscheme, texlive (>= 2007-11)
-Standards-Version: 3.7.2
+Build-Depends: debhelper (>= 7.1), plt-scheme, texlive (>= 2007-11)
+Standards-Version: 3.8.4
+Homepage: http://www.minlog-system.de
Package: minlog
-Architecture: all
-Depends: mzscheme | guile
-Recommends: emacs22 | emacs21 | emacsen
+Architecture: all
+Depends: ${misc:Depends}, plt-scheme | guile
+Recommends: emacs23 | emacs22 | emacsen
Suggests: proofgeneral-minlog, quack-el
Description: Proof assistant based on first order natural deduction calculus
- intended to reason about computable functionals, using minimal
- rather than classical or intuitionistic logic. The main motivation
- behind MINLOG is to exploit the proofs-as-programs paradigm for
- program development and program verification. Proofs are in fact
- treated as first class objects which can be normalized. If a formula
- is existential then its proof can be used for reading off an instance
- of it, or changed appropriately for program development by proof
- transformation. To this end MINLOG is equipped with tools to extract
- functional programs directly from proof terms. This also applies to
- non-constructive proofs, using a refined A-translation. The system
- is supported by automatic proof search and normalization by
+ intended to reason about computable functionals, using minimal
+ rather than classical or intuitionistic logic. The main motivation
+ behind MINLOG is to exploit the proofs-as-programs paradigm for
+ program development and program verification. Proofs are in fact
+ treated as first class objects which can be normalized. If a formula
+ is existential then its proof can be used for reading off an instance
+ of it, or changed appropriately for program development by proof
+ transformation. To this end MINLOG is equipped with tools to extract
+ functional programs directly from proof terms. This also applies to
+ non-constructive proofs, using a refined A-translation. The system
+ is supported by automatic proof search and normalization by
evaluation as an efficient term rewriting device.
.
- Minlog can be used with ProofGeneral, which allows proofs to be
- edited using emacs and xemacs. This requires the proofgeneral-minlog
+ Minlog can be used with ProofGeneral, which allows proofs to be
+ edited using emacs and xemacs. This requires the proofgeneral-minlog
package to be installed.
diff -Nru minlog-4.0.99.20100221/debian/copyright minlog-4.0.99.20100221/debian/copyright
--- minlog-4.0.99.20100221/debian/copyright 2010-02-20 08:47:52.000000000 -0800
+++ minlog-4.0.99.20100221/debian/copyright 2010-05-08 11:07:10.000000000 -0700
@@ -3,7 +3,7 @@
It was downloaded from http://www.minlog-system.de/
-Here is a list of files followed by their respective copyright holder
+Here is a list of files followed by their respective copyright holder
and license:
@@ -39,10 +39,10 @@
lr-dvr.scm, lalr.scm:
-Copyright (C) 1984, 1989, 1990 Free Software Foundation, Inc.
- (for the Bison source code translated in Scheme)
-Copyright (C) 1996 Dominique Boucher
- (for the translation in Scheme)
+Copyright (C) 1984, 1989, 1990 Free Software Foundation, Inc.
+ (for the Bison source code translated in Scheme)
+Copyright (C) 1996 Dominique Boucher
+ (for the translation in Scheme)
lalr.scm and lr-dvr.scm are free software; you can redistribute them
and/or modify them under the terms of the GNU General Public License
@@ -51,11 +51,10 @@
distributed in the hope that they will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
-for more details. You should have received a copy of the GNU General
-Public License along with lalr.scm; see the file COPYING. If not,
-write to the Free Software Foundation, 675 Mass Ave, Cambridge, MA
-02139, USA. Dominique Boucher -- Universite de Montreal Send
-questions, comments or suggestions to bouch...@iro.umontreal.ca
+for more details. You should have received a copy of the GNU General Public
+License along with this program. If not, see <http://www.gnu.org/licenses/>
+Dominique Boucher -- Universite de Montreal Send questions, comments
+or suggestions to bouch...@iro.umontreal.ca
bussproofs.sty. Version 0.6c:
@@ -73,12 +72,12 @@
Copyright Holder: Helmut Schwichtenberg (schwi...@math.lmu.de) and
members of the logic group (lo...@math.lmu.de)
- minlog mail is min...@mathematik.uni-muenchen.de
+ minlog mail is min...@mathematik.uni-muenchen.de
License:
You are free to distribute this software under the terms of the GNU
-General Public License.
+General Public License.
On Debian systems, the complete text of the GNU General Public License
-can be found in the file `/usr/share/common-licenses/GPL'.
+can be found in the file "/usr/share/common-licenses/GPL-2".
diff -Nru minlog-4.0.99.20100221/debian/minlog.doc-base minlog-4.0.99.20100221/debian/minlog.doc-base
--- minlog-4.0.99.20100221/debian/minlog.doc-base 1969-12-31 16:00:00.000000000 -0800
+++ minlog-4.0.99.20100221/debian/minlog.doc-base 2010-05-08 11:25:54.000000000 -0700
@@ -0,0 +1,11 @@
+Document: doc-base
+Title: First order natural deduction calculus
+Author: Aubrey Jaffer
+Abstract: MINLOG is based on first order natural deduction calculus and
+ it is intended to reason about computable functionals, using minimal
+ rather than classical or intuitionistic logic.
+Section: Science/Mathematics
+
+Format: PDF
+Files: /usr/share/doc/minlog/tutor.pdf /usr/share/doc/minlog/mlcf.pdf /usr/share/doc/minlog/ref.pdf /usr/share/doc/minlog/reflection_manual.pdf
+
diff -Nru minlog-4.0.99.20100221/debian/rules minlog-4.0.99.20100221/debian/rules
--- minlog-4.0.99.20100221/debian/rules 2010-02-20 08:47:52.000000000 -0800
+++ minlog-4.0.99.20100221/debian/rules 2010-05-08 11:30:02.000000000 -0700
@@ -1,10 +1,5 @@
#!/usr/bin/make -f
# -*- makefile -*-
-# Sample debian/rules that uses debhelper.
-# This file was originally written by Joey Hess and Craig Small.
-# As a special exception, when this file is copied by dh-make into a
-# dh-make output file, you may use that output file without restriction.
-# This special exception was added by Craig Small in version 0.37 of dh-make.
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
@@ -30,7 +25,7 @@
build: build-stamp
-build-stamp: configure-stamp
+build-stamp: configure-stamp
dh_testdir
# Add here commands to compile the package.
@@ -47,12 +42,12 @@
# Add here commands to clean up after the build process.
$(MAKE) clean
- dh_clean
+ dh_clean
install: build
dh_testdir
dh_testroot
- dh_clean -k
+ dh_prep
dh_installdirs
# Add here commands to install the package into debian/minlog.
@@ -69,7 +64,7 @@
dh_installman debian/minlog.1
dh_link
dh_strip
- dh_compress -Xminlog/examples
+ dh_compress -Xminlog/examples -X.pdf
dh_fixperms
dh_installdeb
dh_shlibdeps
diff -Nru minlog-4.0.99.20100221/debian/source/format minlog-4.0.99.20100221/debian/source/format
--- minlog-4.0.99.20100221/debian/source/format 1969-12-31 16:00:00.000000000 -0800
+++ minlog-4.0.99.20100221/debian/source/format 2010-05-08 11:08:16.000000000 -0700
@@ -0,0 +1 @@
+3.0 (quilt)
diff -Nru minlog-4.0.99.20100221/debian/watch minlog-4.0.99.20100221/debian/watch
--- minlog-4.0.99.20100221/debian/watch 1969-12-31 16:00:00.000000000 -0800
+++ minlog-4.0.99.20100221/debian/watch 2010-05-11 03:36:28.000000000 -0700
@@ -0,0 +1,2 @@
+version=3
+http://www.minlog-system.de .*minlog-([\d.]+).tar.gz
