Coq: Difference between revisions

(One intermediate revision by one other user not shown)

Line 1:

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

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

Line 38:

Line 44:

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 1: / Line 1: @@
 == 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>
-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 ==
@@ Line 38: / Line 44: @@
 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 ===