The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi all,

This happened a while ago, but I forgot to send an update. During the Coq Users & Developers Workshop, I updated three of the four plugin tutorials in the Coq repository: https://github.com/coq/coq/tree/master/doc/plugin_tutorial

tuto0, tuto1, and tuto2 should now be using best practices. They went through code review from the Coq developers. I have also documented them a lot, and I have expanded them with some new functionality:

• printing warnings
• printing errors
• understanding the DSL for writing tactics and commands in OCaml
• more on interning and externing
• looking up terms you have defined, refreshing the environment appropriately
• threading state properly, e.g. in type-checking
• checking if two terms are possibly convertible under some set of constraints
  
• implementing a counter whose state persists across imports
  

I'm yet to touch tuto3, but I hope to get to it soon.

I hope this will help anyone who is considering writing a plugin. I have had a lot of my own plugin tutorials floating around in the past, and they are useful too, but none of them used best practices. I will update them as well, soon. But this is nice because it has been reviewed by the Coq developers, so it is a good place to look if you are writing a plugin and aren't sure which APIs to call, what on earth you're supposed to do with an evar_map, or how you are supposed to define a cache for your command that persists across imports.

Let me know if you have any questions, or open an issue and assign it to me if there is functionality you don't see here that you'd really like in the plugin tutorials.

Talia