New port: math/abella: Interactive theorem prover

math/Makefile

@@ -113,6 +113,7 @@
     SUBDIR += SCIP
     SUBDIR += SoPlex
     SUBDIR += aamath
+    SUBDIR += abella
     SUBDIR += abs
     SUBDIR += acalc
     SUBDIR += add

math/abella/Makefile

@@ -0,0 +1,24 @@
+# $FreeBSD$
+
+PORTNAME=	abella
+DISTVERSION=	2.0.6
+CATEGORIES=	math
+MASTER_SITES=	http://abella-prover.org/distributions/
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Interactive theorem prover
+
+LICENSE=	GPLv3
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+BUILD_DEPENDS=	ocamlbuild:devel/ocaml-ocamlbuild \
+		ocamlfind:devel/ocaml-findlib
+
+USES=		gmake
+
+PLIST_FILES=	bin/${PORTNAME}
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/${PORTNAME} ${STAGEDIR}${PREFIX}/bin
+
+.include <bsd.port.mk>

math/abella/distinfo

@@ -0,0 +1,3 @@
+TIMESTAMP = 1575054547
+SHA256 (abella-2.0.6.tar.gz) = d1f793b1e34f3adcaf6d28e2c0274bccb281afe89c8e3093c1e64df6ec4b9898
+SIZE (abella-2.0.6.tar.gz) = 214785

math/abella/pkg-descr

@@ -0,0 +1,6 @@
+Abella is an interactive theorem prover based on lambda-tree syntax. This means
+that Abella is well-suited for reasoning about the meta-theory of programming
+languages and other logical systems which manipulate objects with binding. For
+example, the following applications are included in the distribution of Abella.
+
+WWW: http://abella-prover.org/