# List of general purpose Coq sublanguages for defining custom tactics

I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml.

It's tricky. You need to define an .mlg file (which gets lowered to an .ml file by coqpp source) ... which appears to call into the Mktop library and do some other stuff to register your .cmxs file so Coq can find it.

Also, the exact details of how you build such a thing appear to be very sensitive to the exact version of Coq and dune that you're using. (I gave up on using dune or coq_makefile -f _CoqProject and just used a horrible Makefile to build all the artifacts manually.)

I'm wondering what the alternatives are to writing a Coq extension in this way.

From what I can tell, Coq ships with at least two "tactic scripting languages" of sorts:

• Ltac -- the original one
• Ltac2 -- the successor

And two more are maintained externally:

I think a gathering a list of these sublanguages would be interesting.

I'd be especially interested in tactic-defining languages that are dynamically typed and have good support for pretty-printing ... and have simple syntaxes like Forth or Lisp.

• Is coq-elpi also the sort of tactic scripting language you mean? Mar 13 at 16:43
• @MikeShulman, yes, elpi definitely counts. Based on this example from elpi's repo, it seems like it works at a basic level by defining a new syntax inside lp:{{ ... }} with {{ ... }} as a form of anti-quotation to insert Coq terms into the elpi subprogram. Mar 13 at 17:27
• @GregoryNisbet am a bit surprised that you had trouble with coq_makefile. It is quite straightforward to write a plugin nowadays, as long as you follow the pattern from the tutorial (layout and meta files). For this kind of trouble I recommend asking people on the Coq Zulip. Mar 14 at 11:53