When I announced my plugin there, @Enrico Tassi and others warned me that developing a coq plugin in OCaml is troublesome. Since then, the plugin has changed directions and goals, and now I believe that rewriting the OCaml part in ELPI is the way forward. However, ELPI builtins do not expose enough functionality for me to do so. Furthermore, I'd like to be able to rewrite the plugin part by part, without having to do a rewrite from scratch.
To solve both of these issues, I need the entry point of my plugin to be in OCaml, and from there to run ELPI code. There is some documentation on how to run ELPI from OCaml, but what I need is to run coq-elpi from a Proofview.tactic monad, and I haven't found any documentation on how to do that.
Last updated: Oct 13 2024 at 01:02 UTC