rpms/prover9/F-9 import.log, NONE, 1.1 prover9-fedora.patch, NONE, 1.1 prover9-manpages.patch, NONE, 1.1 prover9-no-2.5isms.patch, NONE, 1.1 prover9.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2

Tue Aug 5 09:08:47 UTC 2008

Author: tcolles

Update of /cvs/pkgs/rpms/prover9/F-9
In directory cvs-int.fedora.redhat.com:/tmp/cvs-serv14405/F-9

Modified Files:
	.cvsignore sources 
Added Files:
	import.log prover9-fedora.patch prover9-manpages.patch 
	prover9-no-2.5isms.patch prover9.spec 
Log Message:
* Wed Jul 09 2008 Tim Colles <timc at inf.ed.ac.uk> - 200805a-4
- exclude ppc64 architecture as test2 fails

--- NEW FILE import.log ---
prover9-200805a-4:F-9:prover9-200805a-4.src.rpm:1217930805

prover9-fedora.patch:

--- NEW FILE prover9-fedora.patch ---
--- utilities/attack	2007-02-09 23:19:40.000000000 +0000
+++ utilities/attack.fedora	2008-01-31 14:48:50.000000000 +0000
@@ -1,5 +1,22 @@
 #!/usr/bin/python
 
+# Copyright (C) 2006, 2007 William McCune
+# 
+# This file is part of the LADR Deduction Library.
+# 
+# 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.
+
 # This script takes a Mace4 input file (the head) and a stream of
 # candidates.  It builds a list of models (M) of the candidates w.r.t.
 # the clauses in the head.
--- utilities/looper	2007-05-30 20:04:08.000000000 +0100
+++ utilities/looper.fedora	2008-01-31 14:48:56.000000000 +0000
@@ -1,5 +1,22 @@
 #!/usr/bin/python
 
+# Copyright (C) 2006, 2007 William McCune
+# 
+# This file is part of the LADR Deduction Library.
+# 
+# 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.
+
 # This script takes a (Prover9|Mace4) input file (the head), and
 # a stream of candidates.  For each candidate, it appends the
 # candidate to the head, and then runs (Prover9|Mace4).
--- utilities/prover9-mace4	2007-09-03 21:02:36.000000000 +0100
+++ utilities/prover9-mace4.fedora	2008-01-31 14:49:00.000000000 +0000
@@ -1,5 +1,22 @@
 #!/usr/bin/python
 
+# Copyright (C) 2006, 2007 William McCune
+# 
+# This file is part of the LADR Deduction Library.
+# 
+# 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.
+
 # This script takes a Prover9 input file and runs Prover9 and Mace4
 # in parallel.  If the one that finishes first finished with success,
 # its output is sent to stdout of this process.
--- README.first	2008-01-11 23:36:28.000000000 +0000
+++ README.first.fedora	2008-06-18 14:58:41.000000000 +0100
@@ -8,3 +8,58 @@
 
 for the HTML manual, examples, and updates.
 
+Copyright: 
+
+    utilities/gvizify: Copyright (C) 2007 David A. Wheeler
+    Other files: Copyright (C) 2006, 2007 William McCune
+
+License for utilities/gvizify:
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program 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 this program; if not, write to the Free Software
+    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+
+License for provers.src/white_black.h, provers.src/giv_select.c,
+provers.src/white_black.c, provers.src/giv_select.h, ladr/clause_eval.c,
+ladr/tmp/definitions.c, ladr/tmp/multiset.c, ladr/clause_eval.h,
+ladr/definitions.c, ladr/definitions.h, ladr/multiset.c, ladr/multiset.h:
+
+    The LADR Deduction Library is free software; you can redistribute it
+    and/or modify it under the terms of the GNU General Public License
+    as published by the Free Software Foundation; either version 2 of the
+    License, or (at your option) any later version.
+
+    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.
+
+License for all other files:
+
+    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.
+
--- copyright	1970-01-01 01:00:00.000000000 +0100
+++ copyright.fedora	2008-06-18 15:06:17.000000000 +0100
@@ -0,0 +1,52 @@
+This package was debianized by Peter Collingbourne <pcc03 at doc.ic.ac.uk> on
+Sat, 11 Aug 2007 23:22:34 +0100. It was converted for Fedora by Tim Colles
+<timc at inf.ed.ac.uk> on 18/06/2008.
+
+It was downloaded from <http://www.cs.unm.edu/~mccune/mace4/download/>
+
+Upstream Authors: 
+
+    William McCune <mccune at cs.unm.edu>
+    David A. Wheeler <dwheeler at dwheeler.com>
+
+Copyright: 
+
+    utilities/gvizify: Copyright (C) 2007 David A. Wheeler
+    Other files: Copyright (C) 2006, 2007 William McCune
+
+License for utilities/gvizify:
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program 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 this program; if not, write to the Free Software
+    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+
+License for all other files:
+
+    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 (C) 2008, Peter Collingbourne <pcc03 at doc.ic.ac.uk> and
+is licensed under the GPL, see `/usr/share/common-licenses/GPL'.

prover9-manpages.patch:

--- NEW FILE prover9-manpages.patch ---
diff -Naur LADR-2008-04A.upstream/manpages/clausefilter.1 LADR-2008-04A/manpages/clausefilter.1
--- LADR-2008-04A.upstream/manpages/clausefilter.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/clausefilter.1	2008-06-18 10:26:17.000000000 +0100
@@ -0,0 +1,43 @@
+.TH CLAUSEFILTER 1 "January 20, 2007"
+.SH NAME
+clausefilter - filter formulas with models
+.SH SYNOPSIS
+.B clausefilter
+.RI < interpretations-file >
+.RI < test >
+<
+.RI < formulas-file >
+>
+.RI < passing-formulas-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B clausefilter
+command.
+.PP
+Given a set of \fIinterpretations\fP, a \fItest\fP to perform, and a
+stream of \fIformulas\fP, \fBclausefilter\fP outputs the formulas
+that pass the test.
+.SH TESTS
+The following tests are available.
+.TP
+.B true_in_all
+Formula true in all interpretations.
+.TP
+.B true_in_some
+Formula true in some interpretation.
+.TP
+.B false_in_all
+Formula false in all interpretations.
+.TP
+.B false_in_some
+Formula false in some interpretation.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBclausefilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBclausefilter\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/clausetester.1 LADR-2008-04A/manpages/clausetester.1
--- LADR-2008-04A.upstream/manpages/clausetester.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/clausetester.1	2008-06-18 10:26:16.000000000 +0100
@@ -0,0 +1,29 @@
+.TH CLAUSETESTER 1 "January 20, 2007"
+.SH NAME
+clausetester - check formulas in models
+.SH SYNOPSIS
+.B clausetester
+.RI < interpretations-file >
+<
+.RI < formulas-file >
+>
+.RI < annotated-formulas-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B clausetester
+command.
+.PP
+This program takes a set of \fIinterpretations\fP and stream of
+\fIformulas\fP. For each formula, the interpretations in which the
+formula is true are shown, and at the end the number of formulas true
+in each interpretation is shown.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBclausetester\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBclausetester\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/interpfilter.1 LADR-2008-04A/manpages/interpfilter.1
--- LADR-2008-04A.upstream/manpages/interpfilter.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/interpfilter.1	2008-06-18 10:26:17.000000000 +0100
@@ -0,0 +1,43 @@
+.TH INTERPFILTER 1 "January 20, 2007"
+.SH NAME
+interpfilter - filter models with formulas
+.SH SYNOPSIS
+.B interpfilter
+.RI < formulas-file >
+.RI < test >
+<
+.RI < interpretations-file >
+>
+.RI < passing-interpretations-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B interpfilter
+command.
+.PP
+Given a set of \fIformulas\fP, a \fItest\fP to perform, and a
+stream of \fIinterpretations\fP, \fBinterpfilter\fP outputs the interpretations
+that pass the test.
+.SH TESTS
+The following tests are available.
+.TP
+.B all_true
+All formulas true in given interpretation.
+.TP
+.B some_true
+Some formula true in given interpretation.
+.TP
+.B all_false
+All formulas false in given interpretation.
+.TP
+.B some_false
+Some formula false in given interpretation.
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBinterpfilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBinterpfilter\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/interpformat.1 LADR-2008-04A/manpages/interpformat.1
--- LADR-2008-04A.upstream/manpages/interpformat.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/interpformat.1	2008-06-18 10:26:17.000000000 +0100
@@ -0,0 +1,65 @@
+.TH INTERPFORMAT 1 "January 20, 2007"
+.SH NAME
+interpformat \- tool for transforming
+.BR mace4 (1)
+models
+.SH SYNOPSIS
+.B interpformat
+.RI [ options ]
+.RI < transformation >
+\-f
+.I input-file
+>
+.I output-file
+.br
+.B interpformat
+.RI [ options ]
+.RI < transformation >
+<
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+The models (structures) in
+.BR mace4 (1)
+output files can be transformed in various ways with the program \fBinterpformat\fP.
+.SH TRANSFORMATIONS
+The transformations are listed here.
+.TP
+.B standard
+one line per operation
+.TP
+.B standard2
+standard, with binary operations in a square (default)
+.TP
+.B portable
+list of lists, suitable for parsing by Python, GAP, etc.
+.TP
+.B tabular
+as nice tables
+.TP
+.B raw
+similar to standard, but without punctuation
+.TP
+.B cooked
+as terms, e.g., f(0,1)=2
+.TP
+.B tex
+formatted for LaTeX
+.TP
+.B xml
+XML
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B output \fI<operations>
+Output only the listed \fIoperations\fP.
+.SH SEE ALSO
+.BR mace4 (1).
+.br
+Full documentation for \fBinterpformat\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBinterpformat\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/isofilter.1 LADR-2008-04A/manpages/isofilter.1
--- LADR-2008-04A.upstream/manpages/isofilter.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/isofilter.1	2008-06-18 10:26:16.000000000 +0100
@@ -0,0 +1,65 @@
+.TH ISOFILTER 1 "January 20, 2007"
+.SH NAME
+isofilter - removes isomorphic structures from
+.BR mace4 (1)
+models
+.SH SYNOPSIS
+.B isofilter
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.br
+.B isofilter0
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.br
+.B isofilter2
+.RI [ options ]
+<
+.I input-file
+>
+.I output-file
+.SH DESCRIPTION
+This manual page documents briefly the \fBisofilter\fP, \fBisofilter0\fP and \fBisofilter2\fP commands.
+.PP
+If
+.BR mace4 (1)
+produces more than one structure, some of them are very likely to be
+isomorphic to others. The program \fBisofilter\fP can be used to remove isomorphic
+structures.
+.SH ALGORITHM
+There are multiple \fBisofilter\fP variants providing alternative algorithms.
+.TP
+.B isofilter
+Uses Occurrence Profiles algorithm.
+.TP
+.B isofilter2
+Uses Canonical Forms algorithm.
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B ignore_constants
+Ignore all constants during the isomorphism tests.
+.TP
+.B check \fI<operations>
+Consider only the listed \fIoperations\fP in the isomorphism tests.
+.TP
+.B output \fI<operations>
+Output only the listed \fIoperations\fP.
+.TP
+.B wrap
+Enclose the resulting structures in \fBlist(interpretations). ... end_of_list.\fP
+.SH SEE ALSO
+.BR mace4 (1).
+.br
+Full documentation for \fBisofilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBisofilter\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/mace4.1 LADR-2008-04A/manpages/mace4.1
--- LADR-2008-04A.upstream/manpages/mace4.1	2007-12-31 04:43:54.000000000 +0000
+++ LADR-2008-04A/manpages/mace4.1	2008-06-18 10:26:16.000000000 +0100
@@ -80,7 +80,7 @@
 .br
 The original \fBmace4\fP manual, which can be downloaded at http://www.cs.unm.edu/~mccune/prover9/mace4.pdf
 .SH AUTHOR
-\fBmace4\fP ws written by William McCune <mccune at cs.unm.edu>
+\fBmace4\fP was written by William McCune <mccune at cs.unm.edu>
 .PP
 This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
 for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/prooftrans.1 LADR-2008-04A/manpages/prooftrans.1
--- LADR-2008-04A.upstream/manpages/prooftrans.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/prooftrans.1	2008-06-18 10:26:16.000000000 +0100
@@ -0,0 +1,73 @@
+.TH PROOFTRANS 1 "January 20, 2007"
+.SH NAME
+prooftrans - tool for transforming Prover9 proofs
+.SH SYNOPSIS
+.B prooftrans
+.RI [ parents_only ]
+.RI [ expand ]
+.RI [ renumber ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+xml
+.RI [ expand ]
+.RI [ renumber ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+ivy
+.RI [ renumber ]
+[\fI-f file\fP]
+.br
+.B prooftrans
+hints
+[\fI-label label\fP]
+.RI [ expand ]
+.RI [ striplabels ]
+[\fI-f file\fP]
+.SH DESCRIPTION
+This manual page documents briefly the
+.B prooftrans
+command.
+.PP
+\fBprooftrans\fP can extract proofs from
+.BR prover9 (1)
+output files and transform them in various ways.
+
+.SH OPTIONS
+A summary of options is included below.
+.TP
+.B renumber
+Renumber steps.
+.TP
+.B parents_only
+Simplify justifications by listing only parents.
+.TP
+.B expand
+Expand all steps, turning secondary justifications into explicit steps.
+.TP
+.B xml
+Produce proofs in XML.
+.TP
+.B ivy
+Produce proofs for checking by the IVY proof checker.
+.TP
+.B hints
+Produce hints for guiding subsequent searches.
+.TP
+.B \-label \fIlabel\fP
+Attach label attributes to the hint clauses consisting of the string \fIlabel\fP and a sequence number generated by prooftrans.
+.TP
+.B \-f \fIfile
+Take input from \fIfile\fP instead of from standard input.
+.SH SEE ALSO
+.BR prover9 (1).
+.br
+Full documentation for \fBprooftrans\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBprooftrans\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/prover9.1 LADR-2008-04A/manpages/prover9.1
--- LADR-2008-04A.upstream/manpages/prover9.1	2007-12-31 04:43:54.000000000 +0000
+++ LADR-2008-04A/manpages/prover9.1	2008-06-18 10:26:17.000000000 +0100
@@ -11,7 +11,7 @@
 .br
 .B prover9
 .RI [ options ]
--f
+\-f
 .I input-file
 >
 .I output-file
@@ -38,15 +38,15 @@
 .B \-t \fIn
 Constrain the search to last about \fIn\fP seconds.  For UNIX-like systems, the `user CPU' time is used.
 .TP
-.B \-f \fIfiles
-Take input from \fIfiles\fP instead of from standard input.
+.B \-f \fIfile
+Take input from \fIfile\fP instead of from standard input.
 .SH SEE ALSO
 .BR mace4 (1),
 .BR otter (1).
 .br
 On Debian systems, the manual is found in the \fIprover9-doc\fP package, at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
 .SH AUTHOR
-\fBprover9\fP ws written by William McCune <mccune at cs.unm.edu>
+\fBprover9\fP was written by William McCune <mccune at cs.unm.edu>
 .PP
 This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
 for the Debian project (but may be used by others).
diff -Naur LADR-2008-04A.upstream/manpages/prover9-apps.1 LADR-2008-04A/manpages/prover9-apps.1
--- LADR-2008-04A.upstream/manpages/prover9-apps.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/prover9-apps.1	2008-06-18 11:40:34.000000000 +0100
@@ -0,0 +1,17 @@
+.TH PROVER9-APPS 1 "June 18, 2008"
+.SH NAME
+prover9-apps \- undocumented Prover9 applications
+.SH DESCRIPTION
+Some programs in the \fBprover9-apps\fP package currently have no manual
+pages.  You can obtain documentation on some of these applications via the
+\fBprover9\fP manual, which is available via the package \fIprover9-doc\fP,
+at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+Alternatively invoking the application with the \fB-help\fP option may
+produce documentation.  Patches to add manual pages are welcome, and may
+be sent to the Debian package maintainer, whose details are listed below.
+.SH AUTHOR
+The applications were written by William McCune <mccune at cs.unm.edu>.
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others) and modified for Fedora
+by Tim Colles <timc at inf.ed.ac.uk>.
diff -Naur LADR-2008-04A.upstream/manpages/rewriter.1 LADR-2008-04A/manpages/rewriter.1
--- LADR-2008-04A.upstream/manpages/rewriter.1	1970-01-01 01:00:00.000000000 +0100
+++ LADR-2008-04A/manpages/rewriter.1	2008-06-18 10:26:17.000000000 +0100
@@ -0,0 +1,60 @@
+.de Sp \" Vertical space (when we can't use .PP)
+.if t .sp .5v
+.if n .sp
+..
+.de Vb \" Begin verbatim text
+.ft CW
+.nf
+.ne \\$1
+..
+.de Ve \" End verbatim text
+.ft R
+.fi
+..
+.TH REWRITER 1 "January 20, 2007"
+.SH NAME
+rewriter - demodulate terms
+.SH SYNOPSIS
+.B rewriter
+.RI < demodulators-file >
+<
+.RI < terms-file >
+>
+.RI < rewritten-terms-file >
+.SH DESCRIPTION
+This manual page documents briefly the
+.B rewriter
+command.
+.PP
+Rewrite a stream of \fIterms\fP with a list of \fIdemodulators\fP. The
+demodulators are used left-to-right as given, and they are not checked
+for termination.
+.SH SYNTAX
+The file of demodulators contains optional commands
+then a list of demodulators.  The commands can be used to
+declare infix operations and associativity/commutativity.
+Example file of demodulators:
+.Sp
+.Vb 10
+\&    op(400, infix, ^).
+\&    op(400, infix, v).
+\&    assoc_comm(^).
+\&    assoc_comm(v).
+\&    formulas(demodulators).
+\&    x ^ x = x.
+\&    x ^ (x v y) = x.
+\&    x v x = x.
+\&    x v (x ^ y) = x.
+\&    end_of_list.
+.Ve
+.Sp
+.SH SEE ALSO
+.BR prover9 (1),
+.BR mace4 (1).
+.br
+Full documentation for \fBrewriter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
+.SH AUTHOR
+\fBrewriter\fP was written by William McCune <mccune at cs.unm.edu>
+.PP
+This manual page was written by Peter Collingbourne <pcc03 at doc.ic.ac.uk>,
+for the Debian project (but may be used by others).

prover9-no-2.5isms.patch:

--- NEW FILE prover9-no-2.5isms.patch ---
diff -urNad ladr-0.0.200712~/utilities/gvizify ladr-0.0.200712/utilities/gvizify
--- ladr-0.0.200712~/utilities/gvizify	2008-01-24 20:57:07.000000000 +0000
+++ ladr-0.0.200712/utilities/gvizify	2008-01-24 20:58:24.000000000 +0000
@@ -208,7 +208,10 @@
   if options.multipage:
     print " page=\"%s\";" % (options.size,)
   else:
-    force="" if options.relax else "!"
+    if options.relax:
+      force=""
+    else:
+      force="!"
     print " size=\"%s%s\";" % (options.size, force)
   print " margin=\"%s\";" % (options.margin,)
   if options.command != "":


--- NEW FILE prover9.spec ---
%define upstreamname LADR
%define upstreamver 2008-05A

Name:           prover9
Version:        200805a
Release:        4%{?dist}
Summary:        Thereom Prover and Countermodel Generator

Group:          Applications/Productivity
# All files are GPLv2 except utilities/gvizify which is GPLv2+
License:        GPLv2 and GPLv2+
URL:            http://www.cs.unm.edu/~mccune/prover9/
Source0:        http://www.cs.unm.edu/~mccune/prover9/download/%{upstreamname}-%{upstreamver}.tar.gz
Source1:        http://www.cs.unm.edu/~mccune/prover9/manual/%{name}-manual-%{upstreamver}.tar.gz
Patch0:         %{name}-no-2.5isms.patch
Patch1:         %{name}-manpages.patch
Patch2:         %{name}-fedora.patch
BuildRoot:      %(mktemp -ud %{_tmppath}/%{name}-%{version}-%{release}-XXXXXX)
BuildRequires:  libtool

# Fails test2 in check section on ppc64 architecture
ExcludeArch:    ppc64

%description 
This package provides the Prover9 resolution/paramodulation theorem prover
and the Mace4 countermodel generator.

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.

The program Mace4 searches for finite structures satisfying first-order and
equational statements, the same kind of statement that Prover9 accepts. If
the statement is the denial of some conjecture, any structures found by
Mace4 are counterexamples to the conjecture.

Mace4 can be a valuable complement to Prover9, looking for counterexamples
before (or at the same time as) using Prover9 to search for a proof. It can
also be used to help debug input clauses and formulas for Prover9. 


%package devel
Group:          Development/Libraries
Summary:        LADR Deduction Library - Development Files
Requires:       %{name} = %{version}-%{release}
Provides:       %{name}-static = %{version}-%{release}

%description devel
LADR (Library for Automated Deduction Research) is a library for use in
constructing theorem provers. Among other useful routines it provides
facilities for applying inference rules such as resolution and
paramodulation to clauses. LADR is used by the prover9 theorem prover,
and by the mace4 countermodel generator.

This package provides development support files and static development
libraries for LADR.


%package apps
Group:          Applications/Productivity
Summary:        LADR Deduction Library - Miscellaneous Applications
Requires:       %{name} = %{version}-%{release}

%description apps
LADR (Library for Automated Deduction Research) is a library for use in
constructing theorem provers. Among other useful routines it provides
facilities for applying inference rules such as resolution and
paramodulation to clauses. LADR is used by the prover9 theorem prover,
and by the mace4 countermodel generator.

This package provides miscellaneous LADR applications.


%package doc
Group:          Documentation
Summary:        LADR Deduction Library - Documentation
Requires:       %{name} = %{version}-%{release}

%description doc
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. 


%prep
%setup -q -n %{upstreamname}-%{upstreamver} -a 1
%patch0 -p1
%patch1 -p1
%patch2 -p0


%build
make all CFLAGS="%{optflags}"


%install
%{__rm} -rf %{buildroot}
%{__install} -p -d -m 0755 %{buildroot}%{_bindir}
for f in bin/*; do
  %{__install} -p -m 0755 $f %{buildroot}%{_bindir}/%{name}-`basename $f`
done
%{__rm} %{buildroot}%{_bindir}/%{name}-proof3fo.xsl
%{__rm} %{buildroot}%{_bindir}/%{name}-prover9-mace4
%{__rm} %{buildroot}%{_bindir}/%{name}-test_clause_eval
%{__mv} %{buildroot}%{_bindir}/%{name}-mace4 %{buildroot}%{_bindir}/mace4
%{__mv} %{buildroot}%{_bindir}/%{name}-prover9 %{buildroot}%{_bindir}/prover9
# manpages
%{__install} -p -d -m 0755 %{buildroot}%{_mandir}/man1
%{__install} -p -m 0644 manpages/interpformat.1 %{buildroot}%{_mandir}/man1/%{name}-interpformat.1
%{__install} -p -m 0644 manpages/isofilter.1 %{buildroot}%{_mandir}/man1/%{name}-isofilter.1
%{__ln_s} %{name}-isofilter.1.gz %{buildroot}%{_mandir}/man1/%{name}-isofilter0.1.gz
%{__ln_s} %{name}-isofilter.1.gz %{buildroot}%{_mandir}/man1/%{name}-isofilter2.1.gz
%{__install} -p -m 0644 manpages/prooftrans.1 %{buildroot}%{_mandir}/man1/%{name}-prooftrans.1
%{__install} -p -m 0644 manpages/mace4.1 %{buildroot}%{_mandir}/man1
%{__install} -p -m 0644 manpages/prover9.1 %{buildroot}%{_mandir}/man1
# header files and libraries for devel package
%{__install} -p -d -m 0755 %{buildroot}%{_includedir}/ladr
%{__install} -p -m 0644 ladr/*.h %{buildroot}%{_includedir}/ladr
%{__install} -p -d -m 0755 %{buildroot}%{_libdir}
%{__install} -p -m 0644 ladr/lib*.a %{buildroot}%{_libdir}
# manpages for apps package
%{__install} -p -m 0644 manpages/clausefilter.1 %{buildroot}%{_mandir}/man1/%{name}-clausefilter.1
%{__install} -p -m 0644 manpages/clausetester.1 %{buildroot}%{_mandir}/man1/%{name}-clausetester.1
%{__install} -p -m 0644 manpages/interpfilter.1 %{buildroot}%{_mandir}/man1/%{name}-interpfilter.1
%{__install} -p -m 0644 manpages/rewriter.1 %{buildroot}%{_mandir}/man1/%{name}-rewriter.1
%{__install} -p -m 0644 manpages/prover9-apps.1 %{buildroot}%{_mandir}/man1
# fix incorrect permission on one of the example scripts
chmod 0644 apps.examples/run-all


%clean
%{__rm} -rf %{buildroot}


%check
make test1 test2 test3


%files
%defattr(-,root,root,-)
%doc Changelog COPYING TODO copyright mace4.examples prover9.examples
%{_bindir}/mace4
%{_bindir}/prover9
%{_bindir}/%{name}-interpformat
%{_bindir}/%{name}-isofilter
%{_bindir}/%{name}-isofilter0
%{_bindir}/%{name}-isofilter2
%{_bindir}/%{name}-prooftrans
%{_mandir}/man1/mace4.1.gz
%{_mandir}/man1/prover9.1.gz
%{_mandir}/man1/%{name}-interpformat.1.gz
%{_mandir}/man1/%{name}-isofilter.1.gz
%{_mandir}/man1/%{name}-isofilter0.1.gz
%{_mandir}/man1/%{name}-isofilter2.1.gz
%{_mandir}/man1/%{name}-prooftrans.1.gz


%files devel
%defattr(-,root,root,-)
%doc ladr/html
%{_includedir}/ladr
%{_libdir}/lib*.a


%files apps
%defattr(-,root,root,-)
%doc apps.examples apps.src/README.directproof
%{_bindir}/%{name}-attack
%{_bindir}/%{name}-autosketches4
%{_bindir}/%{name}-clausefilter
%{_bindir}/%{name}-clausetester
%{_bindir}/%{name}-directproof
%{_bindir}/%{name}-dprofiles
%{_bindir}/%{name}-fof-prover9
%{_bindir}/%{name}-get_givens
%{_bindir}/%{name}-get_interps
%{_bindir}/%{name}-get_kept
%{_bindir}/%{name}-gvizify
%{_bindir}/%{name}-idfilter
%{_bindir}/%{name}-interpfilter
%{_bindir}/%{name}-ladr_to_tptp
%{_bindir}/%{name}-latfilter
%{_bindir}/%{name}-looper
%{_bindir}/%{name}-miniscope
%{_bindir}/%{name}-mirror-flip
%{_bindir}/%{name}-newauto
%{_bindir}/%{name}-newsax
%{_bindir}/%{name}-olfilter
%{_bindir}/%{name}-perm3
%{_bindir}/%{name}-renamer
%{_bindir}/%{name}-rewriter
%{_bindir}/%{name}-sigtest
%{_bindir}/%{name}-tptp_to_ladr
%{_bindir}/%{name}-unfast
%{_bindir}/%{name}-upper-covers
%{_mandir}/man1/prover9-apps.1.gz
%{_mandir}/man1/%{name}-clausefilter.1.gz
%{_mandir}/man1/%{name}-clausetester.1.gz
%{_mandir}/man1/%{name}-interpfilter.1.gz
%{_mandir}/man1/%{name}-rewriter.1.gz


%files doc
%defattr(-,root,root,-)
%doc %{name}-manual-%{upstreamver}/*.{html,css,gif}


%changelog
* Wed Jul 09 2008 Tim Colles <timc at inf.ed.ac.uk> - 200805a-4
- exclude ppc64 architecture as test2 fails

* Tue Jul 08 2008 Tim Colles <timc at inf.ed.ac.uk> - 200805a-3
- make -apps require base package instead of other way around
- added check section to run built-in tests
- fix perms on static library
- fix perms on example script
- use name prefix and install all binaries in /usr/bin
- add name prefix to manpages, drop symlinks for missing manpages

* Fri Jun 06 2008 Tim Colles <timc at inf.ed.ac.uk> - 200805a-2
- dropped libtoolize patch and stopped shipping shared libraries
- changed build to use rpm optflags
- added -p flag to preserve timestamps
- install all binaries except mace4/prover9 to /usr/lib/prover9/bin

* Fri Jun 06 2008 Tim Colles <timc at inf.ed.ac.uk> - 200805a-1
- renamed as prover9
- redesigned borrowing heavily from the Debian package by Peter Collingbourne
- included patches from Debian package by Peter Collingbourne
- added documentation source/package
- updated version

* Thu Jan 10 2008 Tim Colles <timc at inf.ed.ac.uk> - 200712-1
- initial version


Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/prover9/F-9/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- .cvsignore	4 Aug 2008 18:45:31 -0000	1.1
+++ .cvsignore	5 Aug 2008 09:08:17 -0000	1.2
@@ -0,0 +1,2 @@
+LADR-2008-05A.tar.gz
+prover9-manual-2008-05A.tar.gz


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/prover9/F-9/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- sources	4 Aug 2008 18:45:31 -0000	1.1
+++ sources	5 Aug 2008 09:08:17 -0000	1.2
@@ -0,0 +1,2 @@
+73cba4f17bee85f85c579a7dd8c7f099  LADR-2008-05A.tar.gz
+a544ecd335070e5ef24c84f7eef936f7  prover9-manual-2008-05A.tar.gz


