Skip site navigation (1)Skip section navigation (2)
Date:      Sun, 28 Jun 2015 08:38:47 +0000 (UTC)
From:      John Marino <marino@FreeBSD.org>
To:        ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org
Subject:   svn commit: r390756 - in head/math: . alt-ergo-spark
Message-ID:  <201506280838.t5S8cl0U058006@svn.freebsd.org>

next in thread | raw e-mail | index | archive | help
Author: marino
Date: Sun Jun 28 08:38:46 2015
New Revision: 390756
URL: https://svnweb.freebsd.org/changeset/ports/390756

Log:
  Add new port math/alt-ergo-spark (required by SPARK 2015)
  
  This will be RUN_DEPENDS for lang/spark when it is fixed.  The "stock"
  math/alt-ergo cannot be used, it locks up when gnatprove calls it.

Added:
  head/math/alt-ergo-spark/
  head/math/alt-ergo-spark/Makefile   (contents, props changed)
  head/math/alt-ergo-spark/distinfo   (contents, props changed)
  head/math/alt-ergo-spark/pkg-descr   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Sun Jun 28 08:38:43 2015	(r390755)
+++ head/math/Makefile	Sun Jun 28 08:38:46 2015	(r390756)
@@ -52,6 +52,7 @@
     SUBDIR += algae
     SUBDIR += algotutor
     SUBDIR += alt-ergo
+    SUBDIR += alt-ergo-spark
     SUBDIR += analitza
     SUBDIR += ann
     SUBDIR += apc

Added: head/math/alt-ergo-spark/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/alt-ergo-spark/Makefile	Sun Jun 28 08:38:46 2015	(r390756)
@@ -0,0 +1,32 @@
+# $FreeBSD$
+
+PORTNAME=	alt-ergo
+PORTVERSION=	2015
+CATEGORIES=	math
+MASTER_SITES=	http://downloads.dragonlace.net/src/
+PKGNAMESUFFIX=	-spark
+DISTNAME=	alt-ergo-for-spark-gpl-${PORTVERSION}-src
+
+MAINTAINER=	marino@FreeBSD.org
+COMMENT=	Automatic solver for SPARK 2015
+
+LICENSE=	CeCILL-C
+LICENSE_NAME=	Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre] C license, version 1
+LICENSE_FILE=	${WRKSRC}/LICENSE
+LICENSE_PERMS=	dist-mirror dist-sell pkg-mirror pkg-sell auto-accept
+
+BUILD_DEPENDS=	ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \
+		ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph
+RUN_DEPENDS=	ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph
+
+USES=		gmake
+USE_OCAML=	yes
+GNU_CONFIGURE=	yes
+MAKE_ARGS=	NAME=alt-ergo-spark
+PLIST_FILES=	bin/alt-ergo-spark man/man1/alt-ergo-spark.1.gz
+
+post-install:
+	${MV} ${STAGEDIR}${MANPREFIX}/man/man1/alt-ergo.1 \
+		${STAGEDIR}${MANPREFIX}/man/man1/alt-ergo-spark.1.gz
+
+.include <bsd.port.mk>

Added: head/math/alt-ergo-spark/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/alt-ergo-spark/distinfo	Sun Jun 28 08:38:46 2015	(r390756)
@@ -0,0 +1,2 @@
+SHA256 (alt-ergo-for-spark-gpl-2015-src.tar.gz) = 56e70ee8d7b67e95945c156ff80833e45612882605a163a779b7d11ea01f6fbf
+SIZE (alt-ergo-for-spark-gpl-2015-src.tar.gz) = 230073

Added: head/math/alt-ergo-spark/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/alt-ergo-spark/pkg-descr	Sun Jun 28 08:38:46 2015	(r390756)
@@ -0,0 +1,4 @@
+This is a component of SPARK 2015:  Those looking for the automatic
+theorem prover known as Alt-Ergo should refer to math/alt-ergo instead
+
+WWW: https://forge.open-do.org/projects/spark2014



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201506280838.t5S8cl0U058006>