diff options
| author | Théo Zimmermann <theo.zimmermann@telecom-paris.fr> | 2026-01-16 10:12:05 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2026-01-16 10:12:05 +0000 |
| commit | dc351d25c35a5d896c5d61a3666ac256fcc33a40 (patch) | |
| tree | a39f651729cbbe3b30606c036606a0bcce1267d9 /doc | |
| parent | codex: 0.84.0 -> 0.86.0 (#480597) (diff) | |
| parent | coqPackages: add coqWithPackages/coqWithPackages' functions (diff) | |
| download | nixpkgs-dc351d25c35a5d896c5d61a3666ac256fcc33a40.tar.gz | |
coqPackages: add coqWithPackages/coqWithPackages' functions (#444257)
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/languages-frameworks/coq.section.md | 19 | ||||
| -rw-r--r-- | doc/redirects.json | 6 |
2 files changed, 25 insertions, 0 deletions
diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index f758d89d3269..0eab34d044e4 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/doc/languages-frameworks/coq.section.md @@ -10,6 +10,25 @@ The Coq derivation is overridable through the `coq.override overrides`, where ov The associated package set can be obtained using `mkCoqPackages coq`, where `coq` is the derivation to use. +## Creating custom Coq environments with `coq.withPackages` {#coq-withPackages} + +The `coq.withPackages` function provides a convenient way to create a Coq environment that includes additional Coq packages. This is similar to how `python.withPackages` works for Python environments. + +The function takes a function that receives the Coq package set and returns a list of packages. It returns a wrapped Coq environment where all Coq binaries (`coqtop`, `coqc`, `coqdep`, `coqchk`, `coqide`, etc.) are configured with the appropriate environment variables to find the packages. + +### Usage {#coq-withPackages-usage} + +Here is an example of creating a Coq environment with specific packages. + +```nix +coq.withPackages ( + ps: with ps; [ + mathcomp + bignums + ] +) +``` + ## Coq packages attribute sets: `coqPackages` {#coq-packages-attribute-sets-coqpackages} The recommended way of defining a derivation for a Coq library, is to use the `coqPackages.mkCoqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Coq libraries. The following attributes are supported: diff --git a/doc/redirects.json b/doc/redirects.json index 8e072af31e4e..cbff4ea2f226 100644 --- a/doc/redirects.json +++ b/doc/redirects.json @@ -20,6 +20,12 @@ "cmake-ctest-variables": [ "index.html#cmake-ctest-variables" ], + "coq-withPackages": [ + "index.html#coq-withPackages" + ], + "coq-withPackages-usage": [ + "index.html#coq-withPackages-usage" + ], "cuda": [ "index.html#cuda" ], |