The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 02/19/2016 07:08 PM, Pierre-Marie Pédrot wrote:
> On 20/02/2016 01:00, Jonathan Leivent wrote:
>> Thanks, Robbert.  Unfortunately, I guess this means "not without a
>> plugin".  Instead, I'll just define hopefully enough numbers via
>> Notations...
> 
> Out of curiosity, what prevents you from writing / using a plugin?

Here's my take on that question:
* It requires knowledge of a second programming language beyond Ltac and 
Gallina, and of some Coq internals
* It's harder to audit for people reviewing my code, due to the point above; 
it's also harder to maintain or extend for others
* It won't work with all Coq interfaces; for example, it won't work with 
jsCoq IIUC
* It will make it harder to ensure backwards compatibility (now I need to 
care about Coq's internal interfaces). Maybe it'll break or become outdated, 
and there won't be as much documentation about ways to update it (there's not 
much about internals in CHANGES)
* I don't know how to do it, and I'm not sure where to learn (quick searches 
didn't turn up documentation, just tutorials), or whether it would be a good 
investment to learn
* Coq's notations are pretty good already

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature