reinit the tree, so we can have metadata

4 files changed, 610 insertions, 0 deletions

diff --git a/sci-mathematics/prover9/Manifest b/sci-mathematics/prover9/Manifest
new file mode 100644
index 000000000000..c3edc553c262
--- /dev/null
+++ b/sci-mathematics/prover9/Manifest
@@ -0,0 +1,7 @@
+AUX LADR-2009-11A-manpages.patch 13832 SHA256 d9ecfc1a476d1e06a4b83dc3a96a57c3cf78943571e910ea4be420ce5a255371 SHA512 4c9f862b33d7b6b33b5e4a82b38418c6ae41b7adae565d376cc741608eb989e3846c1e98589dea62f7cadeb0b1f0f5814afe95ee6cf0da63c6961620d8b2677c WHIRLPOOL ce25b003f4ea4262e2431437e840d188ac73bab08f2397d7869badb9adfd783e58fb09d01ddaee983fc4b9078b716cb04958125df800984bdb486f11badd39a6
+DIST LADR-2009-11A-makefile.patch.xz 4300 SHA256 7340ec2ce439a6ed039d7077a417ca5d81ad3acce0b174e96469e8ebad274adf SHA512 c1d2e27d991036af24a29deb4401fbf9687415d2a37bebabb9cfc77d8672e0804d974f92cbd7b8e16c0a0c10b75831847f7b8ddb94244d7e632de7b1be5081f1 WHIRLPOOL 15401ed0b9edafb3841bed7c1c270d8a38544470abf87abd9b70b9eb0aa194d7296146e88b797a568aff7e557a118bfc2ee40d5a5c8ae6a426902db51e11c0ae
+DIST LADR-2009-11A.tar.gz 1795750 SHA256 c32bed5807000c0b7161c276e50d9ca0af0cb248df2c1affb2f6fc02471b51d0 SHA512 f26d3713eb2ba809fb3d55ce179e9d91555ab9166e075aa0843bafe57ce00f153cfed178b61993d4fd471655840e4f40775d75dac9fb5242a67e5d59c970dfc7 WHIRLPOOL 6e6abd1a5c7bfc988fb693eeea08bdfba77c9badea3d4a77764efcb9ee16c36b372241fbf4d4dead911cabf9a03721988f334977379da47d04b4320bae257fad
+EBUILD prover9-2009.11a.ebuild 2501 SHA256 e5f7881d48c8dd70eee7e6ef300f58b5de2e453387556ac10529da3d4e90224f SHA512 9fcd42d72dbb823fd2a71064416fb7d5565c2104aaf78274d3986b605e5182ff5bc09f706191c5441d64392e7de6ae779d33afcb2ca7df6d5476cbcdd01724f0 WHIRLPOOL 4c8ecc39cd6a8e4272d851ac1344e2990e3c0eed1cd01b5182c217791711065063cc9dde5d4838bf9f8922959d624d8390282e4eed8e33c7835ad2d06687d368
+MISC ChangeLog 2506 SHA256 11eea2ed086a936c3bd01d4e215e126b1b934f3685c8788e10388974b7231962 SHA512 0107cff7c26b34a4a2a67f53b8c0dfda01a1ae334b8aac71993b1e6b595e5a83b4a2927c6475856a670c9ef5265870e0024273f44e310f1947196c451b3e5c86 WHIRLPOOL c466e09a66b45b300aed7b389f800cb4bc679707317d83ab54aa4c21a39db38a9d5f7f7b914f95979f4c9cd96f46652651b86be45daf83c89bac228b7573f128
+MISC ChangeLog-2015 1093 SHA256 accadcaa67650488616b1d397e357382252040095843ec6afbaa9d290ae3a92f SHA512 65e8adfe60b4ccb86fbb60990162ee057bf56afc88e0a10f0263325560cf6d5bb71191d76104ff7651aaef39caa8d84c975ad8cef0bafa42416019868be97b6b WHIRLPOOL 5f7bd44aaff1b05be2fa420667c5727c42f86d640eceac4112131ca9b760dd39a65614ac2215f9fb429bd71200e66c09fed67f33686defa64c3e720a84e4b91d
+MISC metadata.xml 643 SHA256 4b9cacae281684bc0e74de2c98f56c897a723a936f5b48e51158896ab72eee7b SHA512 c3160f8aadceb5f065af9c5f14e9fe904b270bba1cf7781d33c39dca4f2641d61123839b93c4d7ad38139e8fc4c221016fe444cbfd7ddc99ea224090fccd7078 WHIRLPOOL d16c76482900958caa7db7be34c00ca77dfb7b86b141189245fd112ff9cb4b002a0dad0c6b7689e36a6620ec715cad91ce89b643e7bb31615dec2f051877009a
diff --git a/sci-mathematics/prover9/files/LADR-2009-11A-manpages.patch b/sci-mathematics/prover9/files/LADR-2009-11A-manpages.patch
new file mode 100644
index 000000000000..6e2324a6a390
--- /dev/null
+++ b/sci-mathematics/prover9/files/LADR-2009-11A-manpages.patch
@@ -0,0 +1,466 @@
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/clausefilter.1	2012-01-07 19:30:44.311801364 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/clausetester.1	2012-01-07 19:30:44.312801386 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/interpfilter.1	2012-01-07 19:30:44.312801386 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/interpformat.1	2012-01-07 19:30:44.313801403 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/isofilter.1	2012-01-07 19:30:44.313801403 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- LADR-2009-11A-orig/manpages/mace4.1	2007-12-31 15:43:54.000000000 +1100
++++ LADR-2009-11A/manpages/mace4.1	2012-01-07 19:55:18.746508266 +1100
+@@ -76,11 +76,11 @@
+ .SH SEE ALSO
+ .BR prover9 (1).
+ .br
+-Full documentation for \fBmace4\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.
++Full documentation for \fBmace4\fP is found in the \fBprover9\fP manual, available on Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/index.html\fP.
+ .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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/prooftrans.1	2012-01-07 19:30:44.314801424 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- LADR-2009-11A-orig/manpages/prover9.1	2007-12-31 15:43:54.000000000 +1100
++++ LADR-2009-11A/manpages/prover9.1	2012-01-07 19:54:30.928968388 +1100
+@@ -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.
++On Gentoo systems, the manual is found at \fI/usr/share/doc/prover9-2009.11a/html/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).
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/prover9-apps.1	2012-01-07 19:30:44.315801449 +1100
+@@ -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
++at \fI/usr/share/doc/prover9-2009.11a/html/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>.
+--- /dev/null	2012-01-07 09:10:22.797165727 +1100
++++ LADR-2009-11A/manpages/rewriter.1	2012-01-07 19:30:44.315801449 +1100
+@@ -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 Gentoo systems at \fI/usr/share/doc/prover9-2009.11a/html/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/sci-mathematics/prover9/metadata.xml b/sci-mathematics/prover9/metadata.xml
new file mode 100644
index 000000000000..7ff123879bf7
--- /dev/null
+++ b/sci-mathematics/prover9/metadata.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+  <maintainer type="person">
+    <email>gienah@gentoo.org</email>
+    <name>Mark Wright</name>
+  </maintainer>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription lang="en">
+  Prover9 and Mace4 Prover9 is an automated theorem prover for
+  first-order and equational logic, and Mace4 searches for finite
+  models and counterexamples. Prover9 is the successor of the
+  Otter prover. 
+</longdescription>
+</pkgmetadata>
diff --git a/sci-mathematics/prover9/prover9-2009.11a.ebuild b/sci-mathematics/prover9/prover9-2009.11a.ebuild
new file mode 100644
index 000000000000..56c2ad3a4132
--- /dev/null
+++ b/sci-mathematics/prover9/prover9-2009.11a.ebuild
@@ -0,0 +1,119 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=5
+
+inherit eutils toolchain-funcs versionator
+
+MY_PN="LADR"
+typeset -u MY_PV
+MY_PV=$(replace_all_version_separators '-')
+MY_P="${MY_PN}-${MY_PV}"
+
+DESCRIPTION="Automated theorem prover for first-order and equational logic"
+HOMEPAGE="http://www.cs.unm.edu/~mccune/mace4/"
+SRC_URI="
+	http://www.cs.unm.edu/~mccune/mace4/download/${MY_P}.tar.gz
+	https://dev.gentoo.org/~jlec/distfiles/${MY_PN}-2009-11A-makefile.patch.xz"
+
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+LICENSE="GPL-2"
+IUSE="examples"
+
+PATCHES=(
+	"${WORKDIR}"/${MY_PN}-2009-11A-makefile.patch
+	"${FILESDIR}"/${MY_PN}-2009-11A-manpages.patch
+	)
+
+S="${WORKDIR}/${MY_P}/"
+
+src_prepare() {
+	MAKEOPTS+=" -j1"
+	epatch "${PATCHES[@]}"
+	sed \
+		-e "/^CC =/s:gcc:$(tc-getCC):g" \
+		-i */Makefile || die
+}
+
+src_compile() {
+	emake all
+}
+
+src_install () {
+	dobin \
+		bin/attack \
+		bin/autosketches4 \
+		bin/clausefilter \
+		bin/clausetester \
+		bin/complex \
+		bin/directproof \
+		bin/dprofiles \
+		bin/fof-prover9 \
+		bin/gen_trc_defs \
+		bin/get_givens \
+		bin/get_interps \
+		bin/get_kept \
+		bin/gvizify \
+		bin/idfilter \
+		bin/interpfilter \
+		bin/interpformat \
+		bin/isofilter \
+		bin/isofilter0 \
+		bin/isofilter2 \
+		bin/ladr_to_tptp \
+		bin/latfilter \
+		bin/looper \
+		bin/mace4 \
+		bin/miniscope \
+		bin/mirror-flip \
+		bin/newauto \
+		bin/newsax \
+		bin/olfilter \
+		bin/perm3 \
+		bin/proof3fo.xsl \
+		bin/prooftrans \
+		bin/prover9 \
+		bin/renamer \
+		bin/rewriter \
+		bin/sigtest \
+		bin/test_clause_eval \
+		bin/test_complex \
+		bin/tptp_to_ladr \
+		bin/unfast \
+		bin/upper-covers
+
+	doman \
+		manpages/interpformat.1 \
+		manpages/isofilter.1 \
+		manpages/prooftrans.1  \
+		manpages/mace4.1 \
+		manpages/prover9.1  \
+		manpages/clausefilter.1 \
+		manpages/clausetester.1 \
+		manpages/interpfilter.1 \
+		manpages/rewriter.1 \
+		manpages/prover9-apps.1
+
+	dohtml ladr/index.html.master ladr/html/*
+
+	insinto /usr/$(get_libdir)
+	dolib.so ladr/.libs/libladr.so.4.0.0
+
+	dosym libladr.so.4.0.0 /usr/$(get_libdir)/libladr.so.4
+	dosym libladr.so.4.0.0 /usr/$(get_libdir)/libladr.so
+
+	dodir /usr/include/ladr
+	insinto /usr/include/ladr
+	doins ladr/*.h
+
+	if use examples; then
+		insinto /usr/share/${PN}/examples
+		doins prover9.examples/*
+
+		# The prover9-mace4 script is installed as an example script
+		# to avoid confusion with the GUI sci-mathematics/p9m4 prover9mace4.py
+		insinto /usr/share/${PN}/scripts
+		doins bin/prover9-mace4
+	fi
+}