rtyler
/
pkgsrc-wip
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Synchronised with pkgsrc, updated coq to 8.11+beta1

This commit is contained in:
Jaap Boender 2020-01-24 16:03:29 +01:00
parent f0704352b0
commit 370094edf4
7 changed files with 81 additions and 129 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
coq/Makefile
View File

@ -1,13 +1,13 @@
# $NetBSD: Makefile,v 1.121 2019/05/05 22:49:48 ryoon Exp $
# $NetBSD: Makefile,v 1.128 2020/01/24 15:54:48 jaapb Exp $
#
DISTNAME= coq-8.10+beta1
DISTNAME= coq-8.11+beta1
CATEGORIES= lang math
MASTER_SITES= ${MASTER_SITE_GITHUB:=coq/}
GITHUB_TAG= V${PKGVERSION_NOREV:S/_/+/}
MAINTAINER= jaapb@NetBSD.org
HOMEPAGE= http://coq.inria.fr/
HOMEPAGE= https://coq.inria.fr/
COMMENT= Theorem prover which extracts programs from proofs
LICENSE= gnu-lgpl-v2.1
@ -28,20 +28,20 @@ BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
.include "../../mk/bsd.prefs.mk"
.include "../../mk/ocaml.mk"
PLIST_VARS+= native
PLIST_VARS+= native
.if ${OCAML_USE_OPT_COMPILER} == "yes"
COQIDE_TYPE= opt
PLIST.native= yes
COQIDE_TYPE= opt
PLIST.native= yes
CONFIGURE_ARGS+= -native-compiler yes
UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this
BUILD_TARGET= world
BUILD_TARGET= world
.else
COQIDE_TYPE= byte
COQIDE_TYPE= byte
CONFIGURE_ARGS+= -native-compiler no
BUILD_TARGET= byte
INSTALL_TARGET= install-byte
BUILD_TARGET= byte
INSTALL_TARGET= install-byte
.endif
PLIST_SUBST+= COQIDE_TYPE=${COQIDE_TYPE}
PLIST_SUBST+= COQIDE_TYPE=${COQIDE_TYPE}
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
. if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
@ -55,14 +55,14 @@ PLIST.natdynlink= yes
.include "../../lang/python/pyversion.mk"
REPLACE_SH= configure install.sh
REPLACE_SH= configure install.sh
REPLACE_INTERPRETER= python
REPLACE.python.old= python
REPLACE.python.old= python3
REPLACE.python.new= ${PYTHONBIN}
REPLACE_FILES.python= tools/TimeFileMaker.py \
tools/make-both-single-timing-files.py \
tools/make-both-time-files.py \
tools/make-one-time-file.py
tools/make-both-single-timing-files.py \
tools/make-both-time-files.py \
tools/make-one-time-file.py
INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
@ -73,11 +73,11 @@ PLIST_VARS+= coqide natdynlink doc
EGDIR= ${PREFIX}/share/coq/examples
#CONF_FILES= {EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
SUBST_CLASSES+= fix-paths
SUBST_STAGE.fix-paths= post-configure
SUBST_CLASSES+= fix-paths
SUBST_STAGE.fix-paths= post-configure
SUBST_MESSAGE.fix-paths= Remove buildlink references from Coq_config module
SUBST_FILES.fix-paths= config/coq_config.ml
SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g"
SUBST_FILES.fix-paths= config/coq_config.ml
SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g"
.include "../../math/ocaml-num/buildlink3.mk"
.include "../../mk/pthread.buildlink3.mk"

10
coq/PLIST
View File

@ -1,4 +1,4 @@
@comment $NetBSD: PLIST,v 1.29 2019/03/06 09:28:23 jaapb Exp $
@comment $NetBSD: PLIST,v 1.30 2020/01/24 15:54:48 jaapb Exp $
bin/coq-tex
bin/coq_makefile
bin/coqc
@ -134,6 +134,7 @@ lib/coq/engine/univops.cmi
${PLIST.ocaml-opt}lib/coq/engine/univops.cmx
${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.a
lib/coq/gramlib/.pack/gramlib.cmi
${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmx
${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmxa
lib/coq/gramlib/.pack/gramlib__Gramext.cmi
${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Gramext.cmx
@ -517,6 +518,10 @@ lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
@ -577,6 +582,9 @@ lib/coq/plugins/extraction/ExtrHaskellZInteger.vo
lib/coq/plugins/extraction/ExtrHaskellZNum.glob
lib/coq/plugins/extraction/ExtrHaskellZNum.v
lib/coq/plugins/extraction/ExtrHaskellZNum.vo
lib/coq/plugins/extraction/ExtrOCamlInt63.glob
lib/coq/plugins/extraction/ExtrOCamlInt63.v
lib/coq/plugins/extraction/ExtrOCamlInt63.vo
lib/coq/plugins/extraction/ExtrOcamlBasic.glob
lib/coq/plugins/extraction/ExtrOcamlBasic.v
lib/coq/plugins/extraction/ExtrOcamlBasic.vo

14
coq/distinfo
View File

@ -1,9 +1,7 @@
$NetBSD: distinfo,v 1.32 2019/03/06 09:28:23 jaapb Exp $
$NetBSD: distinfo,v 1.35 2020/01/24 15:54:48 jaapb Exp $
SHA1 (coq-8.10+beta1.tar.gz) = d6e9d8e0acd31aa7ffc8fb7ca9be8dcc7166d7b1
RMD160 (coq-8.10+beta1.tar.gz) = e1d20986be73eed2b33394e1ddc04d5d7cca1e75
SHA512 (coq-8.10+beta1.tar.gz) = dcbab2cd76d06d3efbddcae774f061383eddcf8b193b7822c084efbc89d0cd568ec60f67d56adaa0c770b69aa785b49724ef0116af0d1c5f7654355c4956affd
Size (coq-8.10+beta1.tar.gz) = 6200493 bytes
SHA1 (patch-Makefile.common) = f232485fddc61c51cd12ac5567b706f5f2299328
SHA1 (patch-Makefile.ide) = d89329524d2c3d917399bffbc4f59d3538ae21d1
SHA1 (patch-configure.ml) = c4cbfa2039edd5d5d72acd91f315829a14b4fa2d
SHA1 (coq-8.11+beta1.tar.gz) = 3c2a882534417817eb5cefebf58edbb5bbd82470
RMD160 (coq-8.11+beta1.tar.gz) = c932bb68f73623d5542603f3ce7f259dc360e7a7
SHA512 (coq-8.11+beta1.tar.gz) = bcb3b63e80795e44b94591eefb2caa1a2f3782dff8ba592606dd8c30160b1f2c8dfcbc78127a058fd8af6c8dc33346ff4ec2c03593c71659ed5b53a7516af516
Size (coq-8.11+beta1.tar.gz) = 6544784 bytes
SHA1 (patch-Makefile.common) = 85bcb271103f87f1e1573d3856740319ee0344cd

88
coq/options.mk
View File

@ -1,57 +1,57 @@
# $NetBSD: options.mk,v 1.6 2019/04/26 12:44:43 roy Exp $
# $NetBSD: options.mk,v 1.9 2020/01/24 15:54:48 jaapb Exp $
PKG_OPTIONS_VAR= PKG_OPTIONS.coq
PKG_SUPPORTED_OPTIONS= doc coqide
PKG_SUGGESTED_OPTIONS= coqide
PKG_OPTIONS_VAR= PKG_OPTIONS.coq
PKG_SUPPORTED_OPTIONS= doc coqide
PKG_SUGGESTED_OPTIONS= coqide
.include "../../mk/bsd.options.mk"
.if !empty(PKG_OPTIONS:Mdoc)
PYTHON_VERSIONS_INCOMPATIBLE= 27
CONFIGURE_ARGS+= -with-doc yes
PLIST.doc= yes
BUILD_DEPENDS+= tex-latex-bin-[0-9]*:../../print/tex-latex-bin
BUILD_DEPENDS+= hevea>=1.10:../../textproc/hevea
BUILD_DEPENDS+= tex-moreverb-[0-9]*:../../print/tex-moreverb
BUILD_DEPENDS+= tex-preprint-[0-9]*:../../print/tex-preprint
BUILD_DEPENDS+= tex-ucs-[0-9]*:../../print/tex-ucs
BUILD_DEPENDS+= py[0-9]*-sphinx-[0-9]*:../../textproc/py-sphinx
BUILD_DEPENDS+= py[0-9]*-sphinx-rtd-theme-[0-9]*:../../textproc/py-sphinx-rtd-theme
BUILD_DEPENDS+= py[0-9]*-sphinxcontrib-bibtex-[0-9]*:../../textproc/py-sphinxcontrib-bibtex
BUILD_DEPENDS+= py[0-9]*-pybtex-[0-9]*:../../textproc/py-pybtex
BUILD_DEPENDS+= py[0-9]*-pybtex-docutils-[0-9]*:../../textproc/py-pybtex-docutils
BUILD_DEPENDS+= py[0-9]*-pexpect-[0-9]*:../../devel/py-pexpect
BUILD_DEPENDS+= py[0-9]*-antlr4-[0-9]*:../../textproc/py-antlr4
BUILD_DEPENDS+= py[0-9]*-beautifulsoup4-[0-9]*:../../www/py-beautifulsoup4
BUILD_DEPENDS+= latexmk-[0-9]*:../../print/latexmk
BUILD_DEPENDS+= tex-xetex-[0-9]*:../../print/tex-xetex
BUILD_DEPENDS+= tex-polyglossia-[0-9]*:../../print/tex-polyglossia
BUILD_DEPENDS+= tex-fncychap-[0-9]*:../../print/tex-fncychap
BUILD_DEPENDS+= tex-tabulary-[0-9]*:../../print/tex-tabulary
BUILD_DEPENDS+= tex-varwidth-[0-9]*:../../print/tex-varwidth
BUILD_DEPENDS+= tex-parskip-[0-9]*:../../print/tex-parskip
BUILD_DEPENDS+= tex-upquote-[0-9]*:../../print/tex-upquote
BUILD_DEPENDS+= tex-capt-of-[0-9]*:../../print/tex-capt-of
BUILD_DEPENDS+= tex-needspace-[0-9]*:../../print/tex-needspace
BUILD_DEPENDS+= tex-unicode-math-[0-9]*:../../math/tex-unicode-math
BUILD_DEPENDS+= tex-microtype-[0-9]*:../../print/tex-microtype
BUILD_DEPENDS+= tex-adjustbox-[0-9]*:../../print/tex-adjustbox
BUILD_DEPENDS+= tex-xindy-[0-9]*:../../textproc/tex-xindy
BUILD_DEPENDS+= tex-ec-[0-9]*:../../fonts/tex-ec
BUILD_DEPENDS+= tex-xcolor-[0-9]*:../../print/tex-xcolor
BUILD_DEPENDS+= tex-xkeyval-[0-9]*:../../print/tex-xkeyval
BUILD_DEPENDS+= tex-titlesec-[0-9]*:../../print/tex-titlesec
BUILD_DEPENDS+= tex-framed-[0-9]*:../../print/tex-framed
BUILD_DEPENDS+= tex-float-[0-9]*:../../print/tex-float
BUILD_DEPENDS+= tex-wrapfig-[0-9]*:../../print/tex-wrapfig
BUILD_DEPENDS+= tex-lm-math-[0-9]*:../../fonts/tex-lm-math
BUILD_DEPENDS+= dvipsk-[0-9]*:../../print/dvipsk
CONFIGURE_ARGS+= -with-doc yes
PLIST.doc= yes
BUILD_DEPENDS+= tex-latex-bin-[0-9]*:../../print/tex-latex-bin
BUILD_DEPENDS+= hevea>=1.10:../../textproc/hevea
BUILD_DEPENDS+= tex-moreverb-[0-9]*:../../print/tex-moreverb
BUILD_DEPENDS+= tex-preprint-[0-9]*:../../print/tex-preprint
BUILD_DEPENDS+= tex-ucs-[0-9]*:../../print/tex-ucs
BUILD_DEPENDS+= py[0-9]*-sphinx-[0-9]*:../../textproc/py-sphinx
BUILD_DEPENDS+= py[0-9]*-sphinx-rtd-theme-[0-9]*:../../textproc/py-sphinx-rtd-theme
BUILD_DEPENDS+= py[0-9]*-sphinxcontrib-bibtex-[0-9]*:../../textproc/py-sphinxcontrib-bibtex
BUILD_DEPENDS+= py[0-9]*-pybtex-[0-9]*:../../textproc/py-pybtex
BUILD_DEPENDS+= py[0-9]*-pybtex-docutils-[0-9]*:../../textproc/py-pybtex-docutils
BUILD_DEPENDS+= py[0-9]*-pexpect-[0-9]*:../../devel/py-pexpect
BUILD_DEPENDS+= py[0-9]*-antlr4-[0-9]*:../../textproc/py-antlr4
BUILD_DEPENDS+= py[0-9]*-beautifulsoup4-[0-9]*:../../www/py-beautifulsoup4
BUILD_DEPENDS+= latexmk-[0-9]*:../../print/latexmk
BUILD_DEPENDS+= tex-xetex-[0-9]*:../../print/tex-xetex
BUILD_DEPENDS+= tex-polyglossia-[0-9]*:../../print/tex-polyglossia
BUILD_DEPENDS+= tex-fncychap-[0-9]*:../../print/tex-fncychap
BUILD_DEPENDS+= tex-tabulary-[0-9]*:../../print/tex-tabulary
BUILD_DEPENDS+= tex-varwidth-[0-9]*:../../print/tex-varwidth
BUILD_DEPENDS+= tex-parskip-[0-9]*:../../print/tex-parskip
BUILD_DEPENDS+= tex-upquote-[0-9]*:../../print/tex-upquote
BUILD_DEPENDS+= tex-capt-of-[0-9]*:../../print/tex-capt-of
BUILD_DEPENDS+= tex-needspace-[0-9]*:../../print/tex-needspace
BUILD_DEPENDS+= tex-unicode-math-[0-9]*:../../math/tex-unicode-math
BUILD_DEPENDS+= tex-microtype-[0-9]*:../../print/tex-microtype
BUILD_DEPENDS+= tex-adjustbox-[0-9]*:../../print/tex-adjustbox
BUILD_DEPENDS+= tex-xindy-[0-9]*:../../textproc/tex-xindy
BUILD_DEPENDS+= tex-ec-[0-9]*:../../fonts/tex-ec
BUILD_DEPENDS+= tex-xcolor-[0-9]*:../../print/tex-xcolor
BUILD_DEPENDS+= tex-xkeyval-[0-9]*:../../print/tex-xkeyval
BUILD_DEPENDS+= tex-titlesec-[0-9]*:../../print/tex-titlesec
BUILD_DEPENDS+= tex-framed-[0-9]*:../../print/tex-framed
BUILD_DEPENDS+= tex-float-[0-9]*:../../print/tex-float
BUILD_DEPENDS+= tex-wrapfig-[0-9]*:../../print/tex-wrapfig
BUILD_DEPENDS+= tex-lm-math-[0-9]*:../../fonts/tex-lm-math
BUILD_DEPENDS+= dvipsk-[0-9]*:../../print/dvipsk
.else
CONFIGURE_ARGS+= -with-doc no
CONFIGURE_ARGS+= -with-doc no
.endif
.if !empty(PKG_OPTIONS:Mcoqide)
.include "../../wip/ocaml-lablgtk3/buildlink3.mk"
.include "../../x11/ocaml-lablgtk3/buildlink3.mk"
.include "../../x11/gtk3/buildlink3.mk"
CONFIGURE_ARGS+= -coqide ${COQIDE_TYPE}
PLIST.coqide= yes

3
coq/patches/patch-Makefile.common
View File

@ -1,6 +1,7 @@
$NetBSD: patch-Makefile.common,v 1.5 2019/03/06 09:28:23 jaapb Exp $
$NetBSD: patch-Makefile.common,v 1.6 2020/01/24 15:54:48 jaapb Exp $
Use BSD_INSTALL_*
--- Makefile.common.orig 2018-10-31 12:53:51.000000000 +0000
+++ Makefile.common
@@ -83,8 +83,8 @@ DYNOBJ:=.cmo

41
coq/patches/patch-Makefile.ide
View File

@ -1,41 +0,0 @@
$NetBSD$
Correct package name for lablgtk3
--- Makefile.ide.orig 2019-05-14 14:52:16.000000000 +0000
+++ Makefile.ide
@@ -43,7 +43,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/prot
ifeq ($(HASCOQIDE),no)
COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS))
else
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3-sourceview3
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3.sourceview3
endif
IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
@@ -106,7 +106,7 @@ ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 -linkall $(IDEFLAGS:.cma=.cmxa) $^
+ -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 -linkall $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
else
$(COQIDE): $(COQIDEBYTE)
@@ -116,7 +116,7 @@ endif
$(COQIDEBYTE): $(LINKIDE)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+ -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
@rm -f $@
@@ -245,7 +245,7 @@ $(COQIDEAPP)/Contents:
$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
+ -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents

14
coq/patches/patch-configure.ml
View File

@ -1,14 +0,0 @@
$NetBSD$
Correct lablgtk3 detection
--- configure.ml.orig 2019-05-14 14:52:16.000000000 +0000
+++ configure.ml
@@ -703,7 +703,7 @@ let numlib =
(** Detect and/or verify the Lablgtk3 location *)
let get_lablgtkdir () =
- tryrun camlexec.find ["query";"lablgtk3-sourceview3"]
+ tryrun camlexec.find ["query";"lablgtk3.sourceview3"]
(** Detect and/or verify the Lablgtk2 version *)