Rocq: Difference between revisions
imported>Tora0101 Update to current environment |
Link to nixpkgs manual, add cleanup notice |
||
| (2 intermediate revisions 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 [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 == | == Installation == | ||
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> | <code>nix-env -iA nixpkgs.coq</code> | ||
| Line 57: | Line 61: | ||
<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 | == See also == | ||
Related blog post: https://yannherklotz.com/nix-for-coq/ | Related blog post: https://yannherklotz.com/nix-for-coq/ | ||
[[Category:Applications]] | [[Category:Applications]] | ||