Question: how to properly call some OCaml code from Ltac2?

[erikmd]

Hi @ppedrot,

In the validsdp library developed by @proux01 and I, we have:

• an OCaml tactic (soswitness) that calls external solvers and retrieves a witness,
• and a Ltac frontend that calls soswitness and behaves as a reflexive tactic.

We'd like to fully migrate to Ltac2.
As it didn't seem possible to call soswitness as is from Ltac2, we currently have a Ltac1 wrapper like this:

Ltac2 soswitness_wrapper input params :=
  Control.plus (fun () =>
    set_state_ltac2 input;
    set_state_ltac2 params;
    ltac1:(pop_state_ltac1 ltac:(fun params =>
      pop_state_ltac1 ltac:(fun input => let w := fresh "w" in
      soswitness of input as w with params;
      revert w)));
    pop_state_ltac2 ())
  (fun e => Control.throw e).

but it is somewhat unsatisfactory as the set_state…/pop_state… bookkeeping (basically a variant of generalize/intros) adds some unwanted, duplicate let-ins in the final proof term…

Hence the question: would you have pointers or advice regarding the OCaml interfacing w.r.t. Ltac2?

[ppedrot]

You can register external tactics as done for all core Ltac2 tactics. This is performed in two steps. First, ML side, you register your function in a global table through a unique name. Second, Coq side, you declare the existence of such a global through an external declaration.

To have an idea of how to do that, look for instance at https://github.com/ppedrot/ltac2/blob/6d6ea351b0ea7e6e54915a0d82bc737306c0e86a/src/tac2core.ml#L686-L690
and
https://github.com/ppedrot/ltac2/blob/6d6ea351b0ea7e6e54915a0d82bc737306c0e86a/theories/Control.v#L21

[erikmd]

Hi @ppedrot, thanks a lot for your feedback! this works fine for us, so I'm closing the issue.