The package rpms/prover9.git has added or updated architecture specific content in its spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s): https://src.fedoraproject.org/cgit/rpms/prover9.git/commit/?id=172bd8841cced....
Change: -ExcludeArch: ppc64
Thanks.
Full change: ============
commit 172bd8841cced4143170b5017f704c042cc27eed Author: Miro Hronok miro@hroncok.cz Date: Mon May 20 11:32:01 2019 +0200
Orphaned for 6+ weeks
diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 95d79a7..0000000 --- a/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -LADR-2008-05A.tar.gz -prover9-manual-2008-05A.tar.gz -LADR-2009-11A.tar.gz -prover9-manual-2009-11A.tar.gz diff --git a/dead.package b/dead.package new file mode 100644 index 0000000..5204a84 --- /dev/null +++ b/dead.package @@ -0,0 +1 @@ +Orphaned for 6+ weeks diff --git a/format-fix.patch b/format-fix.patch deleted file mode 100644 index e880d4c..0000000 --- a/format-fix.patch +++ /dev/null @@ -1,48 +0,0 @@ ---- ladr/fastparse.c.orig 2015-07-27 10:15:11.423522124 -0500 -+++ ladr/fastparse.c 2015-07-27 10:16:48.745891297 -0500 -@@ -183,8 +183,8 @@ - Pos = 0; - t = fast_parse(s); - if (s[Pos] != '.') { -- fprintf(stderr, s); -- fprintf(stdout, s); -+ fprintf(stderr, "%s", s); -+ fprintf(stdout, "%s", s); - fatal_error("fast_read_term, term ends before period."); - } - return t; ---- mace4.src/print.c.orig 2015-07-27 10:23:08.719183948 -0500 -+++ mace4.src/print.c 2015-07-27 10:25:31.202292819 -0500 -@@ -111,12 +111,12 @@ - printf(s1, i); - printf("\n ---"); - for (i = 0; i < n; i++) -- printf(s2); -+ printf("%s", s2); - printf("\n "); - for (i = 0; i < n; i++) { - int v = f1_val(p->base, i); - if (v < 0) -- printf(s3); -+ printf("%s", s3); - else - printf(s1, v); - } -@@ -134,7 +134,7 @@ - printf(s1, i); - printf("\n --+"); - for (i = 0; i < n; i++) -- printf(s2); -+ printf("%s", s2); - printf("\n"); - - for (i = 0; i < n; i++) { -@@ -142,7 +142,7 @@ - for (j = 0; j < n; j++) { - int v = f2_val(p->base, i, j); - if (v < 0) -- printf(s3); -+ printf("%s", s3); - else - printf(s1, v); - } diff --git a/prover9-fedora.patch b/prover9-fedora.patch deleted file mode 100644 index 5e78ea6..0000000 --- a/prover9-fedora.patch +++ /dev/null @@ -1,191 +0,0 @@ ---- 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@doc.ic.ac.uk on -+Sat, 11 Aug 2007 23:22:34 +0100. It was converted for Fedora by Tim Colles -+timc@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@cs.unm.edu -+ David A. Wheeler dwheeler@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@doc.ic.ac.uk and -+is licensed under the GPL, see `/usr/share/common-licenses/GPL'. diff --git a/prover9-manpages.patch b/prover9-manpages.patch deleted file mode 100644 index 1e3e89b..0000000 --- a/prover9-manpages.patch +++ /dev/null @@ -1,470 +0,0 @@ -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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+\fBmace4\fP was written by William McCune mccune@cs.unm.edu - .PP - This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu -+\fBprover9\fP was written by William McCune mccune@cs.unm.edu - .PP - This manual page was written by Peter Collingbourne pcc03@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@cs.unm.edu. -+.PP -+This manual page was written by Peter Collingbourne pcc03@doc.ic.ac.uk, -+for the Debian project (but may be used by others) and modified for Fedora -+by Tim Colles timc@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@cs.unm.edu -+.PP -+This manual page was written by Peter Collingbourne pcc03@doc.ic.ac.uk, -+for the Debian project (but may be used by others). diff --git a/prover9-no-2.5isms.patch b/prover9-no-2.5isms.patch deleted file mode 100644 index e439f99..0000000 --- a/prover9-no-2.5isms.patch +++ /dev/null @@ -1,15 +0,0 @@ -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 != "": diff --git a/prover9.spec b/prover9.spec deleted file mode 100644 index 7e4e570..0000000 --- a/prover9.spec +++ /dev/null @@ -1,289 +0,0 @@ -%define upstreamname LADR -%define upstreamver 2009-11A - -Name: prover9 -Version: 200911a -Release: 17%{?dist} -Summary: Theorem Prover and Countermodel Generator - -# 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/%%7Bupstreamname%7D-%%7Bupstr... -Source1: http://www.cs.unm.edu/~mccune/prover9/manual/%%7Bname%7D-manual-%%7Bupstream... -Patch0: %{name}-no-2.5isms.patch -Patch1: %{name}-manpages.patch -Patch2: %{name}-fedora.patch -Patch3: format-fix.patch -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 -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 -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 -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 -%patch3 -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 - - - -%check -make test1 test2 test3 - - -%files -%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 -%doc ladr/html -%{_includedir}/ladr -%{_libdir}/lib*.a - - -%files apps -%doc apps.examples apps.src/README.directproof -%{_bindir}/%{name}-attack -%{_bindir}/%{name}-autosketches4 -%{_bindir}/%{name}-clausefilter -%{_bindir}/%{name}-clausetester -%{_bindir}/%{name}-complex -%{_bindir}/%{name}-directproof -%{_bindir}/%{name}-dprofiles -%{_bindir}/%{name}-fof-prover9 -%{_bindir}/%{name}-gen_trc_defs -%{_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}-test_complex -%{_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 -%doc %{name}-manual-%{upstreamver}/*.{html,css,gif} - - -%changelog -* Sat Feb 02 2019 Fedora Release Engineering releng@fedoraproject.org - 200911a-17 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Fri Jul 13 2018 Fedora Release Engineering releng@fedoraproject.org - 200911a-16 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Fri Feb 09 2018 Fedora Release Engineering releng@fedoraproject.org - 200911a-15 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Thu Aug 03 2017 Fedora Release Engineering releng@fedoraproject.org - 200911a-14 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild - -* Thu Jul 27 2017 Fedora Release Engineering releng@fedoraproject.org - 200911a-13 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Sat Feb 11 2017 Fedora Release Engineering releng@fedoraproject.org - 200911a-12 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Thu Feb 04 2016 Fedora Release Engineering releng@fedoraproject.org - 200911a-11 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Mon Jul 27 2015 Bruno Wolff III bruno@wolff.to - 200911a-10 -- Fix format string warning - -* Thu Jun 18 2015 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild - -* Sun Aug 17 2014 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild - -* Sat Jun 07 2014 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild - -* Sun Aug 04 2013 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild - -* Thu Feb 14 2013 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild - -* Sat Jul 21 2012 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Sat Jan 14 2012 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_17_Mass_Rebuild - -* Wed Feb 09 2011 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200911a-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild - -* Sat Jul 24 2010 David A. Wheeler dwheeler@dwheeler.com - 200911a-1 -- Update to upstream version 200911a. -- Adds prover9-complex, prover9-gen_trc_defs, prover9-test_complex. -- Fix spelling in RPM summary. - -* Sun Jul 26 2009 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200805a-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild - -* Thu Feb 26 2009 Fedora Release Engineering rel-eng@lists.fedoraproject.org - 200805a-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild - -* Wed Jul 09 2008 Tim Colles timc@inf.ed.ac.uk - 200805a-4 -- exclude ppc64 architecture as test2 fails - -* Tue Jul 08 2008 Tim Colles timc@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@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@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@inf.ed.ac.uk - 200712-1 -- initial version diff --git a/sources b/sources deleted file mode 100644 index 68ed5f1..0000000 --- a/sources +++ /dev/null @@ -1,2 +0,0 @@ -ab409f31ecbb4410b1c7d75deadea2c6 LADR-2009-11A.tar.gz -23fbb9c6b3cbfbb2b893fb788e248a29 prover9-manual-2009-11A.tar.gz
arch-excludes@lists.fedoraproject.org