Merge pull request #9765 from roconnor/master

Add csdp support for Micromega tactics in Coq.

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 = ''

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";
+  };
+}

pkgs/top-level/all-packages.nix

@@ -11037,6 +11037,8 @@ let
     desktopName = "Conkeror";
   };
 
+  csdp = callPackage ../applications/science/math/csdp { };
+
   cuneiform = builderDefsPackage (import ../tools/graphics/cuneiform) {
     inherit cmake patchelf;
     imagemagick = imagemagick;