The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Wednesday 06 January 2010 16:14:23 Christian Doczkal wrote:
> (* Sorry for my previous incomplete message! *)
> 
> Hello Everyone
> 
> >From what I read so far, there seem to be a number of different ways to
> 
> extend Coq with additional tactics.
> 
>      1. Code it directly in Ltac
>      2. Use reflection and code it directly in Gallina
>      3. Code an external tactic and call it using "external" using XML
>         for communication
>      4. Coding the tactic directly into Coq at the OCaml level
> 
> 1 and 2 are covered to some extent in the Coq Reference Manual and in
> Adam Chlipala's cpdt notes. Is there any documentation available how to
> get started with coding tactics using variant 3 and/or 4? (Besides
> browsing the Coq source files)
> 
> Does someone have short nicely documented .ml file of a simple tactic
> for demonstration purposes?

I started writing OCaml tactics a while ago and could not find any 
documentation besides reading the source code. The best approach I found was 
to find a currently implemented Coq tactic that does something similar to 
what 
you want your tactic to do, search the source code to find the code that 
implements that tactic and then use your knowledge of how that tactic works 
to 
figure out what the functions used in the code do. I'd be delighted to know 
if 
there was an easier way than this. 

If you want to write your own plugin, have a look at the "plugins/quote" 
folder. The code for plugin is quite short so should give you an idea for how 
to get started.

Good luck,

Sean