--- prover9-manual-0.0.200902a.orig/debian/install +++ prover9-manual-0.0.200902a/debian/install @@ -0,0 +1,3 @@ +*.html usr/share/doc/prover9-doc/html +*.css usr/share/doc/prover9-doc/html +*.gif usr/share/doc/prover9-doc/html --- prover9-manual-0.0.200902a.orig/debian/copyright +++ prover9-manual-0.0.200902a/debian/copyright @@ -0,0 +1,33 @@ +This package was debianized by Peter Collingbourne on +Sat, 11 Aug 2007 22:13:16 +0100. + +It was downloaded from + +Upstream Author: + + William McCune + +Copyright: + + Copyright (C) 2006, 2007 William McCune + +License: + + The LADR Deduction Library is free software; you can redistribute it + and/or modify it under the terms of the GNU General Public License, + version 2. + + The LADR Deduction 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 General Public License for more details. + + You should have received a copy of the GNU General Public License + along with the LADR Deduction Library; if not, write to the Free Software + Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. + +On Debian systems, the complete text of the GNU General +Public License, version 2 can be found in `/usr/share/common-licenses/GPL-2'. + +The Debian packaging is Copyright (C) 2009 Peter Collingbourne +and is licensed under the GPL, see `/usr/share/common-licenses/GPL-2'. --- prover9-manual-0.0.200902a.orig/debian/watch +++ prover9-manual-0.0.200902a/debian/watch @@ -0,0 +1,4 @@ +version=3 + +# note: not Y2.1K compliant +opts="uversionmangle=s/^(....)-(..)(.?)$/'0.0.'.$1.$2.lc($3)/e;s/^(..)(..)(.?)$/'0.0.20'.$2.$1.lc($3)/e" http://www.cs.unm.edu/~mccune/mace4/manual-examples.html manual/prover9-manual-([0-9]{4}-[0-9]{2}[A-Z]?|[0-9]{4}[A-Z]?).tar.gz --- prover9-manual-0.0.200902a.orig/debian/docs +++ prover9-manual-0.0.200902a/debian/docs @@ -0,0 +1 @@ +finalbook/finalbook.pdf --- prover9-manual-0.0.200902a.orig/debian/examples +++ prover9-manual-0.0.200902a/debian/examples @@ -0,0 +1,110 @@ +2inverter.in +2inverter.out +andrews.in +andrews.out +andrews.out2 +assoc-comm.clauses +BA2.in +BA2.interps +BA2.interps2 +BA2.interps3 +BA2.interps4 +BA2.interps5 +BA4.in +BA4.out +BA-Sheffer.demods +bool-ring.demods +bool-ring.in +bool-ring.out +cabbages.in +cabbages.out +easy.hints +easy.in +easy.out +group.demods +group-terms.in +group-terms.out +hard-hints.out +hard.in +hard.out +interp3.dtd +interp3.xsl +jugs.in +jugs.out +kenken6.in +kenken6.out +list.in +list.out +LT-82-2.in +LT-82-2-interp.in +LT-82-2-interp.out +LT-82-2.out +LT-port.in +LT-port.out +LT-port.out2 +MOL-cand.238 +MOL-cand.296 +MOL.in +MOL.interps +MOL.interps2 +non-MOL-OML.interps +olsax.in +olsax.out +port.py +proof3.dtd +PUZ031-1.in +PUZ031-1.out +PUZ031-1.out2 +PUZ031-1.tptp +qg4-ac.interps +qg4.interps +queens1.in +queens1.out +queens2.in +queens2.out +queens3.in +queens3.out +RBA-2.in +RBA-2q.tptp +RBA-2.tptp +redeclare.in +redeclare.out +ring41.in +ring41.out +send-money.in +send-money.out +subset.in +subset_trans_expand.in +subset_trans_expand.out +subset_trans.in +subset_trans.out +subset_trans.out2 +subset_trans.out3 +subset_trans.out4 +subset_trans.proof1 +subset_trans.proof2 +subset_trans.proof3 +subset_trans.proof4 +subset_trans.proof5.xml +subset_trans.proof6 +subset_trans.proof7 +subset_trans.proof8 +trans.in +uc-18.interps +uc-hunt.clauses +uc-hunt.out +weight_test.in +weight_test.out +x2.cooked +x2.in +x2.mace4.out +x2.portable +x2.prover9.out +x2.raw +x2.standard +x2.standard2 +x2.tabular +x2.tex +x2.xml +zebra2.in +zebra2.out --- prover9-manual-0.0.200902a.orig/debian/changelog +++ prover9-manual-0.0.200902a/debian/changelog @@ -0,0 +1,64 @@ +prover9-manual (0.0.200902a-1) unstable; urgency=low + + * New upstream release. + * debian/examples: updated + * debian/control: new Standards-Version + + -- Peter Collingbourne Sun, 15 Mar 2009 00:53:52 +0000 + +prover9-manual (0.0.200811a-1) unstable; urgency=low + + * New upstream release. + * debian/examples: updated + * debian/control: Vcs-Bzr uses nosmart+http protocol + * debian/control, debian/copyright: changed maintainer email address + (again) + * debian/copyright: changed year to 2009, corrected expression of + copyright, refer to GPL-2 explicitly + * debian/install: eliminated brace expansion + + -- Peter Collingbourne Tue, 17 Feb 2009 02:20:39 +0000 + +prover9-manual (0.0.200809a-1) unstable; urgency=low + + * New upstream release. + * debian/control, debian/copyright: changed maintainer email address + + -- Peter Collingbourne Sat, 13 Sep 2008 21:14:40 +0100 + +prover9-manual (0.0.200806a-1) unstable; urgency=low + + * New upstream release. + * debian/control: new Standards-Version + + -- Peter Collingbourne Sun, 29 Jun 2008 04:57:20 +0100 + +prover9-manual (0.0.200805a-1) unstable; urgency=low + + * New upstream release. + * debian/control: added DM-Upload-Allowed: yes + + -- Peter Collingbourne Mon, 12 May 2008 19:34:36 +0100 + +prover9-manual (0.0.200804a-1) unstable; urgency=low + + * New upstream release. + * debian/watch: added support for new version numbering scheme + + -- Peter Collingbourne Tue, 8 Apr 2008 19:40:46 +0100 + +prover9-manual (0.0.200712-2) unstable; urgency=low + + * debian/rules: removed bashism (closes: #471753) + * debian/doc-base: changed Section to a valid value + + -- Peter Collingbourne Thu, 20 Mar 2008 20:37:05 +0000 + +prover9-manual (0.0.200712-1) unstable; urgency=low + + * Initial release (Closes: #437944) + * syntax.html: replaced literal < and > symbols with entities in order to + prevent htmldoc from failing + + -- Peter Collingbourne Mon, 14 Jan 2008 20:24:28 +0000 + --- prover9-manual-0.0.200902a.orig/debian/control +++ prover9-manual-0.0.200902a/debian/control @@ -0,0 +1,23 @@ +Source: prover9-manual +Section: doc +Priority: optional +Maintainer: Peter Collingbourne +Build-Depends: debhelper (>= 5), dpatch +Build-Depends-Indep: htmldoc +Standards-Version: 3.8.1 +Vcs-Bzr: nosmart+http://bzr.debian.org/collab-maint/prover9-manual/unstable/ +DM-Upload-Allowed: yes +Homepage: http://www.cs.unm.edu/~mccune/mace4/ + +Package: prover9-doc +Architecture: all +Suggests: prover9, ladr4-apps, python +Description: documentation for Prover9 and associated programs + Prover9 is an automated theorem prover for first-order and equational + logic. It is a successor of the Otter prover. Prover9 uses the + inference techniques of ordered resolution and paramodulation with + literal selection. + . + This package provides documentation for Prover9, Mace4 and other + associated programs. + --- prover9-manual-0.0.200902a.orig/debian/doc-base +++ prover9-manual-0.0.200902a/debian/doc-base @@ -0,0 +1,15 @@ +Document: prover9-doc +Title: Prover9 Manual +Author: William McCune +Abstract: This manual describes the + usage of Prover9, Mace4 and other + programs based upon the LADR deduction + library. +Section: Science/Mathematics + +Format: HTML +Index: /usr/share/doc/prover9-doc/html/index.html +Files: /usr/share/doc/prover9-doc/html/*.html + +Format: PDF +Files: /usr/share/doc/prover9-doc/finalbook.pdf.gz --- prover9-manual-0.0.200902a.orig/debian/rules +++ prover9-manual-0.0.200902a/debian/rules @@ -0,0 +1,68 @@ +#!/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 + +include /usr/share/dpatch/dpatch.make + +EGFILES = $(shell cat debian/examples) +EGREGEX = $(shell echo $(EGFILES) | sed -e 's/ /\\|/g ; s/\./\\./g') + +build: build-stamp +build-stamp: patch + dh_testdir + + # Rebuild the pdf to update it and point it to the correct example directory + mkdir -p finalbook + cp *.html *.css *.gif finalbook/ + sed -i 's#href="\($(EGREGEX)\)"#href="examples/\1"#g' finalbook/*.html + ./setup_book < finalbook/nav.html > finalbook/make_book + chmod +x finalbook/make_book + cd finalbook && ./make_book + + touch $@ + +clean: clean-patched unpatch +clean-patched: + dh_testdir + dh_testroot + rm -f build-stamp + + rm -rf finalbook + + dh_clean + +install: build + dh_testdir + dh_testroot + dh_clean -k + dh_installdirs + +# Build architecture-independent files here. +binary-indep: build install + dh_testdir + dh_testroot + dh_install + sed -i 's#href="\($(EGREGEX)\)"#href="../examples/\1"#g' debian/prover9-doc/usr/share/doc/prover9-doc/html/*.html + dh_installchangelogs + dh_installdocs + dh_compress + dh_installexamples + dh_fixperms + dh_installdeb + dh_gencontrol + dh_md5sums + dh_builddeb + +# Build architecture-dependent files here. +binary-arch: build install +# We have nothing to do by default. + +binary: binary-indep binary-arch +.PHONY: build clean binary-indep binary-arch binary install --- prover9-manual-0.0.200902a.orig/debian/compat +++ prover9-manual-0.0.200902a/debian/compat @@ -0,0 +1 @@ +5 --- prover9-manual-0.0.200902a.orig/debian/build-eg-list +++ prover9-manual-0.0.200902a/debian/build-eg-list @@ -0,0 +1,8 @@ +#!/bin/sh + +# Development script used to build list of example files +# An example file is taken as a file satisfying certain +# constraints which is linked to by an html file +# Usage: (from package root directory) debian/build-eg-list > debian/examples + +find * -maxdepth 0 -type f -not -iname '*.html' -not -iname '*.gif' -not -iname '*.css' -not -iname '*.pdf' -exec fgrep -qi 'href="{}"' *.html \; -print --- prover9-manual-0.0.200902a.orig/debian/dirs +++ prover9-manual-0.0.200902a/debian/dirs @@ -0,0 +1 @@ +usr/share/doc/prover9-doc/html --- prover9-manual-0.0.200902a.orig/debian/patches/00list +++ prover9-manual-0.0.200902a/debian/patches/00list @@ -0,0 +1 @@ +01-entities.dpatch --- prover9-manual-0.0.200902a.orig/debian/patches/01-entities.dpatch +++ prover9-manual-0.0.200902a/debian/patches/01-entities.dpatch @@ -0,0 +1,41 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## 01-entities.dpatch by +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Replaced literal < and > symbols with entities in order to prevent +## DP: htmldoc from failing. + +@DPATCH@ +diff -urNad prover9-manual-0.0.200712~/syntax.html prover9-manual-0.0.200712/syntax.html +--- prover9-manual-0.0.200712~/syntax.html 2008-01-25 21:46:20.000000000 +0000 ++++ prover9-manual-0.0.200712/syntax.html 2008-01-25 21:47:10.000000000 +0000 +@@ -228,10 +228,10 @@ + Meaning Connective Example + negation - (-p) + disjunction | (p | q | r) +-conjunction & (p & q & r) +-implication -> (p -> q) +-backward implication <- (p <- q) +-equivalence <-> (p <-> q) ++conjunction & (p & q & r) ++implication -> (p -> q) ++backward implication <- (p <- q) ++equivalence <-> (p <-> q) + universal quantification all (all x all y p(x,y)) + existential quantification exists (exists x exists y p(x,y)) + +@@ -466,10 +466,10 @@ + false $F + negation - + disjunction | +-conjunction & +-implication -> +-backward_implication <- +-equivalence <-> ++conjunction & ++implication -> ++backward_implication <- ++equivalence <-> + universal_quantification all + existential_quantification exists + equality =