diff options
author | Mx Kookie <kookie@spacekookie.de> | 2020-12-09 18:55:19 +0000 |
---|---|---|
committer | Mx Kookie <kookie@spacekookie.de> | 2020-12-09 18:55:19 +0000 |
commit | 80d90d9b204f7c17912740f9f414fe5d59f293ba (patch) | |
tree | 5f2065a06e724270610760d59d01c6888b375a46 /infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md | |
parent | 3a31a84c7d3e589035ad08499206aac44a81f424 (diff) | |
parent | 83cbad92d73216bb0d9187c56cce0b91f9121d5a (diff) |
Merge commit '83cbad92d73216bb0d9187c56cce0b91f9121d5a' into main
Diffstat (limited to 'infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md')
-rw-r--r-- | infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md b/infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md new file mode 100644 index 000000000000..714e84efc8db --- /dev/null +++ b/infra/libkookie/nixpkgs/doc/languages-frameworks/coq.section.md @@ -0,0 +1,40 @@ +# Coq {#sec-language-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 extensions (plugins) might require OCaml and sometimes other OCaml packages. The `coq.ocamlPackages` attribute can be used to depend on the same package set Coq was built against. + +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. + +```nix +{ 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" ]; + }; +} +``` |