Update to 8.5.

math/coq/Makefile

@@ -1,12 +1,10 @@
 # $FreeBSD$
 
 PORTNAME=	coq
-PORTVERSION=	8.4.6
-PORTEPOCH=	3
+PORTVERSION=	8.5
 CATEGORIES=	math
-MASTER_SITES=	http://coq.inria.fr/distrib/V${COQVERSION}/files/ \
+MASTER_SITES=	http://coq.inria.fr/distrib/V${PORTVERSION}/files/ \
 		ftp://ftp.stack.nl/pub/users/johans/coq/
-DISTNAME=	${PORTNAME}-${COQVERSION}
 
 MAINTAINER=	hrs@FreeBSD.org
 COMMENT=	Theorem prover based on lambda-C
@@ -21,64 +19,40 @@ LIB_DEPENDS=	libfontconfig.so:x11-fonts/fontconfig \
 
 COQVERSION=	${PORTVERSION:R}pl${PORTVERSION:E}
 USES=		gmake gettext-runtime
-USE_GNOME=	atk cairo gdkpixbuf2 glib20 gtk20 pango
+USE_EMACS=	yes
+USE_GNOME=	atk cairo gdkpixbuf2 glib20 gtk20 gtksourceview2 pango
+USE_LDCONFIG=	${PREFIX}/lib/coq
 USE_OCAML=	yes
 HAS_CONFIGURE=	yes
-CONFIGURE_ARGS=	--prefix ${PREFIX} \
-		--mandir ${PREFIX}/man \
-		--emacslib ${PREFIX}/share/emacs/site-lisp \
-		--opt
+CONFIGURE_ARGS=	-prefix ${PREFIX} \
+		-mandir ${PREFIX}/man \
+		-emacslib ${PREFIX}/share/emacs/site-lisp/coq \
+		-usecamlp5 \
+		-byteonly \
+		-makecmd ${MAKE_CMD}
+MAKE_ENV=	VERBOSE=1
 ALL_TARGET=	world
 
 BROKEN_powerpc=		does not link
 
-STRIP_FILES= \
-	lib/coq/dllcoqrun.so \
-	lib/coq/plugins/cc/cc_plugin.cmxs \
-	lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs \
-	lib/coq/plugins/extraction/extraction_plugin.cmxs \
-	lib/coq/plugins/field/field_plugin.cmxs \
-	lib/coq/plugins/firstorder/ground_plugin.cmxs \
-	lib/coq/plugins/fourier/fourier_plugin.cmxs \
-	lib/coq/plugins/funind/recdef_plugin.cmxs \
-	lib/coq/plugins/micromega/micromega_plugin.cmxs \
-	lib/coq/plugins/nsatz/nsatz_plugin.cmxs \
-	lib/coq/plugins/omega/omega_plugin.cmxs \
-	lib/coq/plugins/quote/quote_plugin.cmxs \
-	lib/coq/plugins/ring/ring_plugin.cmxs \
-	lib/coq/plugins/romega/romega_plugin.cmxs \
-	lib/coq/plugins/rtauto/rtauto_plugin.cmxs \
-	lib/coq/plugins/setoid_ring/newring_plugin.cmxs \
-	lib/coq/plugins/subtac/subtac_plugin.cmxs \
-	lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs \
-	lib/coq/plugins/syntax/nat_syntax_plugin.cmxs \
-	lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs \
-	lib/coq/plugins/syntax/r_syntax_plugin.cmxs \
-	lib/coq/plugins/syntax/string_syntax_plugin.cmxs \
-	lib/coq/plugins/syntax/z_syntax_plugin.cmxs \
-	lib/coq/plugins/xml/xml_plugin.cmxs
-
 OPTIONS_DEFINE=		DOCS IDE
 OPTIONS_DEFAULT=	IDE
 OPTIONS_SUB=		yes
 IDE_DESC=		Include desktop environment (coqide)
 IDE_BUILD_DEPENDS=	lablgtk2:x11-toolkits/ocaml-lablgtk2
 IDE_RUN_DEPENDS=	lablgtk2:x11-toolkits/ocaml-lablgtk2
-IDE_CONFIGURE_OFF=	--coqide no
+IDE_CONFIGURE_OFF=	-coqide no
 DOCS_USE=		TEX=latex:build,dvipsk:build,texmf:build
 DOCS_BUILD_DEPENDS=	hevea:textproc/hevea
-DOCS_CONFIGURE_OFF=	--with-doc none
-PORTDOCS=		*
+DOCS_CONFIGURE_OFF=	-with-doc no
+
+STRIP_FILES=		lib/coq/dllcoqrun.so
 
 # Workaround bsd.ocaml.mk to fix packaging
 add-plist-post:
 	@${DO_NADA}
 
 post-patch:
-	${REINPLACE_CMD} -e '/FreeBSD.*\.byte/s/^/#/' \
-	    -e '/^MAKE=/d' ${WRKSRC}/configure
-	${REINPLACE_CMD} -e '/^#COQINSTALLPREFIX/{s/^#//;s|$$|$${DESTDIR}|;}' \
-	    ${WRKSRC}/Makefile.build
 	${REINPLACE_CMD} -e '/show_latex_mes/s/)$$/; true)/' \
 	    ${WRKSRC}/Makefile.doc
 

math/coq/distinfo

@@ -1,2 +1,3 @@
-SHA256 (coq-8.4pl6.tar.gz) = a540a231a9970a49353ca039f3544616ff86a208966ab1c593779ae13c91ebd6
-SIZE (coq-8.4pl6.tar.gz) = 4099815
+TIMESTAMP = 1483174912
+SHA256 (coq-8.5.tar.gz) = 89a92fb8b91e7cb0797d41c87cd13e4b63bee76c32a6dcc3d7c8055ca6a9ae3d
+SIZE (coq-8.5.tar.gz) = 5346653

math/coq/files/patch-Makefile.build

@@ -0,0 +1,29 @@
+--- Makefile.build.orig	2016-01-20 16:52:18 UTC
++++ Makefile.build
+@@ -56,7 +56,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES))
+ 
+ # Variables meant to be modifiable via the command-line of make
+ 
+-VERBOSE=
++VERBOSE=1
+ NO_RECOMPILE_ML4=
+ NO_RECALC_DEPS=
+ READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
+@@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U m
+ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+ 
+ COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
+-BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
++BOOTCOQC=$(TIMER) env CAML_LD_LIBRARY_PATH=$${PWD}/kernel/byterun $(COQTOPEXE) -boot $(COQOPTS) -compile
+ 
+ # The SHOW and HIDE variables control whether make will echo complete commands 
+ # or only abbreviated versions. 
+@@ -704,7 +704,7 @@ install-doc-no:
+ .PHONY: install install-doc-all install-doc-no
+ 
+ #These variables are intended to be set by the caller to make
+-#COQINSTALLPREFIX=
++COQINSTALLPREFIX=${DESTDIR}
+ #OLDROOT=
+ 
+   # Can be changed for a local installation (to make packages).

math/coq/files/patch-configure.ml

@@ -0,0 +1,11 @@
+--- configure.ml.orig	2016-01-20 16:52:18 UTC
++++ configure.ml
+@@ -843,7 +843,7 @@ let strip =
+ (** * md5sum command *)
+ 
+ let md5sum =
+-  if arch = "Darwin" then "md5 -q" else "md5sum"
++  if arch = "FreeBSD" then "md5 -q" else "md5sum"
+ 
+ 
+ (** * Documentation : do we have latex, hevea, ... *)