13 files changed, 193 insertions, 100 deletions

diff --git a/doc/language-support.xml b/doc/language-support.xml
index 79b56c572d69..5e49121e695b 100644
--- a/doc/language-support.xml
+++ b/doc/language-support.xml
@@ -377,6 +377,42 @@ fileSystem = buildLuaPackage {
 
 </section>
 
+<section xml:id="ssec-language-coq"><title>Coq</title>
+  <para>
+    Coq libraries should be installed in
+    <literal>$(out)/lib/coq/${coq.coq-version}/user-contrib/</literal>.
+    Such directories are automatically added to the
+    <literal>$COQPATH</literal> environment variable by the hook defined
+    in the Coq derivation.
+  </para>
+  <para>
+    Some libraries require OCaml and sometimes also Camlp5. The exact
+    versions that were used to build Coq are saved in the
+    <literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
+    attributes.
+  </para>
+  <para>
+    Here is a simple package example. It is a pure Coq library, thus it
+    only depends on Coq. Its <literal>makefile</literal> has been
+    generated using <literal>coq_makefile</literal> so we only have to
+    set the <literal>$COQLIB</literal> variable at install time.
+  </para>
+  <programlisting>
+{stdenv, fetchurl, coq}:
+stdenv.mkDerivation {
+  src = fetchurl {
+    url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz;
+    sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1";
+  };
+
+  name = "coq-karatsuba";
+
+  buildInputs = [ coq ];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+}
+</programlisting>
+</section>
 
 <!--
 <section><title>Haskell</title>
diff --git a/lib/licenses.nix b/lib/licenses.nix
index 84710a69eb66..248447423b2b 100644
--- a/lib/licenses.nix
+++ b/lib/licenses.nix
@@ -82,6 +82,11 @@ rec {
     fullName = "Common Development and Distribution License 1.0";
   };
 
+  cecill-b = spdx {
+    shortName = "CECILL-B";
+    fullName  = "CeCILL-B Free Software License Agreement";
+  };
+
   cecill-c = spdx {
     shortName = "CECILL-C";
     fullName  = "CeCILL-C Free Software License Agreement";
diff --git a/pkgs/applications/editors/emacs-modes/proofgeneral/4.3pre.nix b/pkgs/applications/editors/emacs-modes/proofgeneral/4.3pre.nix
index 3a492dc0c7f4..32a036805edc 100644
--- a/pkgs/applications/editors/emacs-modes/proofgeneral/4.3pre.nix
+++ b/pkgs/applications/editors/emacs-modes/proofgeneral/4.3pre.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake }:
+{ stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake, enableDoc ? false }:
 
 stdenv.mkDerivation (rec {
   name = "ProofGeneral-4.3pre131011";
@@ -10,7 +10,7 @@ stdenv.mkDerivation (rec {
 
   sourceRoot = name;
 
-  buildInputs = [ emacs texinfo texLive perl which ];
+  buildInputs = [ emacs texinfo perl which ] ++ stdenv.lib.optional enableDoc texLive;
 
   prePatch =
     '' sed -i "Makefile" \
@@ -25,15 +25,20 @@ stdenv.mkDerivation (rec {
        sed -i '96d' doc/ProofGeneral.texi
     '';
 
+  patches = [ ./pg.patch ];
+
   preBuild = ''
     make clean;
   '';
 
   installPhase =
+    if enableDoc
+    then
     # Copy `texinfo.tex' in the right place so that `texi2pdf' works.
     '' cp -v "${automake}/share/"automake-*/texinfo.tex doc
        make install install-doc
-    '';
+    ''
+    else "make install";
 
   meta = {
     description = "Proof General, an Emacs front-end for proof assistants";
diff --git a/pkgs/applications/editors/emacs-modes/proofgeneral/pg.patch b/pkgs/applications/editors/emacs-modes/proofgeneral/pg.patch
new file mode 100644
index 000000000000..c733911118de
--- /dev/null
+++ b/pkgs/applications/editors/emacs-modes/proofgeneral/pg.patch
@@ -0,0 +1,16 @@
+diff -r c7d8bfff4c0a bin/proofgeneral
+--- a/bin/proofgeneral	Sat Sep 27 02:25:15 2014 +0100
++++ b/bin/proofgeneral	Sat Sep 27 02:28:16 2014 +0100
+@@ -73,11 +73,7 @@
+ 
+ # Try to find Proof General directory
+ if [ -z "$PGHOME" ] || [ ! -d "$PGHOME" ]; then
+-    # default relative to this script, otherwise PGHOMEDEFAULT
+-    MYDIR="`readlink --canonicalize "$0" | sed -ne 's,/bin/proofgeneral$,,p'`"
+-    if [ -d "$MYDIR" ]; then
+-	PGHOME="$MYDIR"
+-    elif [ -d "$PGHOMEDEFAULT" ]; then
++    if [ -d "$PGHOMEDEFAULT" ]; then
+ 	PGHOME="$PGHOMEDEFAULT"
+     else
+ 	echo "Cannot find the Proof General lisp files: Set PGHOME or use --pghome."
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;
   };
 }
diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
deleted file mode 100644
index a784e5fe1b6e..000000000000
--- a/pkgs/applications/science/logic/ssreflect/default.nix
+++ /dev/null
@@ -1,50 +0,0 @@
-# TODO:
-# - coq needs to be invoked with the explicit path to the ssreflect theory
-#   e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ ''
-
-{stdenv, fetchurl, ocaml, camlp5, coq, makeWrapper}:
-
-let
-  pname = "ssreflect";
-  version = "1.5";
-  name = "${pname}-${version}";
-  webpage = http://www.msr-inria.inria.fr/Projects/math-components;
-in
-
-stdenv.mkDerivation {
-  inherit name;
-
-  src = fetchurl {
-    url = "http://ssr.msr-inria.inria.fr/FTP/${name}.tar.gz";
-    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
-  };
-
-  buildInputs = [ ocaml camlp5 coq makeWrapper ];
-
-  patches = [ ./static.patch ];
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/ make -f Makefile.coq install -e
-    mkdir -p $out/bin
-    cp bin/* $out/bin
-    for i in $out/bin/*; do
-      wrapProgram "$i" \
-        --add-flags "-R" \
-        --add-flags "$out/lib/coq/user-contrib/Ssreflect" \
-        --add-flags "Ssreflect"
-    done
-    makeWrapper "${coq}/bin/coqide" "$out/bin/ssrcoqide" --add-flags "-coqtop" --add-flags "$out/bin/ssrcoq"
-  '';
-
-  meta = {
-    description = "Small Scale Reflection extension for Coq";
-    longDescription = ''
-      Small Scale Reflection (ssreflect) is an extension of the Coq Theorem
-      Prover which enable a formal proof methodology based on the pervasive
-      use of computation with symbolic representation
-    '';
-    homepage = webpage;
-    license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-  };
-}
diff --git a/pkgs/applications/science/logic/ssreflect/static.patch b/pkgs/applications/science/logic/ssreflect/static.patch
deleted file mode 100644
index 2211d8802582..000000000000
--- a/pkgs/applications/science/logic/ssreflect/static.patch
+++ /dev/null
@@ -1,21 +0,0 @@
---- ssreflect1.4-coq8.4/Make	(revision 3823)
-+++ ssreflect1.4-coq8.4/Make	(working copy)
-@@ -1,10 +1,10 @@
--### Uncomment for static linking
--##
--#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
--#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
--#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
--#SSRCOQ = bin/ssrcoq
--##
-+## Uncomment for static linking
-+#
-+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
-+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
-+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
-+SSRCOQ = bin/ssrcoq
-+#
- 
- ## What follows should be left untouched by the final user of ssreflect
- -R theories Ssreflect
-
diff --git a/pkgs/development/coq-modules/containers/default.nix b/pkgs/development/coq-modules/containers/default.nix
new file mode 100644
index 000000000000..9856ba6955fe
--- /dev/null
+++ b/pkgs/development/coq-modules/containers/default.nix
@@ -0,0 +1,24 @@
+{stdenv, fetchurl, coq}:
+
+stdenv.mkDerivation {
+
+  name = "coq-containers-${coq.coq-version}";
+
+  src = fetchurl {
+    url = http://coq.inria.fr/pylons/contribs/files/Containers/v8.4/Containers.tar.gz;
+    sha256 = "1y9x2lwrskv2231z9ac3kv4bmg6h1415xpp4gl7v5w90ba6p6w8w";
+  };
+
+  buildInputs = [ coq.ocaml coq.camlp5 ];
+  propagatedBuildInputs = [ coq ];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = with stdenv.lib; {
+    homepage = http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4;
+    description = "A typeclass-based Coq library of finite sets/maps";
+    maintainers = with maintainers; [ vbgl ];
+    platforms = coq.meta.platforms;
+  };
+
+}
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
new file mode 100644
index 000000000000..ca8bd6481efc
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -0,0 +1,24 @@
+{stdenv, fetchurl, coq, ssreflect}:
+
+stdenv.mkDerivation {
+
+  name = "coq-mathcomp-1.5";
+
+  src = fetchurl {
+    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
+    sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
+  };
+
+  propagatedBuildInputs = [ coq ssreflect ];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = with stdenv.lib; {
+    homepage = http://ssr.msr-inria.inria.fr/;
+    license = licenses.cecill-b;
+    maintainers = [ maintainers.vbgl ];
+    platforms = coq.meta.platforms;
+    hydraPlatforms = [];
+  };
+
+}
diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix
new file mode 100644
index 000000000000..912ff7071f8f
--- /dev/null
+++ b/pkgs/development/coq-modules/ssreflect/default.nix
@@ -0,0 +1,26 @@
+{stdenv, fetchurl, coq}:
+
+assert coq.coq-version == "8.4";
+
+stdenv.mkDerivation {
+
+  name = "coq-ssreflect-1.5";
+
+  src = fetchurl {
+    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz;
+    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
+  };
+
+  buildInputs = [ coq.ocaml coq.camlp5 ];
+  propagatedBuildInputs = [ coq ];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = with stdenv.lib; {
+    homepage = http://ssr.msr-inria.inria.fr/;
+    license = licenses.cecill-b;
+    maintainers = with maintainers; [ vbgl ];
+    platforms = coq.meta.platforms;
+  };
+
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index f8382928e0b9..65e33864e03f 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -11456,6 +11456,18 @@ let
     lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
   };
 
+  mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
+
+    containers = callPackage ../development/coq-modules/containers {};
+
+    mathcomp = callPackage ../development/coq-modules/mathcomp {};
+
+    ssreflect = callPackage ../development/coq-modules/ssreflect {};
+
+  };
+
+  coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);
+
   cvc3 = callPackage ../applications/science/logic/cvc3 {};
 
   ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
@@ -11525,10 +11537,6 @@ let
 
   spass = callPackage ../applications/science/logic/spass {};
 
-  ssreflect = callPackage ../applications/science/logic/ssreflect {
-    camlp5 = ocamlPackages.camlp5_transitional;
-  };
-
   tptp = callPackage ../applications/science/logic/tptp {};
 
   twelf = callPackage ../applications/science/logic/twelf {