Merge staging-next into staging (c5829b03) · Commits · nix / nixpkgs

doc/languages-frameworks/coq.section.md

+19 −0

Original line number	Diff line number	Diff line
		@@ -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:

+6 −0

Original line number	Diff line number	Diff line
		@@ -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"
		],

+0 −11

Original line number	Diff line number	Diff line
		@@ -181,17 +181,6 @@ with lib.maintainers;
		github = "cuda-maintainers";
		};

		cyberus = {
		# Verify additions by approval of an already existing member of the team.
		members = [
		xanderio
		snu
		e1mo
		];
		scope = "Team for Cyberus Technology employees who collectively maintain packages.";
		shortName = "Cyberus Technology employees";
		};

		danklinux = {
		members = [
		luckshiba

+4 −1

Original line number	Diff line number	Diff line
		@@ -629,6 +629,9 @@ in
		};

		meta = {
		maintainers = lib.teams.cyberus.members;
		maintainers = with lib.maintainers; [
		e1mo
		xanderio
		];
		};
		}

+4 −1

Original line number	Diff line number	Diff line
		@@ -330,6 +330,9 @@ in
		];
		};

		meta.maintainers = teams.cyberus.members;
		meta.maintainers = with lib.maintainers; [
		e1mo
		xanderio
		];
		meta.doc = ./plausible.md;
		}