Stream: Miscellaneous

Topic: Calling external tools with Coq-Elpi


view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:41):

So, calling OCaml from Elpi is super easy, and if your library gives you a term you can pass it back automatically.
The only problem is that, today, Coq-Elpi does not let one add external predicates, so it is not doable. But I can expose an API for that.
What I mean is that you could write some code like this one:
https://github.com/LPCIC/coq-elpi/blob/3d450f66333340e8b5d86275811147e309ec43c2/src/coq_elpi_builtins.ml#L2885-L2915
as you can see there is a GADT (a la printf really) which describes the type of the arguments in input/output, then calls ocaml code (in this case generating a constr)

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:42):

The limitation is that all external predicates have to be in that file. It could be lifted. And then you could just declare a new elpi builtin from your OSDP plugin.

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:43):

I imagine I already have conversions for all the data types you need.

view this post on Zulip Pierre Roux (Jul 20 2022 at 09:51):

Wow, that sounds great! (no hurry though, since the validsdp plugin is motly reading/writing constr, it's rather easy to maintain)

view this post on Zulip Enrico Tassi (Jul 20 2022 at 09:55):

Another option would be to give a simple FFI (as I do for ltac1) it is just I don't know (if it is possible) to find an ocaml symbol at runtime


Last updated: Jan 29 2023 at 18:03 UTC