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
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:
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.