Coq: Difference between revisions

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