Company-Coq: Taking Proof General one step closer to a real IDE

• Main Authors: Pit-Claudel, Clément (Author), Courtieu, Pierre (Author)
• Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor), Pit-Claudel, Clement F. (Contributor)
• Format: Article
• Language: English
• Published: 2021-09-23T17:56:26Z.
• Subjects: Article
• Online Access: Get fulltext

Company-Coq is a new Emacs package that extends Proof General with a contextual auto-completion engine for Coq proofs and many additional facilities to make writing proofs easier and more efficient. Beyond fuzzy auto-completion of tactics, options, module names, and local definitions, company-coq offers offline in-editor documentation, convenient snippets, and multiple other Coq-specific IDE features. The system will be presented at CoqPL 2016, focusing on a live demo with an emphasis on writing proofs in Emacs more efficiently, and a discussion of desirable features of proof-oriented development environments. https://github.com/cpitclaudel/company-coq