Fix building of Coq and update to version 8.3pl3. (Forgot to save files)

svn path=/nixpkgs/trunk/; revision=33195

pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch

@@ -1,84 +0,0 @@
-From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000)
-Subject: Fix mixed implicit and normal rules
-X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85
-
-Fix mixed implicit and normal rules
-
-This fixes build with GNU Make 3.82. See threads:
-
-  https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
-  http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
-
-git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7
----
-
-diff --git a/Makefile b/Makefile
-index b1edc01..ea73c51 100644
---- a/Makefile
-+++ b/Makefile
-@@ -160,9 +160,19 @@ else
- stage1 $(STAGE1_TARGETS) : always
- 	$(call stage-template,1)
- 
-+ifneq (,$(STAGE1_IMPLICITS))
-+$(STAGE1_IMPLICITS) : always
-+	$(call stage-template,1)
-+endif
-+
- stage2 $(STAGE2_TARGETS) : stage1
- 	$(call stage-template,2)
- 
-+ifneq (,$(STAGE2_IMPLICITS))
-+$(STAGE2_IMPLICITS) : stage1
-+	$(call stage-template,2)
-+endif
-+
- # Nota:
- # - world is one of the targets in $(STAGE2_TARGETS), hence launching
- # "make" or "make world" leads to recursion into stage1 then stage2
-diff --git a/Makefile.common b/Makefile.common
-index cc38980..46bf217 100644
---- a/Makefile.common
-+++ b/Makefile.common
-@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
- 
- SOURCEDOCDIR=dev/source-doc
- 
--CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
-+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
- 
- ### Targets forwarded by Makefile to a specific stage:
- 
-@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
- STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
-   $(GENFILES) \
-   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
--  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
-+  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
-+
-+STAGE1_IMPLICITS:=
- 
- ifdef CM_STAGE1
-- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
-+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
- endif
- 
- ## Enumeration of targets that require being done at stage2
-@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
-   printers debug initplugins plugins \
-   world install coqide coqide-files coq coqlib \
-   coqlight states check init theories theories-light \
--  $(DOC_TARGETS) $(VO_TARGETS) validate \
--  %.vo %.glob states/% install-% %.ml4-preprocessed \
-+  $(DOC_TARGETS) $(VO_TARGETS) validate
-+
-+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
-   $(DOC_TARGET_PATTERNS)
- 
- ifndef CM_STAGE1
-- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
-+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
- endif
- 
- 

pkgs/applications/science/logic/coq/default.nix

@@ -29,8 +29,7 @@ stdenv.mkDerivation {
 
   buildFlags = "world"; # Debug with "world VERBOSE=1";
 
-  #patches = [ ./configure.patch ./coq-8.3-make-3.82-compat.patch ];
-  patches = [ /root/configure.patch ];
+  patches = [ ./configure.patch ];
 
   postPatch = ''
     UNAME=$(type -tp uname)