coq: setup-hook for libraries

Adds a hook to automatically populate the $COQPATH variable.
Coq libraries are expected to be installed in

    lib/coq/${coq-version}/user-contrib/

3 files changed, 42 insertions, 22 deletions

diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix
index f23622de8a03..8664b822cca7 100644
--- a/pkgs/applications/science/logic/coq/8.3.nix
+++ b/pkgs/applications/science/logic/coq/8.3.nix
@@ -54,7 +54,7 @@ stdenv.mkDerivation {
    cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
   '' else "";
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "Coq proof assistant";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
@@ -63,7 +63,7 @@ stdenv.mkDerivation {
       machine-checked proofs.
     '';
     homepage = "http://coq.inria.fr";
-    license = "LGPL";
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
+    license = licenses.lgpl21;
+    maintainers = with maintainers; [ roconnor vbgl ];
   };
 }
diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix
index c76e563ff5f8..4081465fbd27 100644
--- a/pkgs/applications/science/logic/coq/HEAD.nix
+++ b/pkgs/applications/science/logic/coq/HEAD.nix
@@ -1,19 +1,20 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
 
-{stdenv, fetchgit, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{stdenv, fetchgit, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
 
 let 
   version = "8.5pre-01feb42";
+  coq-version = "8.5";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  idePath = if buildIde then ''
-    CAML_LD_LIBRARY_PATH=${lablgtk}/lib/ocaml/3.12.1/site-lib/stublibs
-  '' else "";
 in
 
 stdenv.mkDerivation {
   name = "coq-${version}";
 
+  inherit coq-version;
+  inherit ocaml camlp5;
+
   src = fetchgit {
     url = git://scm.gforge.inria.fr/coq/coq.git;
     rev = "01feb4206d26b41bfaab9bd45a7b2fc4db569baf";
@@ -32,8 +33,17 @@ stdenv.mkDerivation {
     substituteInPlace Makefile.build --replace "ifeq (\$(ARCH),Darwin)" "ifeq (\$(ARCH),Darwinx)"
   '';
 
+  setupHook = writeText "setupHook.sh" ''
+    addCoqPath () {
+      if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
+        export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
+      fi
+    }
+
+    envHooks=(''${envHooks[@]} addCoqPath)
+  '';
+
   preConfigure = ''
-    buildFlagsArray=(${idePath})
     configureFlagsArray=(
       -opt
       ${ideFlags}
@@ -44,7 +54,7 @@ stdenv.mkDerivation {
 
   buildFlags = "revision coq coqide";
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "Coq proof assistant";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
@@ -53,8 +63,8 @@ stdenv.mkDerivation {
       machine-checked proofs.
     '';
     homepage = "http://coq.inria.fr";
-    license = "LGPL";
-    maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
-    platforms = stdenv.lib.platforms.unix;
+    license = licenses.lgpl21;
+    maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
+    platforms = platforms.unix;
   };
 }
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index da77a4c5a9aa..f0f62bfb3537 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -1,19 +1,20 @@
 # - coqide compilation can be disabled by setting lablgtk to null;
 
-{stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
 
-let 
+let
   version = "8.4pl4";
+  coq-version = "8.4";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  idePath = if buildIde then ''
-    CAML_LD_LIBRARY_PATH=${lablgtk}/lib/ocaml/3.12.1/site-lib/stublibs
-  '' else "";
 in
 
 stdenv.mkDerivation {
   name = "coq-${version}";
 
+  inherit coq-version;
+  inherit ocaml camlp5;
+
   src = fetchurl {
     url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
     sha256 = "00bzf4kfbd0g279jrr8ynzvb9wqcly3wi577bkrxivhrg2msxhq6";
@@ -31,7 +32,6 @@ stdenv.mkDerivation {
   '';
 
   preConfigure = ''
-    buildFlagsArray=(${idePath})
     configureFlagsArray=(
       -opt
       -camldir ${ocaml}/bin
@@ -44,7 +44,17 @@ stdenv.mkDerivation {
 
   buildFlags = "revision coq coqide";
 
-  meta = {
+  setupHook = writeText "setupHook.sh" ''
+    addCoqPath () {
+      if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
+        export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
+      fi
+    }
+
+    envHooks=(''${envHooks[@]} addCoqPath)
+  '';
+
+  meta = with stdenv.lib; {
     description = "Formal proof management system";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
@@ -53,8 +63,8 @@ stdenv.mkDerivation {
       machine-checked proofs.
     '';
     homepage = "http://coq.inria.fr";
-    license = "LGPL";
-    maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
-    platforms = stdenv.lib.platforms.unix;
+    license = licenses.lgpl21;
+    maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
+    platforms = platforms.unix;
   };
 }