Add alt-ergo 0.94, an automatic theorem prover dedicated to program

verification.

5 files changed, 88 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 88886fb7fcc1..545d75233200 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -28,6 +28,7 @@
     SUBDIR += add
     SUBDIR += algae
     SUBDIR += algotutor
+    SUBDIR += alt-ergo
     SUBDIR += ann
     SUBDIR += apc
     SUBDIR += aribas
diff --git a/math/alt-ergo/Makefile b/math/alt-ergo/Makefile
new file mode 100644
index 000000000000..5e2fe5a349be
--- /dev/null
+++ b/math/alt-ergo/Makefile
@@ -0,0 +1,65 @@
+# New ports collection makefile for:    alt-ergo
+# Date created:         20 December 2011
+# Whom:                 b.f. <bf@FreeBSD.org>
+#
+# $FreeBSD$
+#
+
+PORTNAME=	alt-ergo
+PORTVERSION=	0.94
+CATEGORIES=	math
+MASTER_SITES=	http://alt-ergo.lri.fr/http/ LOCAL/bf
+
+MAINTAINER=	bf@FreeBSD.org
+COMMENT=	An automatic theorem prover dedicated to program verification
+
+LICENSE=	CeCILL-C
+LICENSE_NAME=	Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre] C license, version 1
+LICENSE_FILE=	${WRKSRC}/CeCILL-C
+LICENSE_PERMS=	auto-accept
+
+BUILD_DEPENDS=	${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph
+RUN_DEPENDS=	${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph
+
+GNU_CONFIGURE=	yes
+USE_GMAKE=	yes
+USE_OCAML=	yes
+
+MAN1=	alt-ergo.1
+
+OPTIONS=	GUI	"Build the GUI" on
+
+.include <bsd.port.options.mk>
+
+.if defined(WITH_GUI)
+BUILD_DEPENDS +=	lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
+RUN_DEPENDS+=		lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
+ALL_TARGET=	all gui
+INSTALL_TARGET =	install install-gui
+PLIST_SUB+=	GUI=""
+.else
+PLIST_SUB+=	GUI="@comment "
+.endif
+
+post-patch:
+	@${REINPLACE_CMD} -e '\|^# installation|,\|^# documentation|{ \
+		\|cp -f.*$$(BINDIR)|s|cp -f|${INSTALL_SCRIPT}|; \
+		\|cp -f.*$$(MANDIR)|s|cp -f|${INSTALL_MAN}|; \
+		\|cp -f.*$$(LIBDIR)|s|cp -f|${INSTALL_DATA}|; \
+		\|/usr/share/gtksourceview-2.0|s|/usr|${PREFIX}|; }' \
+		-e 's|make -C|${GMAKE} -C|' \
+			${WRKSRC}/Makefile.in
+
+.if defined(WITH_GUI)
+pre-configure:
+	@(if [ ! -e ${LOCALBASE}/lib/ocaml/lablgtk2/lablgtksourceview2.cmxa ] ; then \
+	${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \
+	${ECHO_MSG} "==> x11-toolkits/ocaml-lablgtk2 to be built" ; \
+	${ECHO_MSG} "==> WITH_GTKSOURCEVIEW2" ; \
+	exit 1; fi)
+
+pre-install:
+	@${MKDIR} ${PREFIX}/share/gtksourceview-2.0/language-specs
+
+.endif
+.include <bsd.port.mk>
diff --git a/math/alt-ergo/distinfo b/math/alt-ergo/distinfo
new file mode 100644
index 000000000000..adcc633d41fb
--- /dev/null
+++ b/math/alt-ergo/distinfo
@@ -0,0 +1,2 @@
+SHA256 (alt-ergo-0.94.tar.gz) = bb6ddf947357d587eac4dc3375b712af2c58e46d3f5ab2c8eee5f25a99c2cd6e
+SIZE (alt-ergo-0.94.tar.gz) = 188414
diff --git a/math/alt-ergo/pkg-descr b/math/alt-ergo/pkg-descr
new file mode 100644
index 000000000000..21976de2c59e
--- /dev/null
+++ b/math/alt-ergo/pkg-descr
@@ -0,0 +1,10 @@
+Alt-Ergo is an automatic theorem prover dedicated to program verification.
+Alt-Ergo is based on CC(X), a congruence closure algorithm parameterized by
+an equational theory X. Currently, CC(X) can be instantiated by the empty
+equational theory and by the linear arithmetics. Alt-Ergo contains also a
+home made SAT-solver and an instantiation mechanism.
+
+Alt-Ergo is compact, safe, and modular. Each component is described by a small
+set of inference rules and is implemented as an Ocaml functor.
+
+WWW:	http://alt-ergo.lri.fr
diff --git a/math/alt-ergo/pkg-plist b/math/alt-ergo/pkg-plist
new file mode 100644
index 000000000000..de2ca2b20183
--- /dev/null
+++ b/math/alt-ergo/pkg-plist
@@ -0,0 +1,10 @@
+bin/alt-ergo
+%%GUI%%bin/altgr-ergo
+lib/alt-ergo/altErgo.cmi
+lib/alt-ergo/altErgo.cmo
+lib/alt-ergo/altErgo.cmx
+lib/alt-ergo/altErgo.o
+share/gtksourceview-2.0/language-specs/alt-ergo.lang
+@dirrmtry share/gtksourceview-2.0/language-specs
+@dirrmtry share/gtksourceview-2.0
+@dirrm lib/alt-ergo