kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Revbump because of ocaml 4.02, added compilation patch (already in

Browse source 
repository upstream) and updated package to use ocaml.mk framework.
This commit is contained in:
jaapb 2014-10-09 22:19:01 +00:00
parent 7c04b556a4
commit 4c03ebf068
4 changed files with 27 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
lang/coq/Makefile
View file

@ -1,8 +1,9 @@
# $NetBSD: Makefile,v 1.76 2014/10/07 16:47:28 adam Exp $
# $NetBSD: Makefile,v 1.77 2014/10/09 22:19:01 jaapb Exp $
#
DISTNAME= coq-8.4pl4
PKGREVISION= 1
PKGNAME= ${DISTNAME} # to avoid prefixing with ocaml-
PKGREVISION= 2
CATEGORIES= lang math
MASTER_SITES= http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
@ -24,11 +25,9 @@ BUILD_TARGET= world
BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
.include "../../mk/bsd.prefs.mk"
.include "../../mk/ocaml.mk"
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \
(${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64") || \
(${MACHINE_ARCH} == "arm")
PLIST.opt= yes
.if ${OCAML_USE_OPT_COMPILER} == "yes"
PLIST_SUBST+= COQIDE_TYPE="opt"
.else
PLIST_SUBST+= COQIDE_TYPE="byte"
@ -55,7 +54,7 @@ _STRIPFLAG_INSTALL=
REPLACE_SH= configure install.sh
INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
PLIST_VARS= coqide opt natdynlink doc
PLIST_VARS+= coqide natdynlink doc
.include "options.mk"
@ -63,6 +62,5 @@ EGDIR= ${PREFIX}/share/coq/examples
CONF_FILES= ${EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
.include "../../mk/pthread.buildlink3.mk"
.include "../../lang/ocaml/buildlink3.mk"
.include "../../lang/camlp5/buildlink3.mk"
.include "../../mk/bsd.pkg.mk"

10
lang/coq/PLIST
View file

@ -1,9 +1,9 @@
@comment $NetBSD: PLIST,v 1.14 2013/10/30 00:21:49 minskim Exp $
@comment $NetBSD: PLIST,v 1.15 2014/10/09 22:19:01 jaapb Exp $
bin/coq-tex
bin/coq_makefile
bin/coqc
bin/coqchk
${PLIST.opt}bin/coqchk.opt
${PLIST.ocaml-opt}bin/coqchk.opt
bin/coqdep
bin/coqdoc
${PLIST.coqide}bin/coqide
@ -11,7 +11,7 @@ ${PLIST.coqide}bin/coqide.${COQIDE_TYPE}
bin/coqmktop
bin/coqtop
bin/coqtop.byte
${PLIST.opt}bin/coqtop.opt
${PLIST.ocaml-opt}bin/coqtop.opt
bin/coqwc
bin/gallina
lib/coq/config/coq_config.cmi
@ -184,7 +184,7 @@ lib/coq/parsing/tactic_printer.cmi
lib/coq/parsing/tok.cmi
lib/coq/plugins/cc/cc_plugin.a
lib/coq/plugins/cc/cc_plugin.cma
${PLIST.opt}lib/coq/plugins/cc/cc_plugin.cmxa
${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.cmxa
${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
lib/coq/plugins/cc/cc_plugin_mod.cmi
lib/coq/plugins/cc/ccalgo.cmi
@ -196,7 +196,7 @@ lib/coq/plugins/decl_mode/decl_interp.cmi
lib/coq/plugins/decl_mode/decl_mode.cmi
lib/coq/plugins/decl_mode/decl_mode_plugin.a
lib/coq/plugins/decl_mode/decl_mode_plugin.cma
${PLIST.opt}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxa
${PLIST.ocaml-opt}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxa
${PLIST.natdynlink}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
lib/coq/plugins/decl_mode/decl_proof_instr.cmi

3
lang/coq/distinfo
View file

@ -1,6 +1,7 @@
$NetBSD: distinfo,v 1.19 2014/05/13 14:52:28 jaapb Exp $
$NetBSD: distinfo,v 1.20 2014/10/09 22:19:01 jaapb Exp $
SHA1 (coq-8.4pl4.tar.gz) = 4dfc3a1ae65f5c480ddc4387d21549a526183e00
RMD160 (coq-8.4pl4.tar.gz) = 19e3fe905f5db09710b1f862f21e9b57c28f9704
Size (coq-8.4pl4.tar.gz) = 4067355 bytes
SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4
SHA1 (patch-kernel_univ.ml) = 2208e539870d6793b807bae46e0955b5f814f3fc

14
lang/coq/patches/patch-kernel_univ.ml Normal file
View file

@ -0,0 +1,14 @@
$NetBSD: patch-kernel_univ.ml,v 1.1 2014/10/09 22:19:01 jaapb Exp $
Fix comment.
--- kernel/univ.ml.orig 2014-04-24 15:13:03.000000000 +0000
+++ kernel/univ.ml
@@ -226,7 +226,7 @@ let reprleq g arcu =
(* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
-(* between u v = {w|u<=w<=v, w canonical} *)
+(* between u v = { w | u<=w<=v, w canonical} *)
(* between is the most costly operation *)
let between g arcu arcv =