coq: Add csdp dependency

The csdp program is invoked for some uses of Micromega tactics.

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

@@ -1,6 +1,9 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
+# - The csdp program used for the Micromega tactic is statically referenced.
+#   However, coq can build without csdp by setting it to null.
+#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
 
-{ stdenv, make, fetchurl, ocaml, findlib, camlp5, ncurses, lablgtk ? null }:
+{ stdenv, make, fetchurl, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null }:
 
 let 
   version = "8.3pl4";
@@ -11,6 +14,10 @@ let
     "\"-I\"; \"+lablgtk2\"" \
     "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
   '' else "";
+  csdpPatch = if csdp != null then ''
+    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
+    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.search_exe_in_path \"csdp\"" "Some \"${csdp}/bin/csdp\""
+  '' else "";
 in
 
 stdenv.mkDerivation {
@@ -44,6 +51,7 @@ stdenv.mkDerivation {
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
     ${idePatch}
+    ${csdpPatch}
   '';
 
   # This post install step is needed to build ssrcoqide from the ssreflect package

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

@@ -1,12 +1,19 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
+# - The csdp program used for the Micromega tactic is statically referenced.
+#   However, coq can build without csdp by setting it to null.
+#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
 
-{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
 
 let
   version = "8.5b2";
   coq-version = "8.5";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
+  csdpPatch = if csdp != null then ''
+    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
+    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
+  '' else "";
 in
 
 stdenv.mkDerivation {
@@ -28,6 +35,7 @@ stdenv.mkDerivation {
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
     substituteInPlace Makefile.build --replace "ifeq (\$(ARCH),Darwin)" "ifeq (\$(ARCH),Darwinx)"
+    ${csdpPatch}
   '';
 
   setupHook = writeText "setupHook.sh" ''

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

@@ -1,12 +1,19 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
+# - The csdp program used for the Micromega tactic is statically referenced.
+#   However, coq can build without csdp by setting it to null.
+#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
 
-{stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
 
 let
   version = "8.5pre-0c999f02";
   coq-version = "8.5";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
+  csdpPatch = if csdp != null then ''
+    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
+    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
+  '' else "";
 in
 
 stdenv.mkDerivation {
@@ -31,6 +38,7 @@ stdenv.mkDerivation {
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
     substituteInPlace Makefile.build --replace "ifeq (\$(ARCH),Darwin)" "ifeq (\$(ARCH),Darwinx)"
+    ${csdpPatch}
   '';
 
   setupHook = writeText "setupHook.sh" ''

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

@@ -1,12 +1,19 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
+# - The csdp program used for the Micromega tactic is statically referenced.
+#   However, coq can build without csdp by setting it to null.
+#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
 
-{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
 
 let
   version = "8.4pl6";
   coq-version = "8.4";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
+  csdpPatch = if csdp != null then ''
+    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
+    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
+  '' else "";
 in
 
 stdenv.mkDerivation {
@@ -29,6 +36,7 @@ stdenv.mkDerivation {
     RM=$(type -tp rm)
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
+    ${csdpPatch}
   '';
 
   preConfigure = ''