Can you pass tactics to a plugin?

Developing plugins
1

Is it possible for a plugin command to get tactic scripts as input?
I would imagine this is possible since try accepts an Ltac expression.

2

Yes it is possible for an OCaml tactic, to accept an argument that would be a Ltac expression passed by the user.

See e.g. this file from coq’s codebase itself: https://github.com/coq/coq/blob/master/plugins/micromega/g_micromega.mlg

It is also possible to use variants of tactic(t) such as tactic3(t), if you are interested in specifying a given tactic precedence level, see also:

2 Likes
3

I’d generally recommend tactic3 as default, and IME most people agree once the consequences are pointed out. If foo takes a tactic instead of a tactic3, then a; foo b; c. parses as a; foo (b;c)., which is not what you usually want. I hear defaults are different with Ltac2 notations.

3 Likes
4

Very helpful answer! Do you know if this is possible for commands as well? It certainly works for OCaml tactics but I’m unsure how to get it to work for commands.

5

Nevermind! To go from tactic(t) to a unit Proofview.tactic:

  • For tactic plugins this requires Tacinterp.tactic_of_value ist t
  • For command plugins this is instead Tacinterp.interp t