Coq: Difference between revisions

(6 intermediate revisions by 2 users 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 ==

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

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

Line 18:

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

Line 56:

<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: @@
 == 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 ==
+[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>
+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 ==
@@ Line 18: / 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 24: / Line 56: @@
 <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]]