Update Coq

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

pkgs/applications/science/logic/coq/8.3rc1.nix

@@ -1,53 +0,0 @@
-# TODO:
-# - coqide compilation should be optional or (better) separate;
-# - coqide libraries are not installed;
-
-{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
-
-stdenv.mkDerivation {
-  name = "coq-devel-8.3pre1";
-
-  src = fetchurl {
-    url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
-    sha256 = "0r43dqr7nzjfkxlz4963sj18gvjni6x3lhrlgh4l8k0cjspi62sj";
-  };
-
-  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
-
-  patches = [ ./coq-8.3-rc1_configure.patch ];
-
-  postPatch = ''
-    substituteInPlace scripts/coqmktop.ml --replace \
-      "\"-I\"; \"+lablgtk2\"" \
-      "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
-  '';
-
-  prefixKey = "-prefix ";
-
-  preConfigure = ''
-    ARCH=`uname -s`
-    CAMLDIR=`type -p ocamlc`
-  '';
-
-  configureFlags =
-    "-arch $ARCH " +
-    "-camldir $CAMLDIR " +
-    "-camldir ${ocaml}/bin " +
-    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
-    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
-    "-opt -coqide opt";
-
-  buildFlags = "world"; # Debug with "world VERBOSE=1";
-
-  meta = {
-    description = "Coq proof assistant (development version)";
-    longDescription = ''
-      Coq is a formal proof management system.  It provides a formal language
-      to write mathematical definitions, executable algorithms and theorems
-      together with an environment for semi-interactive development of
-      machine-checked proofs.
-    '';
-    homepage = "http://coq.inria.fr";
-    license = "LGPL";
-  };
-}

pkgs/applications/science/logic/coq/configure.patch

@@ -1,7 +1,7 @@
-diff -Nuar coq-8.3-rc1/configure coq-8.3-rc1.nixos/configure
---- coq-8.3-rc1/configure	2010-08-06 10:36:16.000000000 +0200
-+++ coq-8.3-rc1.nixos/configure	2010-09-14 20:30:02.000000000 +0200
-@@ -399,7 +399,6 @@
+diff -Nuar coq-8.3/configure coq-8.3.nixos/configure
+--- coq-8.3/configure	2010-10-14 16:02:46.000000000 +0200
++++ coq-8.3.nixos/configure	2010-11-04 09:57:16.000000000 +0100
+@@ -394,7 +394,6 @@
  	 ocamlyaccexec=$CAMLBIN/ocamlyacc
  	 ocamlmktopexec=$CAMLBIN/ocamlmktop
  	 ocamlmklibexec=$CAMLBIN/ocamlmklib
@@ -9,7 +9,7 @@ diff -Nuar coq-8.3-rc1/configure coq-8.3-rc1.nixos/configure
  esac
  
  if test ! -f "$CAMLC" ; then
-@@ -647,7 +646,7 @@
+@@ -637,7 +636,7 @@
              no)  LABLGTKLIB=+lablgtk2                   # Pour le message
                   LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
              yes) LABLGTKLIB="$lablgtkdir"               # Pour le message

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

@@ -4,7 +4,7 @@
 {stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
 
 let
-  version = "8.2pl2";
+  version = "8.3";
 in
 
 stdenv.mkDerivation {
@@ -12,7 +12,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "0dh2vv3bvz8694dd12kjdkdaq19l1vslvygzif11igshc5bw4rhf";
+    sha256 = "02iy4rxz1n1kc85fb3vs4xpxqfxjw87y2gvmi39fxrj8742qx0dx";
   };
 
   buildInputs = [ ocaml camlp5 ncurses lablgtk ];
@@ -27,21 +27,13 @@ stdenv.mkDerivation {
 
   buildFlags = "world"; # Debug with "world VERBOSE=1";
 
-  patches = [ ./configure.patch.gz ];
+  patches = [ ./configure.patch ];
 
   postPatch = ''
-    BASH=$(type -tp bash)
     UNAME=$(type -tp uname)
-    MV=$(type -tp mv)
     RM=$(type -tp rm)
-    substituteInPlace configure --replace "/bin/bash" "$BASH" \
-                                --replace "/bin/uname" "$UNAME"
-    substituteInPlace Makefile --replace "/bin/bash" "$BASH" \
-                               --replace "/bin/mv" "$MV" \
-                               --replace "/bin/rm" "$RM"
-    substituteInPlace Makefile.stage1 --replace "/bin/bash" "$BASH"
-    substituteInPlace install.sh --replace "/bin/bash" "$BASH"
-    substituteInPlace dev/v8-syntax/check-grammar --replace "/bin/bash" "$BASH"
+    substituteInPlace configure --replace "/bin/uname" "$UNAME"
+    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
     substituteInPlace scripts/coqmktop.ml --replace \
       "\"-I\"; \"+lablgtk2\"" \
       "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""

pkgs/top-level/all-packages.nix

@@ -6836,10 +6836,6 @@ let
     camlp5 = camlp5_transitional;
   };
 
-  coq_devel = callPackage ../applications/science/logic/coq/8.3rc1.nix {
-    camlp5 = camlp5_transitional;
-  };
-
   eprover = callPackage ../applications/science/logic/eProver {
     texLive = texLiveAggregationFun {
       paths = [