Updatings ssreflect to depend on camlp5 version 6.

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

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

@@ -1,10 +1,16 @@
-# TODO:
+# - coqide compilation can be disabled by setting lablgtk to null;
-# - coqide compilation should be optional or (better) separate;
 
-{stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}:
+{stdenv, fetchurl, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
 
 let 
   version = "8.3pl4";
+  buildIde = lablgtk != null;
+  ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
+  idePatch = if buildIde then ''
+    substituteInPlace scripts/coqmktop.ml --replace \
+    "\"-I\"; \"+lablgtk2\"" \
+    "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
+  '' else "";
 in
 
 stdenv.mkDerivation {
@@ -21,9 +27,10 @@ stdenv.mkDerivation {
 
   preConfigure = ''
     configureFlagsArray=(
+      -opt
       -camldir ${ocaml}/bin
       -camlp5dir $(ocamlfind query camlp5)
-      -lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -opt -coqide opt
+      ${ideFlags}
     )
   '';
 
@@ -36,17 +43,16 @@ stdenv.mkDerivation {
     RM=$(type -tp rm)
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    substituteInPlace scripts/coqmktop.ml --replace \
+    ${idePatch}
-      "\"-I\"; \"+lablgtk2\"" \
-      "\"-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 = ''
+  # This will likely no longer be necessary for coq >= 8.4. -- roconnor
+  postInstall = if buildIde then ''
    cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
-  '';
+  '' else "";
 
   meta = {
     description = "Coq proof assistant";

pkgs/top-level/all-packages.nix

@@ -8298,7 +8298,7 @@ let
   spass = callPackage ../applications/science/logic/spass {};
 
   ssreflect = callPackage ../applications/science/logic/ssreflect {
-    camlp5 = ocamlPackages.camlp5_5_transitional;
+    camlp5 = ocamlPackages.camlp5_transitional;
   };
 
   tptp = callPackage ../applications/science/logic/tptp {};