Coq: Difference between revisions

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.

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