diff options
Diffstat (limited to 'pkgs/applications/science/logic/coq/default.nix')
| -rw-r--r-- | pkgs/applications/science/logic/coq/default.nix | 10 |
1 files changed, 9 insertions, 1 deletions
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 = '' |