Rocq: Difference between revisions
Link to nixpkgs manual, add cleanup notice |
m subtitle typo |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [ | [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 ( | 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> | ||
In the same way of ''rocqPackages'', a ''coqPackages'' packages set is available to go with the ''coq'' compatibility package. | |||
== 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): | |||
<code>nix-shell -p | <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 '' | 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 | <code>nix-shell --packages rocqPackages.rocq-core rocqPackages.stdlib rocqPackages.mathcomp</code> | ||
This will open a shell in which both | 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 ( | 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 | 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 | 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 | <code>export ROCQPATH=$HOME/.nix-profile/lib/coq/9.1/user-contrib</code> | ||
== See also == | == See also == | ||