2022-01-23 20:38:27 +01:00
|
|
|
← [[doom-module-index:][Back to module index]] ! [[doom-module-issues:::lang coq][Issues]] ↖ [[doom-repo:tree/develop/modules/lang/coq/][Github]] ± [[doom-suggest-edit:][Suggest edits]] ? [[doom-help-modules:][Help]]
|
2021-10-16 01:28:32 +02:00
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
#+TITLE: :lang coq
|
|
|
|
|
#+SUBTITLE: Proofs as programs
|
2021-11-04 13:01:45 +01:00
|
|
|
#+CREATED: August 14, 2018
|
|
|
|
|
#+SINCE: 21.12.0 (#804)
|
2018-08-14 23:30:20 +02:00
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
* Description :unfold:
|
2018-10-06 23:45:09 +02:00
|
|
|
This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]].
|
|
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
- Code completion ([[https://github.com/cpitclaudel/company-coq][company-coq]])
|
|
|
|
|
- [[https://github.com/hlissner/doom-snippets/tree/master/coq-mode][Snippets]]
|
|
|
|
|
|
|
|
|
|
** Maintainers
|
|
|
|
|
/This module has no dedicated maintainers./ [[doom-contrib-maintainer:][Become a maintainer?]]
|
|
|
|
|
|
|
|
|
|
** Module flags
|
|
|
|
|
/This module has no flags./
|
|
|
|
|
|
|
|
|
|
** Packages
|
|
|
|
|
- [[doom-package:][proof-general]]
|
|
|
|
|
- [[doom-package:][company-coq]]
|
|
|
|
|
|
|
|
|
|
** Hacks
|
2022-01-02 19:49:22 +02:00
|
|
|
+ Replaces coq-mode abbrevs with yasnippet snippets from doom's snippet library
|
2021-10-16 01:28:32 +02:00
|
|
|
|
|
|
|
|
** TODO Changelog
|
|
|
|
|
# This section will be machine generated. Don't edit it by hand.
|
|
|
|
|
/This module does not have a changelog yet./
|
|
|
|
|
|
2022-01-02 19:49:22 +02:00
|
|
|
* Installation
|
|
|
|
|
+ [[id:01cffea4-3329-45e2-a892-95a384ab2338][Enable this module in your ~doom!~ block.]]
|
|
|
|
|
+ To use the completion features of company-coq you need to enable ~(:completion company)~
|
|
|
|
|
+ Make sure you have Coq installed and that the ~coqtop~ command is available. This comes with a standard installation of Coq.
|
|
|
|
|
You can use your linux distribution's Coq package or one of the methods given on the [[https://coq.inria.fr/download][Coq website]].
|
|
|
|
|
|
2021-10-16 01:28:32 +02:00
|
|
|
* TODO Usage
|
|
|
|
|
#+begin_quote
|
|
|
|
|
🔨 This module has no usage documentation yet. [[doom-contrib-module:][Write some?]]
|
|
|
|
|
#+end_quote
|
|
|
|
|
|
2022-01-02 19:49:22 +02:00
|
|
|
* Configuration
|
|
|
|
|
This module provides no additional configuration over that of the [[Packages]] it loads
|
2021-10-16 01:28:32 +02:00
|
|
|
|
|
|
|
|
* Troubleshooting
|
2022-01-02 19:49:22 +02:00
|
|
|
See [[https://github.com/hlissner/doom-emacs/issues?q=is%3Aissue+is%3Aopen+label%3A%22%3Alang+coq"][related github issues]]
|
2021-10-16 01:28:32 +02:00
|
|
|
/There are no known problems with this module./ [[doom-report:][Report one?]]
|
|
|
|
|
|
|
|
|
|
* Frequently asked questions
|
|
|
|
|
/This module has no FAQs yet./ [[doom-suggest-faq:][Ask one?]]
|
|
|
|
|
|
|
|
|
|
* TODO Appendix
|
|
|
|
|
#+begin_quote
|
|
|
|
|
🔨 This module has no appendix yet. [[doom-contrib-module:][Write one?]]
|
|
|
|
|
#+end_quote
|
