Updated Coq to version 8.2pl1

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

2 files changed, 54 insertions, 11 deletions

diff --git a/pkgs/applications/science/logic/coq/configure.patch.gz b/pkgs/applications/science/logic/coq/configure.patch.gz
new file mode 100644
index 000000000000..85ecfda6dae1
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/configure.patch.gz
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 475c68f7b9cf..19827022072d 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -1,23 +1,66 @@
-{stdenv, fetchurl, ocaml, ncurses}:
+# TODO:
+# - coqide compilation should be optional or (better) separate;
+# - coqide libraries are not installed;
 
-stdenv.mkDerivation (rec {
+{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
+
+let
+
+  pname = "coq";
+  version = "8.2pl1";
+  name = "${pname}-${version}";
+
+in
+
+stdenv.mkDerivation {
+  inherit name;
 
-  name = "coq-8.1pl3";
   src = fetchurl {
-    url = "http://coq.inria.fr/V8.1pl3/files/coq-8.1pl3.tar.gz";
-    sha256 = "7f8f45594adff2625312c5ecb144cb00d39c99201dac309c9286b34d01a36bb6";
+    url = "http://coq.inria.fr/V${version}/files/${name}.tar.gz";
+    sha256 = "7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c";
   };
 
-  buildInputs = [ocaml ncurses];
+  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
 
   prefixKey = "-prefix ";
-  patchPhase = ''
+
+  configureFlags =
+    "-camldir ${ocaml}/bin " +
+    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
+    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
+    "-opt -coqide opt";
+
+  buildFlags = "world"; # Debug with "world VERBOSE=1";
+
+  patches = [ ./configure.patch.gz ];
+
+  postPatch = ''
+    BASH=$(type -tp bash)
     UNAME=$(type -tp uname)
     MV=$(type -tp mv)
-    RM=$(type -tp cp)
-    substituteInPlace ./configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace Makefile --replace "/bin/mv" "$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 scripts/coqmktop.ml --replace \
+      "\"-I\"; \"+lablgtk2\"" \
+      "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
   '';
 
-})
+  meta = {
+    description = "Coq proof assistant";
+    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";
+  };
+}