coqPackages: update documentation
This commit is contained in:
parent
4c454a3208
commit
5642f4ac6f
|
@ -11,31 +11,53 @@
|
||||||
in the Coq derivation.
|
in the Coq derivation.
|
||||||
</para>
|
</para>
|
||||||
<para>
|
<para>
|
||||||
Some libraries require OCaml and sometimes also Camlp5. The exact
|
Some libraries require OCaml and sometimes also Camlp5 or findlib.
|
||||||
versions that were used to build Coq are saved in the
|
The exact versions that were used to build Coq are saved in the
|
||||||
<literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
|
<literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
|
||||||
attributes.
|
and <literal>coq.findlib</literal> attributes.
|
||||||
|
</para>
|
||||||
|
<para>
|
||||||
|
Coq libraries may be compatible with some specific versions of Coq only.
|
||||||
|
The <liberal>compatibleCoqVersions</liberal> attribute is used to
|
||||||
|
precisely select those versions of Coq that are compatible with this
|
||||||
|
derivation.
|
||||||
</para>
|
</para>
|
||||||
<para>
|
<para>
|
||||||
Here is a simple package example. It is a pure Coq library, thus it
|
Here is a simple package example. It is a pure Coq library, thus it
|
||||||
only depends on Coq. Its <literal>makefile</literal> has been
|
depends on Coq. It builds on the Mathematical Components library, thus it
|
||||||
generated using <literal>coq_makefile</literal> so we only have to
|
also takes <literal>mathcomp</literal> as <literal>buildInputs</literal>.
|
||||||
|
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.
|
set the <literal>$COQLIB</literal> variable at install time.
|
||||||
</para>
|
</para>
|
||||||
<programlisting>
|
<programlisting>
|
||||||
{stdenv, fetchurl, coq}:
|
{ stdenv, fetchFromGitHub, coq, mathcomp }:
|
||||||
stdenv.mkDerivation {
|
|
||||||
src = fetchurl {
|
stdenv.mkDerivation rec {
|
||||||
url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz;
|
name = "coq${coq.coq-version}-multinomials-${version}";
|
||||||
sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1";
|
version = "1.0";
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "math-comp";
|
||||||
|
repo = "multinomials";
|
||||||
|
rev = version;
|
||||||
|
sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
|
||||||
};
|
};
|
||||||
|
|
||||||
name = "coq-karatsuba";
|
|
||||||
|
|
||||||
buildInputs = [ coq ];
|
buildInputs = [ coq ];
|
||||||
|
propagatedBuildInputs = [ mathcomp ];
|
||||||
|
|
||||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
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" ];
|
||||||
|
};
|
||||||
}
|
}
|
||||||
</programlisting>
|
</programlisting>
|
||||||
</section>
|
</section>
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue