Stream: Elpi users & devs

Topic: Calling external tools with Coq-Elpi


view this post on Zulip Pierre Roux (Jul 20 2022 at 08:23):

Couldn't calling an OCaml library be another legitimate use case? (to retrieve some witness in a reflexive tactic for instance)
Is there a way in elpi to call some external tool?

view this post on Zulip Enrico Tassi (Jul 20 2022 at 08:29):

Hum, not "streamlined for Coq" in the sense that you have APIs to run an external command and read a file but that is a bit too low level IMO to be recommended.
But if someone has a use case in mind, I'm happy to think about a better API for this use case.

view this post on Zulip Pierre Roux (Jul 20 2022 at 08:30):

I was thinking about the plugin of validsdp (but smtcoq is probably in a similar situation)

view this post on Zulip Enrico Tassi (Jul 20 2022 at 08:31):

You mean, you want to call OCaml code directly?

view this post on Zulip Pierre Roux (Jul 20 2022 at 08:34):

That's what we are doing in validsdp: calling the OSDP OCaml library, that itself calls external solvers. But we could indeed make a standalone executable. We would then need a simple language at the interface (something to encode simple OCaml inductive types). Do we have something in elpi to parse back lisp expressions or something like that?

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

view this post on Zulip Karl Palmskog (Jul 22 2022 at 20:47):

I think this is very specific Elpi stuff, so moving there to make it easier to find

view this post on Zulip Notification Bot (Jul 22 2022 at 20:47):

This topic was moved here from #Miscellaneous > Calling external tools with Coq-Elpi by Karl Palmskog.


Last updated: Mar 28 2024 at 18:02 UTC