update coq to 8.3pl1

update ssreflect to 1.3pl1

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

2 files changed, 13 insertions, 18 deletions

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 8556e975de3b..fcd342e0b594 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -4,7 +4,7 @@
 {stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}:
 
 let
-  version = "8.3";
+  version = "8.3pl1";
 in
 
 stdenv.mkDerivation {
@@ -12,7 +12,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "02iy4rxz1n1kc85fb3vs4xpxqfxjw87y2gvmi39fxrj8742qx0dx";
+    sha256 = "0a791gsbf17y2wi0a376n78pxkhpl0lkzifhy5d3mx3lpn376j9s";
   };
 
   buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
@@ -29,7 +29,7 @@ stdenv.mkDerivation {
 
   buildFlags = "world"; # Debug with "world VERBOSE=1";
 
-  patches = [ ./configure.patch ./coq-8.3-make-3.82-compat.patch ];
+  patches = [ ./configure.patch ];
 
   postPatch = ''
     UNAME=$(type -tp uname)
@@ -41,6 +41,9 @@ stdenv.mkDerivation {
       "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
   '';
 
+  # This post install step is needed to build ssrcoqide from the ssreflect package
+  # It could be made optional, but I see little harm in including it in the default
+  # distribution -- roconnor
   postInstall = ''
    cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
   '';
diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
index 61901d545d7a..5a51fe2136a1 100644
--- a/pkgs/applications/science/logic/ssreflect/default.nix
+++ b/pkgs/applications/science/logic/ssreflect/default.nix
@@ -1,13 +1,12 @@
 # TODO:
-# - ssrcoqide does not build successfully (missing coqide libraries in the coq installation).
-# - ssrcoq needs to be invoked with the explicit path to the ssreflect theory
-#   e.g.. ssrcoq -I /nix/store/rp09dlb2y2hpddb0xa7fyrgjlzb284ar-ssreflect-1.2/lib/coq/user-contrib/theories/
+# - coq needs to be invoked with the explicit path to the ssreflect theory
+#   e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ ''
 
 {stdenv, fetchurl, ocaml, camlp5, coq}:
 
 let
   pname = "ssreflect";
-  version = "1.2";
+  version = "1.3pl1";
   name = "${pname}-${version}";
   webpage = http://www.msr-inria.inria.fr/Projects/math-components;
 in
@@ -16,18 +15,12 @@ stdenv.mkDerivation {
   inherit name;
 
   src = fetchurl {
-    url = "${webpage}/${name}.tgz";
-    sha256 = "0800b085e6a0caec5093c6c02aacdd8dfd9cc282177e8586f14f9a9e15f64d0b";
+    url = "${webpage}/${name}.tar.gz";
+    sha256 = "0ykrhqb68aanl5d4dmn0vnx8m34gg0jsbdhwx2852rqi7r00b9ri";
   };
 
   buildInputs = [ ocaml camlp5 coq ];
 
-  preBuild = ''
-    coq_makefile -f Make -o Makefile
-    substituteInPlace Makefile \
-      --replace 'install -D $$i $(COQLIB)' 'install -D $$i '$out'/lib/coq'
-  '';
-
   # this fails
   /*
   postBuild = ''
@@ -36,10 +29,9 @@ stdenv.mkDerivation {
   '';
   */
 
-  postInstall = ''
+  installPhase = ''
+    COQLIB=$out/lib/coq make -f Makefile.coq install -e
     ensureDir $out/bin
-    #cp -a bin/ssrcoq bin/ssrcoqide $out/bin
-    cp -a bin/ssrcoq $out/bin
   '';
 
   meta = {