Hi,
I'm new to writing Coq plugins and am wondering how I can access a Rewrite database as used for autorewrite
from within a Coq plugin. How can I access such a database from within the plugin? Perhaps also more generally, what is the best source for more in depth documentation for writing Coq plugins where I could find?
FWIW, before writing a plugin, you should probably consider whether you absolutely need it. Nowadays, its often easier to use a metalanguage such as Ltac2 or Elpi (Ltac2 is documented in the refman and Elpi comes with excelent tutorials https://github.com/LPCIC/coq-elpi/ ). Plugin development is not only harder due to the lower level API but is also much more maintenance intensive due to the instability of the OCaml API (it's not uncommon for plugins to only work with a given version of Coq).
Is it possible to call external tools (i.e., via a C-style API) from Ltac2?
@Adrian it is actually not really supported from the OCaml API either.
I've seen it before in plugins though where the plugin interfaces with C and I am trying to connect to an external solver so I need to call out of OCaml somehow
I know what you mean @Adrian , and indeed there is limited support for doing that (for example I think SMT Coq does use the right tactic engine API, it is called NonLogical
).
However, Coq API doesn't support that case well, as it cannot tell for example when a tactic execution did indeed use NonLogical and it is not "pure".
This is close to what I am trying to do. Would suggest NonLogical
as the way to go? Or is there some way to "hack" this into an Ltac2?
For the record, there was once a plugin to call external commands via Ltac (https://github.com/coq-contribs/maple-mode). It would make sense to provide something for Ltac2 (if not already done). For accessing the internal databases, I'd be curious to know the answer.
This looks similar to this https://github.com/K-dizzled/relations-via-egg. But if I understand correctly, this invokes maple specifically and doesn't allow arbitrary calls, right?
There actually used to be an external "command" args
tactic supporting arbitrary calls between 2005 and 2016 but I don't remember well the ins and outs of the experiment.
Last updated: Oct 13 2024 at 01:02 UTC