Stream: Coq devs & plugin devs

Topic: Access lemma database from plugin


view this post on Zulip Adrian (Sep 09 2024 at 12:02):

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?

view this post on Zulip Pierre Roux (Sep 09 2024 at 12:06):

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).

view this post on Zulip Adrian (Sep 09 2024 at 14:50):

Is it possible to call external tools (i.e., via a C-style API) from Ltac2?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:01):

@Adrian it is actually not really supported from the OCaml API either.

view this post on Zulip Adrian (Sep 09 2024 at 15:26):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:32):

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".

view this post on Zulip Adrian (Sep 09 2024 at 16:51):

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?

view this post on Zulip Hugo Herbelin (Sep 09 2024 at 18:49):

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.

view this post on Zulip Adrian (Sep 09 2024 at 20:46):

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?

view this post on Zulip Hugo Herbelin (Sep 10 2024 at 06:58):

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