3
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Is coq-elpi also the sort of tactic scripting language you mean? $\endgroup$
    – Mike Shulman
    Mar 13, 2022 at 16:43
  • $\begingroup$ @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. $\endgroup$
    – Greg Nisbet
    Mar 13, 2022 at 17:27
  • $\begingroup$ @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. $\endgroup$
    – Pierre-Marie Pédrot
    Mar 14, 2022 at 11:53

1 Answer 1

Reset to default
3
$\begingroup$

I guess I'll post this as an answer:

  • Coq-elpi is a plugin for writing Coq tactics in ELPI, which is a dialect of λProlog. λProlog is a higher-order statically typed logic programming language. I haven't used coq-elpi myself, but apparently one of its advantages is a higher-order abstract syntax representation of binders.
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.