1 files changed, 124 insertions, 0 deletions
diff --git a/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild b/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild
new file mode 100644
index 000000000000..63b9fad1839f
--- /dev/null
+++ b/sci-mathematics/prover9/prover9-2009.11a-r1.ebuild
@@ -0,0 +1,124 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit toolchain-funcs
+
+MY_PN="LADR"
+typeset -u MY_PV
+MY_PV="$(ver_rs 1 '-')"
+MY_P="${MY_PN}-${MY_PV}"
+
+DESCRIPTION="Automated theorem prover for first-order and equational logic"
+HOMEPAGE="https://www.cs.unm.edu/~mccune/mace4/"
+SRC_URI="
+	https://www.cs.unm.edu/~mccune/mace4/download/${MY_P}.tar.gz
+	https://dev.gentoo.org/~jlec/distfiles/${MY_PN}-2009-11A-makefile.patch.xz
+"
+S="${WORKDIR}/${MY_P}/"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="examples"
+
+PATCHES=(
+	"${WORKDIR}/${MY_PN}-2009-11A-makefile.patch"
+	"${FILESDIR}/${MY_PN}-2009-11A-manpages.patch"
+)
+
+src_prepare() {
+	default
+
+	sed -e "/^CC =/s:gcc:$(tc-getCC):g" -i */Makefile || die
+
+	export MAKEOPTS+=" -j1 "
+	tc-export AR CC
+}
+
+src_compile() {
+	emake CFLAGS="${CFLAGS} ${LDFLAGS}" -j1 all
+}
+
+src_test() {
+	LD_LIBRARY_PATH="${S}/ladr/.libs/" emake -j1 test1 test2 test3
+}
+
+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
+
+	docinto html
+	dodoc -r 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"
+
+	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
+}