diff --git a/coq/Makefile b/coq/Makefile index 140fdd2d41..80d663022c 100644 --- a/coq/Makefile +++ b/coq/Makefile @@ -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" diff --git a/coq/PLIST b/coq/PLIST index 4898876d45..fa833ac5be 100644 --- a/coq/PLIST +++ b/coq/PLIST @@ -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 diff --git a/coq/distinfo b/coq/distinfo index 10bae9a156..2cd63e6b8a 100644 --- a/coq/distinfo +++ b/coq/distinfo @@ -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 diff --git a/coq/options.mk b/coq/options.mk index 6a7deb007e..103240f2a0 100644 --- a/coq/options.mk +++ b/coq/options.mk @@ -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 diff --git a/coq/patches/patch-Makefile.common b/coq/patches/patch-Makefile.common index fb60da1f81..d92820f9b1 100644 --- a/coq/patches/patch-Makefile.common +++ b/coq/patches/patch-Makefile.common @@ -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 diff --git a/coq/patches/patch-Makefile.ide b/coq/patches/patch-Makefile.ide deleted file mode 100644 index f5867f9840..0000000000 --- a/coq/patches/patch-Makefile.ide +++ /dev/null @@ -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 diff --git a/coq/patches/patch-configure.ml b/coq/patches/patch-configure.ml deleted file mode 100644 index 7924fbc7b7..0000000000 --- a/coq/patches/patch-configure.ml +++ /dev/null @@ -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 *) -