The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

A few useful plugins to check out to learn how to write them are:

https://github.com/braibant/coq-tutorial-ml-tactics

https://github.com/braibant/Timing-plugin (this provides a [time tac] tactic that records the amount of time spent when running [tac])

https://github.com/gmalecha/coq-plugin-utils (this has a bunch of useful utility functions that I use in a bunch of plugins that I write)

https://github.com/gmalecha/template-coq (this dumps Coq's internal representation into a simple Coq inductive type)

On Tue, Dec 2, 2014 at 8:19 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 02/12/2014 03:52, Jonathan wrote:
> What is the best way to get started writing plugins?  Is there a tutorial?

There was a blog post at Gallium.

http://gallium.inria.fr/blog/your-first-coq-plugin/

It is a bit outdated w.r.t. to trunk though. When I have time, I should
write one too, but this is not really to happen soon...

PMP

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/