The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

On Fri, Dec 11, 2015 at 3:24 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 12/11/2015 03:51 PM, Gregory Malecha wrote:

...
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 will take a close look at this.  I have wanted to be able to use Hint databases for my own purposes without using auto, eauto, or typeclasses eauto - because all of them are somewhat broken with respect to proper proof search backtracking (auto is closest to working properly, but still has issues).  So, this iterator could be very useful to me.

If you run into problems, please report bugs. If the bugs can be worked out, I can add it as an opam package. 

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

Thanks.  I will look at these - but I still wish there was a better divide between Coq developers and Coq users, such that even very serious users didn't have to become developers.

I think this is a general sentiment.

I'm not a developer though I have worked a bit on the code base. IMO more code should be removed from the core Coq code base and installed as extras (probably packaged for new uses as a "batteries" package). This would probably go a long way to making it easier to work with the internals.

A while ago I examined several plugins in an attempt to write what I thought would be a trivial one: a conversion tactical between OCaml and Coq numbers (between integer and constrs of type Z, for instance).  However, nothing about any of the tactics I saw could be used to get this fundamental behavior.  I suspect, even though it is probably easy, it requires considerable knowledge of Coq internals to do properly.  And that's part of the problem with plugins - it's probably going to be the case that each reason for writing a plugin is an attempt to bridge between Ltac and some part of Coq's internals that nothing else bridges between.

For this purpose, you mainly care about the contents of kernel/term.mli (https://github.com/coq/coq/blob/trunk/kernel/term.mli) which has functions for building pieces of Coq's abstract syntax tree. These functions exist in coq-plugin-utils.

https://github.com/gmalecha/coq-plugin-utils/blob/master/src/coqstd.ml#L61 

-- Jonathan

--

gregory malecha