The Coq mailing list

[Joey Dodds <jdodds AT galois.com>]

Thank you! This is a great set of features for anyone using PG. Building in diff on type errors is probably my favorite.

Joey

On Tue, Jan 19, 2016 at 10:03 PM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

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.