coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit--Claudel <clement.pit AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Announcing Company-Coq 1.0
- Date: Wed, 20 Jan 2016 00:15:47 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
- Ironport-phdr: 9a23:ybBuNhxn2jZIxwnXCy+O+j09IxM/srCxBDY+r6Qd0eIWIJqq85mqBkHD//Il1AaPBtWFrasc06GH6OjJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6MyZ3vj6vjoNX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjdSTExVDK+2J9qVFqtoyMOKjI09CmDgch9ia9dvFS5pgBXzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmxOs5WV7IM
Hi Coq-Club,
It's a great pleasure to announce the first release of company-coq
(https://github.com/cpitclaudel/company-coq/), a collection of extensions for
Proof General [1].
Company-Coq builds on top of Proof General to make proof-writing more
efficient and more enjoyable. At its core are a collection of autocompletion
engines, offering suggestions and documentation as you type tactics,
commands, module names, and Ltac constructs. Company-Coq comes with a
collection of snippets, an enhanced display of mathematics, documentation for
Coq errors, code folding, automatic extraction of lemmas, inline
documentation popups (quick peek), enhanced support for CoqDoc comments,
notifications for long-running proofs, and source browsing features.
Installing company-coq is very easy: I encourage you to try it out (setup
instructions are on the GitHub page), to suggest features and report issues,
and to enjoy the improved experience. And if you are coming to CoqPL this
year, please attend our presentation [2] and join us for discussion on the
future of Coq development environments!
[1] Aspinall, D. (2000). Proof General: A generic tool for proof development.
In Tools and Algorithms for the Construction and Analysis of Systems (pp.
38-43). Springer Berlin Heidelberg.
[2] Pit-Claudel, C. & Courtieu, P. (2016). Company-Coq: Taking Proof General
one step closer to a real IDE. In CoqPL'16: The Second International Workshop
on Coq for PL.
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Announcing Company-Coq 1.0, Clément Pit--Claudel, 01/20/2016
- Re: [Coq-Club] Announcing Company-Coq 1.0, Joey Dodds, 01/21/2016
Archive powered by MHonArc 2.6.18.