Rocq: Difference between revisions

(3 intermediate revisions by 2 users not shown)

Line 1:

[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [nixpkgs manual](https://nixos.org/manual/nixpkgs/unstable/#sec-language-rocq) for more information about using Rocq with Nix.

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

Rocq 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-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 --~~packages coq --run~~ coqide</code>

<code>nix-shell -p coqPackages.coqide -c coqide</code>

== ProofGeneral ==

Line 51:

Line 61:

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

[[Category:Applications]]

@@ Line 1: / Line 1: @@
+[https://rocq-prover.org/ Rocq] (formerly known as Coq) is an interactive theorem prover. Consult the [nixpkgs manual](https://nixos.org/manual/nixpkgs/unstable/#sec-language-rocq) for more information about using Rocq with Nix.
+{{Cleanup|reason=Probably don't want to recommend nix-env -iA}}
 == 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:
+Rocq 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-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 --packages coq --run coqide</code>
+<code>nix-shell -p coqPackages.coqide -c coqide</code>
 == ProofGeneral ==
@@ Line 51: / Line 61: @@
 <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/
 [[Category:Applications]]