Coq - Revision history

imported>Tora0101: Update to current environment

2024-03-11T09:41:14Z

Update to current environment

← Older revision		Revision as of 09:41, 11 March 2024
Line 1:		Line 1:
	== Installation ==		== 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>		<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 ==		== ProofGeneral ==

imported>Vbgl: Non-default versions of libraries

2024-02-16T09:45:57Z

Non-default versions of libraries

← Older revision		Revision as of 09:45, 16 February 2024
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.		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 ===		=== Global installation of libraries ===

imported>Vbgl: Typo

2022-06-27T14:03:09Z

Typo

← Older revision		Revision as of 14:03, 27 June 2022
Line 45:		Line 45:
	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

	=== See also… ===		== See also… ==

	Related blog post: https://yannherklotz.com/nix-for-coq/		Related blog post: https://yannherklotz.com/nix-for-coq/

	[[Category:Applications]]		[[Category:Applications]]

imported>Vbgl at 14:02, 27 June 2022

2022-06-27T14:02:41Z

← Older revision		Revision as of 14:02, 27 June 2022
Line 44:		Line 44:

	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<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]]		[[Category:Applications]]

imported>Nix: add Software/Applications subcategory

2021-09-20T05:44:01Z

add Software/Applications subcategory

← Older revision		Revision as of 05:44, 20 September 2021
Line 44:		Line 44:

	<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>		<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>

			[[Category:Applications]]

imported>Vbgl: /* ProofGeneral */ evil-mode

2018-09-06T09:58:19Z

ProofGeneral: evil-mode

← Older revision		Revision as of 09:58, 6 September 2018
Line 24:		Line 24:

	<code>(when (fboundp 'electric-indent-mode) (electric-indent-mode 0))</code>		<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 ==		== Using libraries ==

imported>Vbgl: proofgeneral

2018-03-22T14:02:37Z

proofgeneral

← Older revision		Revision as of 14:02, 22 March 2018
Line 8:		Line 8:

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

	== Using libraries ==		== Using libraries ==

imported>Vbgl: A few words about Coq

2018-03-12T08:58:01Z

A few words about Coq

New page

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

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

<code>nix-shell --packages coq --run coqide</code>

== Using libraries ==

A few third-party libraries are available under the ''coqPackages'' attribute set.

A simple way to use such a library is within a temporary shell, e.g.,

<code>nix-shell --packages coq coqPackages.mathcomp</code>

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.

=== Global installation of libraries ===

It is possible to globally install a Coq library as any other Nix package. Notice however that it will not be automatically visible to Coq. Coq search for libraries in the directories that are listed in the ''COQPATH'' environment variable. When using Coq in a Nix shell (as described above), this variable is automatically populated with paths to the Coq libraries that are provided by the shell inputs. You may manually define this variable to point to your profile, e.g.,

<code>export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib</code>