Coq: Difference between revisions
imported>Vbgl A few words about Coq |
imported>Vbgl proofgeneral |
||
| 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 == | ||