The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

On Thu, Dec 10, 2015 at 4:26 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 12/10/2015 06:54 PM, Epiphanie wrote:

...
Finally, I have questions about LTac. This language seems powerful enough
to perform interesting automation, however as a post on Galinium showed,
there seems to be some heavy restriction on it.
For instance, I cannot find a way to use the Search mechanic (vernacular
command) inside a tactic, or even to know the number of subgoal there is.

See: https://coq.inria.fr/bugs/show_bug.cgi?id=3945

I little while ago I wrote a small plugin that allows you to iterate over the theorems in a hint database. The code is available here:

https://github.com/gmalecha/coq-with-hint-db

It has versions that work in both 8.4pl6 and 8.5 (beta3). It is not an optimal implementation by any stretch of the imagination, but it may be sufficient for some purposes.

I skimmed through the code of SSReflect and they do it through caml plugin,
just like the said post suggested.
However, I found nothing in the documentation about how to write your own
Coq extension just like SSReflect does, and its consacred section on the
FAQ is left blank.

This is a source of continuous frustration and debate.

Ltac is actually quite a bit more powerful than one might expect - than even its developers anticipated.  For example, it is possible to write an Ltac tactic that can know the number of subgoals.  It is even possible to write an Ltac tactic that can label the subgoals with their relative numbers.

Still, for many purposes, there seems to be little alternative but to write an OCaml plugin.  This appears to be because Ltac's ability to automate procedures is treated as very secondary to its direct interactive usage.  Even though the ability to easily automate complex procedures would of course improve that direct interactive usage.

A few other plugins that I have written might help

- template-coq (https://github.com/gmalecha/template-coq) constructs a syntactic representation of Coq terms within Coq.

- coq-plugin-utils (https://github.com/gmalecha/coq-plugin-utils) has a few functions that I have found useful when writing Coq plugins, particularly ones that extend Ltac.

Thomas Braibant also wrote a timing plugin that is documented. I'm not certain if it is still compatible with 8.5

https://github.com/braibant/Timing-plugin

-- Jonathan

--

gregory malecha