Thu May 23 10:55:07 2019 UTC ()
Updated lang/coq to version 8.9.1.

Main changes:
* some quality-of-life bug fixes,
* many improvements to the documentation,
* a critical bug fix related to primitive projections and native_compute,
* several additional Coq libraries shipped with the Windows installer.


(jaapb)
diff -r1.121 -r1.122 pkgsrc/lang/coq/Makefile
diff -r1.32 -r1.33 pkgsrc/lang/coq/distinfo
cvs diff -r1.121 -r1.122 pkgsrc/lang/coq/Makefile (switch to unified diff)

--- pkgsrc/lang/coq/Makefile 2019/05/05 22:49:48 1.121
+++ pkgsrc/lang/coq/Makefile 2019/05/23 10:55:07 1.122
@@ -1,84 +1,83 @@ @@ -1,84 +1,83 @@
1# $NetBSD: Makefile,v 1.121 2019/05/05 22:49:48 ryoon Exp $ 1# $NetBSD: Makefile,v 1.122 2019/05/23 10:55:07 jaapb Exp $
2# 2#
3 3
4DISTNAME= coq-8.9.0 4DISTNAME= coq-8.9.1
5PKGREVISION= 3 
6CATEGORIES= lang math 5CATEGORIES= lang math
7MASTER_SITES= ${MASTER_SITE_GITHUB:=coq/} 6MASTER_SITES= ${MASTER_SITE_GITHUB:=coq/}
8GITHUB_TAG= V${PKGVERSION_NOREV:S/_/+/} 7GITHUB_TAG= V${PKGVERSION_NOREV:S/_/+/}
9 8
10MAINTAINER= jaapb@NetBSD.org 9MAINTAINER= jaapb@NetBSD.org
11HOMEPAGE= http://coq.inria.fr/ 10HOMEPAGE= http://coq.inria.fr/
12COMMENT= Theorem prover which extracts programs from proofs 11COMMENT= Theorem prover which extracts programs from proofs
13LICENSE= gnu-lgpl-v2.1 12LICENSE= gnu-lgpl-v2.1
14 13
15WRKSRC= ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/_/-/} 14WRKSRC= ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/_/-/}
16 15
17USE_TOOLS+= gmake 16USE_TOOLS+= gmake
18HAS_CONFIGURE= yes 17HAS_CONFIGURE= yes
19CONFIGURE_ARGS+= -prefix ${PREFIX} 18CONFIGURE_ARGS+= -prefix ${PREFIX}
20#CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp 19#CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp
21CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR} 20CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR}
22CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq 21CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq
23CONFIGURE_ARGS+= -docdir ${PREFIX}/share/doc/coq 22CONFIGURE_ARGS+= -docdir ${PREFIX}/share/doc/coq
24CONFIGURE_ARGS+= -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq 23CONFIGURE_ARGS+= -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
25 24
26BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10 25BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
27 26
28.include "../../mk/bsd.prefs.mk" 27.include "../../mk/bsd.prefs.mk"
29.include "../../mk/ocaml.mk" 28.include "../../mk/ocaml.mk"
30 29
31PLIST_VARS+= native 30PLIST_VARS+= native
32.if ${OCAML_USE_OPT_COMPILER} == "yes" 31.if ${OCAML_USE_OPT_COMPILER} == "yes"
33PLIST_SUBST+= COQIDE_TYPE="opt" 32PLIST_SUBST+= COQIDE_TYPE="opt"
34PLIST.native= yes 33PLIST.native= yes
35CONFIGURE_ARGS+= -native-compiler yes 34CONFIGURE_ARGS+= -native-compiler yes
36UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this 35UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this
37BUILD_TARGET= world 36BUILD_TARGET= world
38.else 37.else
39PLIST_SUBST+= COQIDE_TYPE="byte" 38PLIST_SUBST+= COQIDE_TYPE="byte"
40CONFIGURE_ARGS+= -native-compiler no 39CONFIGURE_ARGS+= -native-compiler no
41BUILD_TARGET= byte 40BUILD_TARGET= byte
42INSTALL_TARGET= install-byte 41INSTALL_TARGET= install-byte
43.endif 42.endif
44 43
45.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64") 44.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
46. if !empty(MACHINE_PLATFORM:MLinux-*-*) || \ 45. if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
47 !empty(MACHINE_PLATFORM:MDragonFly-*-*) || \ 46 !empty(MACHINE_PLATFORM:MDragonFly-*-*) || \
48 !empty(MACHINE_PLATFORM:MFreeBSD-*-*) || \ 47 !empty(MACHINE_PLATFORM:MFreeBSD-*-*) || \
49 !empty(MACHINE_PLATFORM:MDarwin-*-*) || \ 48 !empty(MACHINE_PLATFORM:MDarwin-*-*) || \
50 !empty(MACHINE_PLATFORM:MNetBSD-*-*) 49 !empty(MACHINE_PLATFORM:MNetBSD-*-*)
51PLIST.natdynlink= yes 50PLIST.natdynlink= yes
52. endif 51. endif
53.endif 52.endif
54 53
55.include "../../lang/python/pyversion.mk" 54.include "../../lang/python/pyversion.mk"
56 55
57REPLACE_SH= configure install.sh 56REPLACE_SH= configure install.sh
58REPLACE_INTERPRETER= python 57REPLACE_INTERPRETER= python
59REPLACE.python.old= python 58REPLACE.python.old= python
60REPLACE.python.new= ${PYTHONBIN} 59REPLACE.python.new= ${PYTHONBIN}
61REPLACE_FILES.python= tools/TimeFileMaker.py \ 60REPLACE_FILES.python= tools/TimeFileMaker.py \
62 tools/make-both-single-timing-files.py \ 61 tools/make-both-single-timing-files.py \
63 tools/make-both-time-files.py \ 62 tools/make-both-time-files.py \
64 tools/make-one-time-file.py 63 tools/make-one-time-file.py
65 64
66INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR} 65INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
67 66
68PLIST_VARS+= coqide natdynlink doc 67PLIST_VARS+= coqide natdynlink doc
69 68
70.include "options.mk" 69.include "options.mk"
71 70
72EGDIR= ${PREFIX}/share/coq/examples 71EGDIR= ${PREFIX}/share/coq/examples
73#CONF_FILES= {EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc 72#CONF_FILES= {EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
74 73
75SUBST_CLASSES+= fix-paths 74SUBST_CLASSES+= fix-paths
76SUBST_STAGE.fix-paths= post-configure 75SUBST_STAGE.fix-paths= post-configure
77SUBST_MESSAGE.fix-paths= Remove buildlink references from Coq_config module 76SUBST_MESSAGE.fix-paths= Remove buildlink references from Coq_config module
78SUBST_FILES.fix-paths= config/coq_config.ml 77SUBST_FILES.fix-paths= config/coq_config.ml
79SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g" 78SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g"
80 79
81.include "../../lang/camlp5/buildlink3.mk" 80.include "../../lang/camlp5/buildlink3.mk"
82.include "../../math/ocaml-num/buildlink3.mk" 81.include "../../math/ocaml-num/buildlink3.mk"
83.include "../../mk/pthread.buildlink3.mk" 82.include "../../mk/pthread.buildlink3.mk"
84.include "../../mk/bsd.pkg.mk" 83.include "../../mk/bsd.pkg.mk"
cvs diff -r1.32 -r1.33 pkgsrc/lang/coq/distinfo (switch to unified diff)

--- pkgsrc/lang/coq/distinfo 2019/03/06 09:28:23 1.32
+++ pkgsrc/lang/coq/distinfo 2019/05/23 10:55:07 1.33
@@ -1,7 +1,7 @@ @@ -1,7 +1,7 @@
1$NetBSD: distinfo,v 1.32 2019/03/06 09:28:23 jaapb Exp $ 1$NetBSD: distinfo,v 1.33 2019/05/23 10:55:07 jaapb Exp $
2 2
3SHA1 (coq-8.9.0.tar.gz) = 8833deafd57649f875f15c0739c8ac1ffe06aeda 3SHA1 (coq-8.9.1.tar.gz) = d26646b33922bcd9eb44ef80162f8d0513784e46
4RMD160 (coq-8.9.0.tar.gz) = b587d945a5eb0366c7a7b280f1ff08940c800a60 4RMD160 (coq-8.9.1.tar.gz) = d82a0f7d31c0e5d7b8b566cd15d7ff9f724c250b
5SHA512 (coq-8.9.0.tar.gz) = 42b2e0ae669c06803b6b527a194d78675de18869f6342fc8afc49cfc94f3e98ca0c3b4fd52d3af8c5ce66c6efb1c665ac0d65e992ad29c3f432e244f98ec2ca1 5SHA512 (coq-8.9.1.tar.gz) = 66344f801b955d1b6daf3ab1d704551070c95cf9032ae74f15fb33f7ec313812b3e05c0ec277a2eb448e3fdfd9721df06d36612e2fb4928b6530d70147f1d983
6Size (coq-8.9.0.tar.gz) = 5992210 bytes 6Size (coq-8.9.1.tar.gz) = 6001970 bytes
7SHA1 (patch-Makefile.common) = f232485fddc61c51cd12ac5567b706f5f2299328 7SHA1 (patch-Makefile.common) = f232485fddc61c51cd12ac5567b706f5f2299328