Pierre Roux (Jul 20 2022 at 08:23): 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?
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.
Pierre Roux (Jul 20 2022 at 08:30):I was thinking about the plugin of validsdp (but smtcoq is probably in a similar situation)
Enrico Tassi (Jul 20 2022 at 08:31):You mean, you want to call OCaml code directly?
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?
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)
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.
Enrico Tassi (Jul 20 2022 at 09:43):I imagine I already have conversions for all the data types you need.
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)
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
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
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: Oct 13 2024 at 01:02 UTC