diff options
| author | Yuri Victorovich <yuri@FreeBSD.org> | 2019-11-29 19:40:18 +0000 |
|---|---|---|
| committer | Yuri Victorovich <yuri@FreeBSD.org> | 2019-11-29 19:40:18 +0000 |
| commit | fae7336844c2bbeaee2bc3644c2c90ca8dbebfe2 (patch) | |
| tree | bd4300e629354c3ae1d7fa18245df372e1f97f3b /math/abella | |
| parent | 225021335c3225c14398aa880d6b590ad02f0608 (diff) | |
| download | ports-fae7336844c2bbeaee2bc3644c2c90ca8dbebfe2.tar.gz ports-fae7336844c2bbeaee2bc3644c2c90ca8dbebfe2.zip | |
New port: math/abella: Interactive theorem prover
Notes
Notes:
svn path=/head/; revision=518670
Diffstat (limited to 'math/abella')
| -rw-r--r-- | math/abella/Makefile | 24 | ||||
| -rw-r--r-- | math/abella/distinfo | 3 | ||||
| -rw-r--r-- | math/abella/pkg-descr | 6 |
3 files changed, 33 insertions, 0 deletions
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/ |