Rocq: Difference between revisions

(6 intermediate revisions by 3 users not shown)

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.

== 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:

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>

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-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 --~~packages coq --run~~ coqide</code>

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

== ProofGeneral ==

Line 38:

Line 48:

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

Line 44:

Line 60:

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

@@ 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 ==
-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:
+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>
-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-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 --packages coq --run coqide</code>
+<code>nix-shell -p coqPackages.coqide -c coqide</code>
 == ProofGeneral ==
@@ Line 38: / Line 48: @@
 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 ===
@@ Line 44: / Line 60: @@
 <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]]