proj/gentoo: Initial commit

This commit represents a new era for Gentoo:
Storing the gentoo-x86 tree in Git, as converted from CVS.

This commit is the start of the NEW history.
Any historical data is intended to be grafted onto this point.

Creation process:
1. Take final CVS checkout snapshot
2. Remove ALL ChangeLog* files
3. Transform all Manifests to thin
4. Remove empty Manifests
5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$
5.1. Do not touch files with -kb/-ko keyword flags.

Signed-off-by: Robin H. Johnson <robbat2@gentoo.org>
X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests
X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project
X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration
X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn
X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts
X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration
X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging
X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed

4 files changed, 603 insertions, 0 deletions

diff --git a/sci-mathematics/prover9/Manifest b/sci-mathematics/prover9/Manifest
new file mode 100644
index 000000000000..f791dc6bd655
--- /dev/null
+++ b/sci-mathematics/prover9/Manifest
@@ -0,0 +1,2 @@
+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
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..719fd32dcf90
--- /dev/null
+++ b/sci-mathematics/prover9/metadata.xml
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+  <maintainer>
+    <email>gienah@gentoo.org</email>
+    <name>Mark Wright</name>
+  </maintainer>
+  <herd>sci-mathematics</herd>
+  <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..5a45978b0ebe
--- /dev/null
+++ b/sci-mathematics/prover9/prover9-2009.11a.ebuild
@@ -0,0 +1,120 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+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
+	http://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
+}