edc9ce12d3
Changes from V8.4pl3 to V8.4pl4 =============================== WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B. For more details, see: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD or https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD Kernel - Unsound check of elimination sort. - Fix guard condition for nested cofixpoints. - Univ constraints of module subtyping were not propagated. Tactics - A new option "Set Stable Omega" ensures that repeated identical calls to omega will produce identical proof terms. This option is off by default for maximal compatibility, but should be pretty safe to activate. - The interpretation of the open_constr tactic argument was erroneously firing type classes resolution in some corner cases. This has been fixed. The tactic argument type open_constr_wTC is provided for retro compatibility purposes. - Fixing bug (fixing precedence of ltac variables over variables in env) introduces rare and justified tactic failure. Bug fixes - micromega: solved an ambiguous symbol resolution. - Coq always uses / as separator between directories on all platforms. - remove trailing '\r' from file names returned by coqtop. - bug correction in proving inversion principles for Function. - ocamlbuild: minor fixes related to camlp4 and cross-compilation. Changes from V8.4pl2 to V8.4pl3 =============================== Ide_slave XML interface - 20120712, 20130419 : Invalidated protocol versions - From 20130419 extra datastructure : union (Inl "" = <union val="in_l"><string></string></union>, Inr _ = <union val="in_r">...) - 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not handle by coqide v8.4. A message has a level and a content (of string). Message levels are Debug of string, Info, Notice, Warning and Error. - 20130425 : * new toplevel entry : feedback, once again not send by coqtop v8.4 and not handle by coqide v8.4. A feedback gives the id of the sentence it provides info about and a content. Feedback contents are Processed, AddedAxiom and GlobRef of Util.loc * string * string * string * string * <call val="interp"> must provide an attribute id of type int. It is OK in coqtop v8.4 to alwais send <call val="interp" id="0"> Bug fixes - Fixing a significant efficiency leak in the code of the field tactic. - Fix caching of local hint database in typeclasses eauto which could miss some hypotheses. - Fix automatic solving of obligation in program, which was not trying to solve obligations that had no undefined dependencies left.
67 lines
2 KiB
Makefile
67 lines
2 KiB
Makefile
# $NetBSD: Makefile,v 1.75 2014/05/13 14:52:28 jaapb Exp $
|
|
#
|
|
|
|
DISTNAME= coq-8.4pl4
|
|
CATEGORIES= lang math
|
|
MASTER_SITES= http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
|
|
|
|
MAINTAINER= jaapb@NetBSD.org
|
|
HOMEPAGE= http://coq.inria.fr/
|
|
COMMENT= Theorem prover which extracts programs from proofs
|
|
LICENSE= gnu-lgpl-v2.1
|
|
|
|
USE_TOOLS+= gmake
|
|
HAS_CONFIGURE= yes
|
|
CONFIGURE_ARGS+= -prefix ${PREFIX}
|
|
CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp
|
|
CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR}
|
|
CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq
|
|
CONFIGURE_ARGS+= -docdir ${PREFIX}/share/doc/coq
|
|
CONFIGURE_ARGS+= -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
|
|
BUILD_TARGET= world
|
|
|
|
BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
|
|
|
|
.include "../../mk/bsd.prefs.mk"
|
|
|
|
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \
|
|
(${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64") || \
|
|
(${MACHINE_ARCH} == "arm")
|
|
PLIST.opt= yes
|
|
PLIST_SUBST+= COQIDE_TYPE="opt"
|
|
.else
|
|
PLIST_SUBST+= COQIDE_TYPE="byte"
|
|
.endif
|
|
|
|
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
|
|
. if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
|
|
!empty(MACHINE_PLATFORM:MDragonFly-*-*) || \
|
|
!empty(MACHINE_PLATFORM:MFreeBSD-*-*) || \
|
|
!empty(MACHINE_PLATFORM:MDarwin-*-*) || \
|
|
!empty(MACHINE_PLATFORM:MNetBSD-*-*)
|
|
PLIST.natdynlink= yes
|
|
. endif
|
|
.endif
|
|
|
|
.if ${OPSYS} == "Darwin"
|
|
INSTALL_UNSTRIPPED= yes
|
|
# See PR# 28772 as the above should work but it appears to be ignored
|
|
# so we set it explicitly below not to stip installed binaries.
|
|
_STRIPFLAG_CC=
|
|
_STRIPFLAG_INSTALL=
|
|
.endif
|
|
|
|
REPLACE_SH= configure install.sh
|
|
INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
|
|
|
|
PLIST_VARS= coqide opt natdynlink doc
|
|
|
|
.include "options.mk"
|
|
|
|
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"
|