From fae7336844c2bbeaee2bc3644c2c90ca8dbebfe2 Mon Sep 17 00:00:00 2001
From: Yuri Victorovich <yuri@FreeBSD.org>
Date: Fri, 29 Nov 2019 19:40:18 +0000
Subject: [PATCH] New port: math/abella: Interactive theorem prover

---
 math/Makefile         |  1 +
 math/abella/Makefile  | 24 ++++++++++++++++++++++++
 math/abella/distinfo  |  3 +++
 math/abella/pkg-descr |  6 ++++++
 4 files changed, 34 insertions(+)
 create mode 100644 math/abella/Makefile
 create mode 100644 math/abella/distinfo
 create mode 100644 math/abella/pkg-descr

diff --git a/math/Makefile b/math/Makefile
index be91dbcf94b0..eae75b2f3df0 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -113,6 +113,7 @@
     SUBDIR += SCIP
     SUBDIR += SoPlex
     SUBDIR += aamath
+    SUBDIR += abella
     SUBDIR += abs
     SUBDIR += acalc
     SUBDIR += add
diff --git a/math/abella/Makefile b/math/abella/Makefile
new file mode 100644
index 000000000000..f2a1a2408bb4
--- /dev/null
+++ b/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>
diff --git a/math/abella/distinfo b/math/abella/distinfo
new file mode 100644
index 000000000000..8b2638535e06
--- /dev/null
+++ b/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
diff --git a/math/abella/pkg-descr b/math/abella/pkg-descr
new file mode 100644
index 000000000000..912d5264ab27
--- /dev/null
+++ b/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/