The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 1/23/19 6:00 AM, Pierre Courtieu wrote:
> It looks to me that this feature could be implemented cleanly if some
> development power were dedicated to it. But there are a lot of cool
> features to wish for and not an infinite manpower in the coq dev team.
> It is very good news that some effort are currently dedicated to UI in
> general.

Thanks for the very thorough summary, Pierre!  And thanks, Maxime, for a 
different kind of summary of the Coq team's perspective.

Surely there are many candidates for features to prioritize in 
implementation.  I just want to repeat myself a bit and emphasize that 
the issue of nested lemmas should not be thought of as a feature 
request.  It is a feature that has been in place for a long time and 
indeed forms a central element of how Coq is used. It is 
disproportionately relied on in large-scale developments that have many 
(in at least one case, literally hundreds of millions) real-world users 
depending on them.  It seems like a governance failure if maintaining 
crucial features is weighed equally to adding cool new stuff.