Rocq - Revision history

Gugo: subtitle typo

2026-07-25T15:27:19Z

subtitle typo

← Older revision		Revision as of 15:27, 25 July 2026
Line 29:		Line 29:
	In the same way of ''rocqPackages'', a ''coqPackages'' packages set is available to go with the ''coq'' compatibility package.		In the same way of ''rocqPackages'', a ''coqPackages'' packages set is available to go with the ''coq'' compatibility package.

	== RocqIDE		== RocqIDE ==

	Using the RocqIDE can be done by adding a flag to the ''coq'' compatibility package asking to also build the IDE. Here is a command spawning a nix shell having the IDE and running it (last tested in July 2026, on nixpkgs 26.05):		Using the RocqIDE can be done by adding a flag to the ''coq'' compatibility package asking to also build the IDE. Here is a command spawning a nix shell having the IDE and running it (last tested in July 2026, on nixpkgs 26.05):

Gugo: Update for nixpkgs 26.05

2026-07-20T09:37:20Z

Update for nixpkgs 26.05

← Older revision		Revision as of 09:37, 20 July 2026
Line 1:		Line 1:
	[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [~~nixpkgs manual](~~https://nixos.org/manual/nixpkgs/unstable/#sec-language-rocq) for more information about using Rocq with Nix.		[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [https://nixos.org/manual/nixpkgs/unstable/#sec-language-rocq nixpkgs manual] for more information about using Rocq with Nix.

	{{Cleanup\|reason=Probably don't want to recommend nix-env -iA}}		{{Cleanup\|reason=Probably don't want to recommend nix-env -iA}}
Line 5:		Line 5:
	== Installation ==		== Installation ==

	Rocq and associated tools (~~coqtop~~, ~~coqc~~, ~~coq_makefile~~, …) may be ~~installed~~ globally, by a user, in its profile:		Rocq and associated tools (repl, checker, makefile generator, compiler, …) may be install globally, by a user, in its profile:

			<code>nix-env -iA nixpkgs.rocq-core</code>

			Rocq can also be run in a local, ephemeral, environment. For instance, the following command will launch the Rocq repl without installing it in the user profile:

			<code>nix-shell -p rocq-core --command "rocq top"</code>

			You will probably also want the standard library (Stdlib) for Rocq containing definitions and lemmas about lists, relations, numbers, … It can be done by using the ''rocqPackages'' package set:

			<code>nix-env -iA nixpkgs.rocqPackages.stdlib</code>

			More details about libraries can be found in the [[Rocq#Using libraries\|Using libraries]]

			<em>The ''rocq-core'' package can also be installed using ''rocqPackages.rocq-core''.</em>

			== Coq compatibility ==

			In order to keep the compatibility with preexisting tools, compilation pipelines and workflows, the ''coq'' package is still available with its associated tools being aliases to the new Rocq variants (e.g. ''coqc'' corresponding to ''rocq compile''). This compatibility package can be installed via:

	<code>nix-env -iA nixpkgs.coq</code>		<code>nix-env -iA nixpkgs.coq</code>

	~~If you want CoqIDE:~~		In the same way of ''rocqPackages'', a ''coqPackages'' packages set is available to go with the ''coq'' compatibility package.

	~~<code>nix-env -iA nixpkgs.~~coqPackages.~~coqide</code>~~

	~~Coq can also be run in a local, ephemeral, environment. For instance, the following command will launch coqtop or CoqIDE without installing it in the user profile:~~		== RocqIDE

	~~<code>~~nix-shell ~~-p coq -c coqtop</code>~~		Using the RocqIDE can be done by adding a flag to the ''coq'' compatibility package asking to also build the IDE. Here is a command spawning a nix shell having the IDE and running it (last tested in July 2026, on nixpkgs 26.05):

	<code>nix-shell -p ~~coqPackages~~.~~coqide~~ -~~c coqide~~</code>		<code>nix-shell -p "coq.override { buildIde = true; }" --command rocqide</code>

	== ProofGeneral ==		== ProofGeneral ==
Line 41:		Line 57:
	== Using libraries ==		== Using libraries ==

	A few third-party libraries are available under the ''~~coqPackages~~'' attribute set.		A few third-party libraries are available under the ''rocqPackages'' attribute set.

	A simple way to use such a library is within a temporary shell, e.g.,		A simple way to use such a library is within a temporary shell, e.g.,

	<code>nix-shell --packages ~~coq coqPackages~~.mathcomp</code>		<code>nix-shell --packages rocqPackages.rocq-core rocqPackages.stdlib rocqPackages.mathcomp</code>

	This will open a shell in which both ~~Coq~~ and the [https://math-comp.github.io/math-comp/ Mathematical Components library] are available. Notice that even if ~~Coq~~ is globally installed, it is required to list it as an input of the shell.		This will open a shell in which both Rocq and the [https://math-comp.github.io/math-comp/ Mathematical Components library] are available. Notice that even if Rocq is globally installed, it is required to list it as an input of the shell.

	=== Using non-default versions of packaged libraries ===		=== Using non-default versions of packaged libraries ===

	For some libraries, several versions are available in nixpkgs. However, there is a default one and accessing non-default versions is non trivial. For instance, at the time of writing (~~February 2024~~, ~~nixos 23~~.11) <code>~~coqPackages~~.mathcomp</code> refers to the mathcomp library at version 1.18.0 (for Coq 8.18). An other version of this library may be accessed by overriding its <code>version</code> argument, as follows: <code>~~coqPackages~~.mathcomp.override { version = "2.1.0"; }</code>.		For some libraries, several versions are available in nixpkgs. However, there is a default one and accessing non-default versions is non trivial. For instance, at the time of writing (July 2026, nixpkgs 26.05) <code>rocqPackages.mathcomp</code> refers to the mathcomp library at version 2.5.0 (for Coq 9.1). An other version of this library may be accessed by overriding its <code>version</code> argument, as follows: <code>ocqPackages.mathcomp.override { version = "mathcomp-2.6.0"; }</code> with ''mathcomp-2.6.0'' being the [https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.6.0 tag name of a release on the Mathcomp GitHub repo].

	In more complex situations, it may be necessary to override several packages, or to use an overridden package as input to an other one. In order to get a consistent set of ~~Coq~~ libraries, one can use the <code>overrideScope'</code> function; for instance <code>~~coqPackages~~.overrideScope' (self: super: { mathcomp = super.mathcomp.override { version = "2.1.0"; }; })</code> is a set of ~~Coq~~ packages in which mathcomp is at version 2.1.0 (i.e., any package in this set that uses mathcomp will use that version).		In more complex situations, it may be necessary to override several packages, or to use an overridden package as input to an other one. In order to get a consistent set of Rocq libraries, one can use the <code>overrideScope</code> function; for instance <code>rocqPackages.overrideScope (self: super: { mathcomp = super.mathcomp.override { version = "mathcomp-2.6.0"; }; })</code> is a set of Rocq packages in which ''mathcomp'' is at version 2.6.0 (i.e., any package in this set that uses ''mathcomp'' will use that version).

	=== Global installation of libraries ===		=== Global installation of libraries ===

	It is possible to globally install a ~~Coq~~ library as any other Nix package. Notice however that it will not be automatically visible to ~~Coq~~. ~~Coq search~~ for libraries in the directories that are listed in the ''COQPATH'' environment variable. When using ~~Coq~~ in a Nix shell (as described above), this variable is automatically populated with paths to the ~~Coq~~ libraries that are provided by the shell inputs. You may manually define this variable to point to your profile, e.g.,		It is possible to globally install a Rocq library as any other Nix package. Notice however that it will not be automatically visible to Rocq. Rocq searches for libraries in the directories that are listed in the ''ROCQPATH'' (or ''COQPATH'' for compatibility) environment variable. When using Rocq in a Nix shell (as described above), this variable is automatically populated with paths to the Rocq libraries that are provided by the shell inputs. You may manually define this variable to point to your profile, e.g.,

	<code>export ~~COQPATH~~=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export ROCQPATH=$HOME/.nix-profile/lib/coq/9.1/user-contrib</code>

	== See also ==		== See also ==

Arch is the best: Link to nixpkgs manual, add cleanup notice

2026-05-29T00:06:47Z

Link to nixpkgs manual, add cleanup notice

← Older revision		Revision as of 00:06, 29 May 2026
Line 1:		Line 1:
			[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [nixpkgs manual](https://nixos.org/manual/nixpkgs/unstable/#sec-language-rocq) for more information about using Rocq with Nix.

			{{Cleanup\|reason=Probably don't want to recommend nix-env -iA}}

	== Installation ==		== Installation ==

	~~The [https://rocq-prover.org/~~ Rocq ~~proof assistant] (formerly known as Coq)~~ and associated tools (coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:		Rocq and associated tools (coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:

	<code>nix-env -iA nixpkgs.coq</code>		<code>nix-env -iA nixpkgs.coq</code>
Line 57:		Line 61:
	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

	== See ~~also…~~ ==		== See also ==

	Related blog post: https://yannherklotz.com/nix-for-coq/		Related blog post: https://yannherklotz.com/nix-for-coq/

	[[Category:Applications]]		[[Category:Applications]]

Arch is the best: Update Rocq website URL

2026-05-28T23:04:50Z

Update Rocq website URL

← Older revision		Revision as of 23:04, 28 May 2026
Line 1:		Line 1:
	== Installation ==		== Installation ==

	The [https://~~coq~~.~~inria.fr Coq~~ proof assistant] and associated tools (coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:		The [https://rocq-prover.org/ Rocq proof assistant] (formerly known as Coq) and associated tools (coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:

	<code>nix-env -iA nixpkgs.coq</code>		<code>nix-env -iA nixpkgs.coq</code>

Arch is the best: Arch is the best moved page Coq to Rocq: Software was renamed

2026-05-28T21:58:11Z

Arch is the best moved page Coq to Rocq: Software was renamed

← Older revision		Revision as of 21:58, 28 May 2026
(No difference)

imported>Tora0101: Update to current environment

2024-03-11T09:41:14Z

Update to current environment

← Older revision		Revision as of 09:41, 11 March 2024
Line 1:		Line 1:
	== Installation ==		== Installation ==

	The [https://coq.inria.fr Coq proof assistant] and associated tools (~~CoqIDE,~~ coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:		The [https://coq.inria.fr Coq proof assistant] and associated tools (coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:

	<code>nix-env -iA nixpkgs.coq</code>		<code>nix-env -iA nixpkgs.coq</code>

	~~Coq can also be run in a local, ephemeral, environment. For instance, the following command will launch~~ CoqIDE ~~without installing it~~:		If you want CoqIDE:

	<code>nix-shell --~~packages coq~~ --~~run~~ coqide</code>		<code>nix-env -iA nixpkgs.coqPackages.coqide</code>

			Coq can also be run in a local, ephemeral, environment. For instance, the following command will launch coqtop or CoqIDE without installing it in the user profile:

			<code>nix-shell -p coq -c coqtop</code>

			<code>nix-shell -p coqPackages.coqide -c coqide</code>

	== ProofGeneral ==		== ProofGeneral ==

imported>Vbgl: Non-default versions of libraries

2024-02-16T09:45:57Z

Non-default versions of libraries

← Older revision		Revision as of 09:45, 16 February 2024
Line 38:		Line 38:

	This will open a shell in which both Coq and the [https://math-comp.github.io/math-comp/ Mathematical Components library] are available. Notice that even if Coq is globally installed, it is required to list it as an input of the shell.		This will open a shell in which both Coq and the [https://math-comp.github.io/math-comp/ Mathematical Components library] are available. Notice that even if Coq is globally installed, it is required to list it as an input of the shell.

			=== Using non-default versions of packaged libraries ===

			For some libraries, several versions are available in nixpkgs. However, there is a default one and accessing non-default versions is non trivial. For instance, at the time of writing (February 2024, nixos 23.11) <code>coqPackages.mathcomp</code> refers to the mathcomp library at version 1.18.0 (for Coq 8.18). An other version of this library may be accessed by overriding its <code>version</code> argument, as follows: <code>coqPackages.mathcomp.override { version = "2.1.0"; }</code>.

			In more complex situations, it may be necessary to override several packages, or to use an overridden package as input to an other one. In order to get a consistent set of Coq libraries, one can use the <code>overrideScope'</code> function; for instance <code>coqPackages.overrideScope' (self: super: { mathcomp = super.mathcomp.override { version = "2.1.0"; }; })</code> is a set of Coq packages in which mathcomp is at version 2.1.0 (i.e., any package in this set that uses mathcomp will use that version).

	=== Global installation of libraries ===		=== Global installation of libraries ===

imported>Vbgl: Typo

2022-06-27T14:03:09Z

Typo

← Older revision		Revision as of 14:03, 27 June 2022
Line 45:		Line 45:
	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

	=== See also… ===		== See also… ==

	Related blog post: https://yannherklotz.com/nix-for-coq/		Related blog post: https://yannherklotz.com/nix-for-coq/

	[[Category:Applications]]		[[Category:Applications]]

imported>Vbgl at 14:02, 27 June 2022

2022-06-27T14:02:41Z

← Older revision		Revision as of 14:02, 27 June 2022
Line 44:		Line 44:

	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

			=== See also… ===

			Related blog post: https://yannherklotz.com/nix-for-coq/

	[[Category:Applications]]		[[Category:Applications]]

imported>Nix: add Software/Applications subcategory

2021-09-20T05:44:01Z

add Software/Applications subcategory

← Older revision		Revision as of 05:44, 20 September 2021
Line 44:		Line 44:

	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

			[[Category:Applications]]