Stream: Coq devs & plugin devs

Topic: Calling Ltac2 from Ocaml


view this post on Zulip Mathis Bouverot-Dupuis (Jul 09 2024 at 18:03):

Hi all, I would like to call some Ltac2 code from Ocaml. Let's say for instance I have an Ltac2 function :

Ltac2 myfunc (x : bool) (y : int list) : unit := ...

Can I call this function from an Ocaml plugin ? And can I pass standard Ocaml values (of type bool and int list) as arguments ?

view this post on Zulip Gaëtan Gilbert (Jul 09 2024 at 18:23):

it's possible
something like

let tac = Tac2interp.interp Tac2interp.empty_environment (GTacApp (GTacRef kn, Tac2ffi.[of_bool true; of_list of_int [1; 2; 3]])) in
Proofview.Monad.map Tac2ffi.to_unit tac

has type unit Proofview.tactic
where kn is the name of your function, buit by doing something like https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/plugins/ltac2/tac2quote.ml#L43 I guess
see Tac2interp Tac2ffi etc for more info

if you're not already in tactics you can run the tactic with https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/engine/proofview.mli#L158
whether that is a good idea I'm not sure

view this post on Zulip Mathis Bouverot-Dupuis (Jul 09 2024 at 20:09):

Thanks ! I'm already in a tactic on the Ocaml side so no worries.
GTacApp expects a list of glb_tacexpr but Tac2ffi produces values of type Tac2val.valexpr, but I can't seem to find how to convert from valexpr to glb_tacexpr ?

view this post on Zulip Gaëtan Gilbert (Jul 09 2024 at 20:12):

oh right
something like

let tac = Tac2val.apply_val (Tac2interp.eval_global kn) Tac2ffi.[of_bool true; etc] in

then

view this post on Zulip Mathis Bouverot-Dupuis (Jul 10 2024 at 09:06):

I can't seem to get the kernel name of the Ltac2 constant. I'm building the same kernel name as I would for a standard Coq definition, is that correct ?
Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?

view this post on Zulip Gaëtan Gilbert (Jul 10 2024 at 10:37):

I'm building the same kernel name as I would for a standard Coq definition, is that correct ?

I don't know what exactly you mean by that so I don't know if it's correct.

view this post on Zulip Gaëtan Gilbert (Jul 10 2024 at 10:38):

Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?

There's Tac2env.globals


Last updated: Oct 13 2024 at 01:02 UTC