The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.

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

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.

-- Jonathan