From 772ec9cae31f1037df1687e3fc83660b699835d6 Mon Sep 17 00:00:00 2001
From: Russell O'Connor <oconnorr@google.com>
Date: Tue, 8 Sep 2015 18:23:24 -0400
Subject: [PATCH 1/2] csdp: init at 6.1.1

---
 .../science/math/csdp/default.nix             | 27 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 ++
 2 files changed, 29 insertions(+)
 create mode 100644 pkgs/applications/science/math/csdp/default.nix

diff --git a/pkgs/applications/science/math/csdp/default.nix b/pkgs/applications/science/math/csdp/default.nix
new file mode 100644
index 000000000000..64fa4579949d
--- /dev/null
+++ b/pkgs/applications/science/math/csdp/default.nix
@@ -0,0 +1,27 @@
+{ lib, stdenv, fetchurl, blas, gfortran, liblapack }:
+
+stdenv.mkDerivation {
+  name = "csdp-6.1.1";
+
+  src = fetchurl {
+    url = "http://www.coin-or.org/download/source/Csdp/Csdp-6.1.1.tgz";
+    sha256 = "1f9ql6cjy2gwiyc51ylfan24v1ca9sjajxkbhszlds1lqmma8n05";
+  };
+
+  buildInputs = [ blas gfortran liblapack ];
+
+  postPatch = ''
+    substituteInPlace Makefile --replace /usr/local/bin $out/bin
+  '';
+
+  preInstall = ''
+    mkdir -p $out/bin
+  '';
+
+  meta = {
+    homepage = https://projects.coin-or.org/Csdp;
+    license = lib.licenses.cpl10;
+    maintainers = [ lib.maintainers.roconnor ];
+    description = "A C Library for Semidefinite Programming";
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 94079eaac043..f102d1f95420 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -11031,6 +11031,8 @@ let
     desktopName = "Conkeror";
   };
 
+  csdp = callPackage ../applications/science/math/csdp { };
+
   cuneiform = builderDefsPackage (import ../tools/graphics/cuneiform) {
     inherit cmake patchelf;
     imagemagick = imagemagick;

From 4cc5f5dbb6db6b17f5346cc601b364f758600083 Mon Sep 17 00:00:00 2001
From: Russell O'Connor <oconnorr@google.com>
Date: Wed, 9 Sep 2015 23:43:31 -0400
Subject: [PATCH 2/2] coq: Add csdp dependency The csdp program is invoked for
 some uses of Micromega tactics.

---
 pkgs/applications/science/logic/coq/8.3.nix     | 10 +++++++++-
 pkgs/applications/science/logic/coq/8.5.nix     | 10 +++++++++-
 pkgs/applications/science/logic/coq/HEAD.nix    | 10 +++++++++-
 pkgs/applications/science/logic/coq/default.nix | 10 +++++++++-
 4 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix
index c59c4b062708..adae2dd067a3 100644
--- a/pkgs/applications/science/logic/coq/8.3.nix
+++ b/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
diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix
index 87b476249f44..2afa18d40a4b 100644
--- a/pkgs/applications/science/logic/coq/8.5.nix
+++ b/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" ''
diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix
index 7b5d1ce62b4e..3656b5cab191 100644
--- a/pkgs/applications/science/logic/coq/HEAD.nix
+++ b/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" ''
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 5a8fa9ff4dc1..38ba14e83cf8 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/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 = ''