mirror/freebsd-ports
1
0
Fork 0
mirror of https://git.FreeBSD.org/ports.git synced 2024-11-20 00:21:35 +00:00
Code Issues Releases Activity

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

Browse Source 
verification.
This commit is contained in:
Brendan Fabeny 2011-12-21 02:58:24 +00:00
parent 780e00e70f
commit 88ece46f9f
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=287773
5 changed files with 88 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
math/Makefile
View File

@ -28,6 +28,7 @@
SUBDIR += add
SUBDIR += algae
SUBDIR += algotutor
SUBDIR += alt-ergo
SUBDIR += ann
SUBDIR += apc
SUBDIR += aribas

65
math/alt-ergo/Makefile Normal file
View File

@ -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>

2
math/alt-ergo/distinfo Normal file
View File

@ -0,0 +1,2 @@
SHA256 (alt-ergo-0.94.tar.gz) = bb6ddf947357d587eac4dc3375b712af2c58e46d3f5ab2c8eee5f25a99c2cd6e
SIZE (alt-ergo-0.94.tar.gz) = 188414

10
math/alt-ergo/pkg-descr Normal file
View File

@ -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

10
math/alt-ergo/pkg-plist Normal file
View File

@ -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