diff options
| author | Tom McLaughlin <tom@codedown.io> | 2025-09-18 17:53:09 -0700 |
|---|---|---|
| committer | Tom McLaughlin <tom@codedown.io> | 2026-01-13 23:43:00 -0800 |
| commit | a776193f6bc7a9bc8c21ebb35e2e52e542cf3ea8 (patch) | |
| tree | 6b498c76b4491ef007715fdff1a24c6d75340f41 /doc/languages-frameworks | |
| parent | dylib: init at 3.0.1 (#476097) (diff) | |
| download | nixpkgs-a776193f6bc7a9bc8c21ebb35e2e52e542cf3ea8.tar.gz | |
coqPackages: add coqWithPackages/coqWithPackages' functions
Diffstat (limited to 'doc/languages-frameworks')
| -rw-r--r-- | doc/languages-frameworks/coq.section.md | 19 |
1 files changed, 19 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: |