# Coq

Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.

Some libraries require OCaml and sometimes also Camlp5 or findlib. The exact versions that were used to build Coq are saved in the `coq.ocaml` and `coq.camlp5` and `coq.findlib` attributes.

Coq libraries may be compatible with some specific versions of Coq only. The `compatibleCoqVersions` attribute is used to precisely select those versions of Coq that are compatible with this derivation.

Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes `mathcomp` as `buildInputs`. Its `Makefile` has been generated using `coq_makefile` so we only have to set the `$COQLIB` variable at install time.

    { stdenv, fetchFromGitHub, coq, mathcomp }:

    stdenv.mkDerivation rec {
      name = "coq${coq.coq-version}-multinomials-${version}";
      version = "1.0";
      src = fetchFromGitHub {
        owner = "math-comp";
        repo = "multinomials";
        rev = version;
        sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
      };

      buildInputs = [ coq ];
      propagatedBuildInputs = [ mathcomp ];

      installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";

      meta = {
        description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
        inherit (src.meta) homepage;
        license = stdenv.lib.licenses.cecill-b;
        inherit (coq.meta) platforms;
      };

      passthru = {
        compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
      };
    }