diff options
| -rw-r--r-- | math/Makefile | 1 | ||||
| -rw-r--r-- | math/abella/Makefile | 24 | ||||
| -rw-r--r-- | math/abella/distinfo | 3 | ||||
| -rw-r--r-- | math/abella/pkg-descr | 6 |
4 files changed, 34 insertions, 0 deletions
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/ |