aboutsummaryrefslogtreecommitdiff
path: root/math/why3
diff options
context:
space:
mode:
authorJohn Marino <marino@FreeBSD.org>2015-06-28 07:11:24 +0000
committerJohn Marino <marino@FreeBSD.org>2015-06-28 07:11:24 +0000
commit768423ca5dc18dade9daf68c3eb2a0f8100b06dc (patch)
treec8d027470055c32fbbbb1c9b557eda81ee15d9ec /math/why3
parent13964b031c8e803621b416b43be66854b8ec5eda (diff)
downloadports-768423ca5dc18dade9daf68c3eb2a0f8100b06dc.tar.gz
ports-768423ca5dc18dade9daf68c3eb2a0f8100b06dc.zip
math/why3: Release port
I only care about math/why3-gpl, which has been decoupled from why3 and has already diverged. Before resetting MAINTAINER, I reintegrated the Makefile.common file (only used by this port) into the main Makefile. In the process, some options placeholders were lost but in all probability these options can't be built without serious work on external ports.
Notes
Notes: svn path=/head/; revision=390740
Diffstat (limited to 'math/why3')
-rw-r--r--math/why3/Makefile51
-rw-r--r--math/why3/Makefile.common66
2 files changed, 48 insertions, 69 deletions
diff --git a/math/why3/Makefile b/math/why3/Makefile
index 2b5b660e0c2f..5d8ff420f616 100644
--- a/math/why3/Makefile
+++ b/math/why3/Makefile
@@ -8,16 +8,61 @@ CATEGORIES= math
MASTER_SITES= http://gforge.inria.fr/frs/download.php/33490/ \
http://pkgs.fedoraproject.org/repo/pkgs/why3/${FEDORA}/
-MAINTAINER= marino@FreeBSD.org
+MAINTAINER= ports@FreeBSD.org
COMMENT= Deductive program verification platform
LICENSE= LGPL21
CONFLICT_INSTALL= why3-gpl-*
+BUILD_DEPENDS= ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \
+ lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 \
+ ocaml-sqlite3>2:${PORTSDIR}/databases/ocaml-sqlite3 \
+ ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph \
+ camlp5o:${PORTSDIR}/devel/ocaml-camlp5
+
+GNU_CONFIGURE= yes
+INSTALL_TARGET= install-all
+
+USES= gmake
+USE_OCAML= yes
+
FEDORA= ${DISTNAME}${EXTRACT_SUFX}/35f99e5f64939e50ea57f641ba2073ec
ALL_TARGET= all byte
-HAS_MANUAL= yes
-.include "${.CURDIR}/Makefile.common"
+CONFIGURE_ARGS= --enable-relocation \
+ --disable-doc \
+ --disable-pvs-libs \
+ --disable-profiling \
+ --disable-coq-tactic \
+ --disable-coq-libs \
+ --disable-isabelle-libs
+
+OPTIONS_DEFINE= DOCS
+
+# The pdf is pre-built, but the makefile wants to build it again in order
+# to generate manual.bbl which is used to build the html documention.
+# Regenerating pdf fails, and the dependencies are heavy. Disable this
+# all for now and just manually install the pdf. The "doc" target was
+# also removed from ALL_TARGET
+#
+#DOCS_CONFIGURE_ENABLE= doc
+#DOCS_BUILD_DEPENDS= rubber:${PORTSDIR}/textproc/rubber \
+# hevea:${PORTSDIR}/textproc/hevea
+
+MAKE_JOBS_UNSAFE= yes
+
+.include <bsd.port.options.mk>
+
+post-patch:
+ @${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
+ ${WRKSRC}/src/util/sysutil.ml \
+ ${WRKSRC}/src/jessie/Makefile.in
+
+post-install:
+.if ${PORT_OPTIONS:MDOCS}
+ ${MKDIR} ${STAGEDIR}${DOCSDIR}
+ ${INSTALL_DATA} ${WRKSRC}/doc/manual.pdf ${STAGEDIR}${DOCSDIR}
+.endif
+
.include <bsd.port.mk>
diff --git a/math/why3/Makefile.common b/math/why3/Makefile.common
deleted file mode 100644
index 368ed18e666d..000000000000
--- a/math/why3/Makefile.common
+++ /dev/null
@@ -1,66 +0,0 @@
-# Created by: John Marino <marino@FreeBSD.org>
-# $FreeBSD$
-
-BUILD_DEPENDS= ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \
- lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 \
- ocaml-sqlite3>2:${PORTSDIR}/databases/ocaml-sqlite3 \
- ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph \
- camlp5o:${PORTSDIR}/devel/ocaml-camlp5
-
-GNU_CONFIGURE= yes
-INSTALL_TARGET= install-all
-
-USES= gmake
-USE_OCAML= yes
-MAKE_JOBS_UNSAFE= yes
-
-# The FRAMA_C plugin is experimental, it actually doesn't even build
-# with ocaml 4.01. Leave the option commented out for future use.
-# There is something wrong with coq, it rebuilds itself in /usr/local.
-# Leave it for now with a TO-DO to fix coq
-
-CONFIGURE_ARGS= --enable-relocation \
- --disable-doc \
- --disable-pvs-libs \
- --disable-profiling \
- --disable-coq-tactic \
- --disable-coq-libs \
- --disable-isabelle-libs
-
-.if defined(HAS_MANUAL)
-OPTIONS_DEFINE= DOCS #COQ FRAMA_C
-.endif
-
-COQ_CONFIGURE_ENABLE= coq-tactic coq-libs
-COQ_DESC= Build coq realizations and tactics
-COQ_BUILD_DEPENDS= coqc:${PORTSDIR}/math/coq
-COQ_RUN_DEPENDS= coqc:${PORTSDIR}/math/coq
-FRAMA_C_CONFIGURE_ENABLE= frama_c
-FRAMA_C_DESC= Build Frama-C plugin
-FRAMA_C_BUILD_DEPENDS= frama-c:${PORTSDIR}/devel/frama-c
-FRAMA_C_RUN_DEPENDS= frama-c:${PORTSDIR}/devel/frama-c
-
-# The pdf is pre-built, but the makefile wants to build it again in order
-# to generate manual.bbl which is used to build the html documention.
-# Regenerating pdf fails, and the dependencies are heavy. Disable this
-# all for now and just manually install the pdf. The "doc" target was
-# also removed from ALL_TARGET
-#
-#DOCS_CONFIGURE_ENABLE= doc
-#DOCS_BUILD_DEPENDS= rubber:${PORTSDIR}/textproc/rubber \
-# hevea:${PORTSDIR}/textproc/hevea
-
-.include <bsd.port.options.mk>
-
-post-patch:
- @${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
- ${WRKSRC}/src/util/sysutil.ml \
- ${WRKSRC}/src/jessie/Makefile.in
-
-post-install:
-.if ${PORT_OPTIONS:MDOCS}
-. if defined(HAS_MANUAL)
- ${MKDIR} ${STAGEDIR}${DOCSDIR}
- ${INSTALL_DATA} ${WRKSRC}/doc/manual.pdf ${STAGEDIR}${DOCSDIR}
-. endif
-.endif