cpet/openbsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

import Prover9, Mace4, and several related programs come packaged in a system

Browse Source 
called LADR (Library for Automated Deduction Research).

split into ladr (prover9 mace4 tools) and p9m4 (gui to ladr)

ok aja@
and thanks to landry@/robert@ too for putting up with my ranting about this..
This commit is contained in:
jasper 2011-03-07 22:26:24 +00:00
parent 5913c1e298
commit 2c96b38d8c
17 changed files with 312 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
math/prover9/Makefile Normal file
View File

@ -0,0 +1,7 @@
# $OpenBSD: Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
SUBDIR =
SUBDIR += ladr
SUBDIR += p9m4
.include <bsd.port.subdir.mk>

13
math/prover9/Makefile.inc Normal file
View File

@ -0,0 +1,13 @@
# $OpenBSD: Makefile.inc,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
CATEGORIES ?= math
HOMEPAGE ?= http://www.cs.unm.edu/~mccune/prover9/
# GPLv2
PERMIT_PACKAGE_CDROM= Yes
PERMIT_PACKAGE_FTP= Yes
PERMIT_DISTFILES_CDROM= Yes
PERMIT_DISTFILES_FTP= Yes
MODULES?= lang/python

43
math/prover9/ladr/Makefile Normal file
View File

@ -0,0 +1,43 @@
# $OpenBSD: Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
COMMENT= Library for Automated Deduction Research
DISTNAME= LADR-Dec-2007
PKGNAME= ${DISTNAME:L:S/-Dec//}
MASTER_SITES= http://www.cs.unm.edu/%7Emccune/prover9/download/
WANTLIB += c m
MODPY_RUNDEP= No
UTIL_FILES= utilities/attack \
utilities/gvizify \
utilities/looper \
utilities/prover9-mace4
MAKE_ENV+= XFLAGS="${CFLAGS}"
REGRESS_TARGET= test1 test2 test3
BIN_DIR= ${PREFIX}/libexec/prover9/
EXAMPLE_DIR= ${PREFIX}/share/examples/prover9/
pre-configure:
.for u in ${UTIL_FILES}
perl -pi -e 's,/usr/bin/python,${MODPY_BIN},g' ${WRKSRC}/$u
.endfor
do-build:
@cd ${WRKSRC} && ${MAKE_ENV} ${MAKE_PROGRAM} ${ALL_TARGET}
do-install:
${INSTALL_DATA_DIR} ${BIN_DIR} ${EXAMPLE_DIR}/{mace4,prover9}
${INSTALL_PROGRAM} ${WRKSRC}/bin/* ${BIN_DIR}
${INSTALL_SCRIPT} ${WRKSRC}/utilities/* ${EXAMPLE_DIR}
${INSTALL_DATA} ${WRKSRC}/mace4.examples/* ${EXAMPLE_DIR}/mace4/
${INSTALL_DATA} ${WRKSRC}/prover9.examples/* ${EXAMPLE_DIR}/prover9/
do-regress:
@cd ${WRKSRC} && ${MAKE_ENV} ${MAKE_PROGRAM} ${REGRESS_TARGET}
.include <bsd.port.mk>

5
math/prover9/ladr/distinfo Normal file
View File

@ -0,0 +1,5 @@
MD5 (LADR-Dec-2007.tar.gz) = biiW7UzORVa/zDIXeN9d/g==
RMD160 (LADR-Dec-2007.tar.gz) = ActjHGKvQ+q1I5Y3pSaIoV7Qa4g=
SHA1 (LADR-Dec-2007.tar.gz) = yCHDib2V+2x8vOUJSY6mwRUlm4g=
SHA256 (LADR-Dec-2007.tar.gz) = iiLdczDMFf43lbpxrk4zezfQ0hyv4Ke6Yb7Svz6AhXc=
SIZE (LADR-Dec-2007.tar.gz) = 1787225

12
math/prover9/ladr/patches/patch-Makefile Normal file
View File

@ -0,0 +1,12 @@
$OpenBSD: patch-Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- Makefile.orig Mon Jan 17 23:08:19 2011
+++ Makefile Mon Jan 17 23:08:49 2011
@@ -6,7 +6,7 @@ all:
cd mace4.src && $(MAKE) all
cd provers.src && $(MAKE) all
cd apps.src && $(MAKE) all
- /bin/cp -p utilities/* bin
+ #/bin/cp -p utilities/* bin
@echo ""
@echo "**** Now try 'make test1'. ****"
@echo ""

11
math/prover9/ladr/patches/patch-apps_src_Makefile Normal file
View File

@ -0,0 +1,11 @@
$OpenBSD: patch-apps_src_Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- apps.src/Makefile.orig Mon Jan 17 23:11:34 2011
+++ apps.src/Makefile Mon Jan 17 23:11:38 2011
@@ -1,6 +1,6 @@
# LADR/apps.src
-CC = gcc
+CC ?= gcc
# XFLAGS can be specified on the command line (see XFLAGS below)

11
math/prover9/ladr/patches/patch-ladr_Makefile Normal file
View File

@ -0,0 +1,11 @@
$OpenBSD: patch-ladr_Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- ladr/Makefile.orig Mon Jan 17 23:09:11 2011
+++ ladr/Makefile Mon Jan 17 23:09:17 2011
@@ -1,6 +1,6 @@
# LADR/ladr
-CC = gcc
+CC ?= gcc
# XFLAGS can be specified on the command line (see XFLAGS below)

11
math/prover9/ladr/patches/patch-mace4_src_Makefile Normal file
View File

@ -0,0 +1,11 @@
$OpenBSD: patch-mace4_src_Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- mace4.src/Makefile.orig Mon Jan 17 23:11:03 2011
+++ mace4.src/Makefile Mon Jan 17 23:11:07 2011
@@ -1,6 +1,6 @@
# LADR/mace4.src
-CC = gcc
+CC ?= gcc
# XFLAGS can be specified on the command line (see XFLAGS below)

11
math/prover9/ladr/patches/patch-provers_src_Makefile Normal file
View File

@ -0,0 +1,11 @@
$OpenBSD: patch-provers_src_Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- provers.src/Makefile.orig Mon Jan 17 23:11:16 2011
+++ provers.src/Makefile Mon Jan 17 23:11:20 2011
@@ -1,6 +1,6 @@
# LADR/prover9.src
-CC = gcc
+CC ?= gcc
# XFLAGS can be specified on the command line (see XFLAGS below)

2
math/prover9/ladr/pkg/DESCR Normal file
View File

@ -0,0 +1,2 @@
Prover9, Mace4, and several related programs come packaged in a system
called LADR (Library for Automated Deduction Research).

48
math/prover9/ladr/pkg/PLIST Normal file
View File

@ -0,0 +1,48 @@
@comment $OpenBSD: PLIST,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
libexec/prover9/
@bin libexec/prover9/autosketches4
@bin libexec/prover9/clausefilter
@bin libexec/prover9/clausetester
@bin libexec/prover9/dprofiles
@bin libexec/prover9/fof-prover9
@bin libexec/prover9/idfilter
@bin libexec/prover9/interpfilter
@bin libexec/prover9/interpformat
@bin libexec/prover9/isofilter
@bin libexec/prover9/isofilter0
@bin libexec/prover9/isofilter2
@bin libexec/prover9/ladr_to_tptp
@bin libexec/prover9/latfilter
@bin libexec/prover9/mace4
@bin libexec/prover9/miniscope
@bin libexec/prover9/mirror-flip
@bin libexec/prover9/newauto
@bin libexec/prover9/newsax
@bin libexec/prover9/olfilter
@bin libexec/prover9/perm3
@bin libexec/prover9/prooftrans
@bin libexec/prover9/prover9
@bin libexec/prover9/renamer
@bin libexec/prover9/rewriter
@bin libexec/prover9/sigtest
@bin libexec/prover9/tptp_to_ladr
@bin libexec/prover9/unfast
@bin libexec/prover9/upper-covers
share/examples/prover9/
share/examples/prover9/attack
share/examples/prover9/get_givens
share/examples/prover9/get_interps
share/examples/prover9/get_kept
share/examples/prover9/gvizify
share/examples/prover9/looper
share/examples/prover9/mace4/
share/examples/prover9/mace4/README
share/examples/prover9/mace4/group2.in
share/examples/prover9/mace4/rw1.in
share/examples/prover9/proof3fo.xsl
share/examples/prover9/prover9/
share/examples/prover9/prover9-mace4
share/examples/prover9/prover9/README
share/examples/prover9/prover9/x2.hints
share/examples/prover9/prover9/x2.in
share/examples/prover9/prover9/x2.out

47
math/prover9/p9m4/Makefile Normal file
View File

@ -0,0 +1,47 @@
# $OpenBSD: Makefile,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
COMMENT= prover9/mace4 GUI
DISTNAME= p9m4-v05
PKGNAME= ${DISTNAME:S/v//}
MASTER_SITES= http://www.cs.unm.edu/%7Emccune/prover9/gui/
CONFIGURE_STYLE= # empty
PKG_ARCH= *
NO_BUILD= Yes
NO_REGRESS= Yes
MODPY_ADJ_FILES= control.py files.py my_setup.py options.py \
partition_input.py platforms.py prover9-mace4.py \
utilities.py wx_utilities.py
RUN_DEPENDS= devel/py-modulegraph \
math/prover9/ladr \
x11/py-wxPython
LIBEXEC_DIR= ${PREFIX}/libexec/prover9/p9m4/
IMAGES_DIR= ${PREFIX}/share/p9m4/Images/
SAMPLES_DIR= ${PREFIX}/share/p9m4/Samples/
# The tarball is a mess and not really designed for installation.
post-extract:
rm -fr ${WRKSRC}/Samples/Kauer.in\~
find ${WRKSRC} -type f -name \*~ -exec rm -f {} \;
pre-configure:
${SUBST_CMD} ${WRKSRC}/files.py
${SUBST_CMD} -c ${FILESDIR}/prover9-mace4.sh ${WRKSRC}/prover9-mace4
do-install:
${INSTALL_SCRIPT} ${WRKSRC}/prover9-mace4 ${PREFIX}/bin/
${INSTALL_DATA_DIR} ${LIBEXEC_DIR} ${IMAGES_DIR} ${SAMPLES_DIR}
${INSTALL_DATA} ${WRKSRC}/Images/* ${IMAGES_DIR}
cd ${WRKSRC}/Samples/ && umask 022 && \
pax -rw . ${SAMPLES_DIR}
.for m in ${MODPY_ADJ_FILES}
${INSTALL_SCRIPT} ${WRKSRC}/$m ${LIBEXEC_DIR}
.endfor
.include <bsd.port.mk>

5
math/prover9/p9m4/distinfo Normal file
View File

@ -0,0 +1,5 @@
MD5 (p9m4-v05.tar.gz) = /gMfvEmVPFgPVMEYZPMaNg==
RMD160 (p9m4-v05.tar.gz) = APZP1dwHresHUiGMMZ4d+hMLUeE=
SHA1 (p9m4-v05.tar.gz) = yc4kQAuW+q7COguD0z0+KDqvTGc=
SHA256 (p9m4-v05.tar.gz) = RRoFF5/LAltmbsmSzUXg1x2sJuQ8H8qBR0e+9UGgQLQ=
SIZE (p9m4-v05.tar.gz) = 889707

7
math/prover9/p9m4/files/prover9-mace4.sh Normal file
View File

@ -0,0 +1,7 @@
#!/bin/sh
#
# $OpenBSD: prover9-mace4.sh,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
#
# Wrapper script to call the actual prover9-mace4.py script
${MODPY_BIN} ${TRUEPREFIX}/libexec/prover9/p9m4/prover9-mace4.py "$@"

20
math/prover9/p9m4/patches/patch-p9m4_files_py Normal file
View File

@ -0,0 +1,20 @@
$OpenBSD: patch-p9m4_files_py,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
--- files.py.orig Fri Dec 7 21:46:28 2007
+++ files.py Tue Jan 18 12:23:50 2011
@@ -63,13 +63,13 @@ def bin():
return 'bin'
def bin_dir():
- return os.path.join(program_dir(), bin())
+ return '${TRUEPREFIX}/libexec/prover9/'
def image_dir():
- return os.path.join(program_dir(), 'Images')
+ return '${TRUEPREFIX}/share/p9m4/Images/'
def sample_dir():
- return os.path.join(program_dir(), 'Samples')
+ return '${TRUEPREFIX}/share/p9m4/Samples/'
def binary_ok(fullpath):
if not fullpath:

1
math/prover9/p9m4/pkg/DESCR Normal file
View File

@ -0,0 +1 @@
GUI for the LADR (prover9 mace4) tools.

58
math/prover9/p9m4/pkg/PLIST Normal file
View File

@ -0,0 +1,58 @@
@comment $OpenBSD: PLIST,v 1.1.1.1 2011/03/07 22:26:24 jasper Exp $
bin/prover9-mace4
libexec/prover9/
libexec/prover9/p9m4/
libexec/prover9/p9m4/control.py
libexec/prover9/p9m4/files.py
libexec/prover9/p9m4/my_setup.py
libexec/prover9/p9m4/options.py
libexec/prover9/p9m4/partition_input.py
libexec/prover9/p9m4/platforms.py
libexec/prover9/p9m4/prover9-mace4.py
libexec/prover9/p9m4/utilities.py
libexec/prover9/p9m4/wx_utilities.py
share/p9m4/
share/p9m4/Images/
share/p9m4/Images/mace4-90t.gif
share/p9m4/Images/p9.ico
share/p9m4/Images/prover9-5a-128t.gif
share/p9m4/Images/prover9-splash.gif
share/p9m4/Samples/
share/p9m4/Samples/Equality/
share/p9m4/Samples/Equality/Mace4/
share/p9m4/Samples/Equality/Mace4/BA-Sheffer-counterexample.in
share/p9m4/Samples/Equality/Mace4/CL-QL.in
share/p9m4/Samples/Equality/Mace4/Megill-68.in
share/p9m4/Samples/Equality/Mace4/Noncommutative-group-48.in
share/p9m4/Samples/Equality/Mace4/Noncommutative-group.in
share/p9m4/Samples/Equality/Mace4/Noncommutative-ring-unit.in
share/p9m4/Samples/Equality/Mace4/Nonmodular-OML.in
share/p9m4/Samples/Equality/Mace4/QG-4.in
share/p9m4/Samples/Equality/Mace4/Ring-19.in
share/p9m4/Samples/Equality/Mace4/TBA-independence-2.in
share/p9m4/Samples/Equality/Prover9/
share/p9m4/Samples/Equality/Prover9/BA-distributivity.in
share/p9m4/Samples/Equality/Prover9/CL-BW.in
share/p9m4/Samples/Equality/Prover9/CL-SK-W.in
share/p9m4/Samples/Equality/Prover9/Cancellative-semigroup-EA.in
share/p9m4/Samples/Equality/Prover9/LT-McKenzie-4basis.in
share/p9m4/Samples/Equality/Prover9/OML-sax.in
share/p9m4/Samples/Equality/Prover9/RBA-2.in
share/p9m4/Samples/GT_Sax.in
share/p9m4/Samples/Kauer.in
share/p9m4/Samples/LT-McKenzie-4basis.in
share/p9m4/Samples/Non-Equality/
share/p9m4/Samples/Non-Equality/Mace4/
share/p9m4/Samples/Non-Equality/Mace4/EC-counterexample.in
share/p9m4/Samples/Non-Equality/Mace4/Kauer.in
share/p9m4/Samples/Non-Equality/Mace4/Steam-bug.in
share/p9m4/Samples/Non-Equality/Mace4/Toughnut.in
share/p9m4/Samples/Non-Equality/Prover9/
share/p9m4/Samples/Non-Equality/Prover9/EC-XCB-reflexivity.in
share/p9m4/Samples/Non-Equality/Prover9/HWV006-1.in
share/p9m4/Samples/Non-Equality/Prover9/Lifschitz.in
share/p9m4/Samples/Non-Equality/Prover9/Steam.in
share/p9m4/Samples/Non-Equality/Prover9/Subset_transitive.in
share/p9m4/Samples/Non-Equality/Prover9/temp
share/p9m4/Samples/Non-Equality/Prover9/temp0
share/p9m4/Samples/Non-Equality/Prover9/temp1