Rocq - Revision history

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]]

imported>Vbgl: /* ProofGeneral */ evil-mode

2018-09-06T09:58:19Z

ProofGeneral: evil-mode

← Older revision		Revision as of 09:58, 6 September 2018
Line 24:		Line 24:

	<code>(when (fboundp 'electric-indent-mode) (electric-indent-mode 0))</code>		<code>(when (fboundp 'electric-indent-mode) (electric-indent-mode 0))</code>

			There is an additional annoyance with evil-mode; see [https://github.com/syl20bnr/spacemacs/issues/8853#issuecomment-302706114 two] [https://github.com/ProofGeneral/PG/issues/174#issuecomment-293719295 discussions] describing a work-around, namely to include the following before loading evil-mode:

			<code>(setq evil-want-abbrev-expand-on-insert-exit nil)</code>

	== Using libraries ==		== Using libraries ==

imported>Vbgl: proofgeneral

2018-03-22T14:02:37Z

proofgeneral

← Older revision		Revision as of 14:02, 22 March 2018
Line 8:		Line 8:

	<code>nix-shell --packages coq --run coqide</code>		<code>nix-shell --packages coq --run coqide</code>

			== ProofGeneral ==

			[https://proofgeneral.github.io/ ProofGeneral] is a “generic [[Emacs]] interface for proof assistants”. A working [[Emacs]] is needed.

			To install ProofGeneral, you can use the corresponding attribute:

			<code>nix-env -iA nixpkgs.emacsPackages.proofgeneral_HEAD</code>

			Then, the following line should be added to Emacs configuration (aka ''.emacs''):

			<code>(require 'proof-site "~/.nix-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-site")</code>

			The ProofGeneral mode automatically sets the ''electric-indent-mode'' (recomputes the indentation of a line when leaving it), that some find extremely annoying. To disable it, the following line may be added to the ''.emacs'' file:

			<code>(when (fboundp 'electric-indent-mode) (electric-indent-mode 0))</code>

	== Using libraries ==		== Using libraries ==