The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Wed, Feb 12, 2014 at 12:06 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> On 02/11/2014 08:43 PM, Kristopher Micinski wrote:
>>
>> Out of curiosity, I may be missing the current one, but is there any
>> resource that systematically attempts to collect the more advanced
>> features of Coq?  As an example, while working through SF and CPDT
>> will teach you a lot, when you hop into real developments you need to
>> learn a laundry list of other things, such as libraries (Penn's
>> metatheory library, SSReflect, etc...), lesser documented features
>> (type classes and coercions), and new theory (e.g., working with the
>> homotopy type theory branch).
>>
>
>
> I think it would be misleading to say that the elements you mention are
> essential for "real developments."  I've only ever used one of them, and I
> actively recommend against using at least one of them, though I'll be
> tactful and not reveal which. :)
>
> The one I've used is coercions, which I think is simple enough that the Coq
> reference manual makes for a good tutorial.
>
> CPDT really is meant to cover all the material for "real developments" in
> Coq that is not easy to pick up from the Coq manual.  Particular application
> domains have their own knowledge bases, but I think of all that as distinct
> from Coq as a tool.

I think it's a fair point that you don't need to use any / all of
these resources to effectively work with Coq code.  But I also think
that it's true that there's not a comprehensive wiki where people can
publicize their different libraries and extensions.

I also don't disagree that CPDT / SF / the Coq manual do a good job of
covering Coq as a tool.  But I also think there's a distinction
between coq the tool, and the community around it.  As such, it might
be nice to have a place that linked these all together (even if it's
just making the Cocorico wiki updated).

Kris