The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

It seems like my reply has triggered a disproportionate reaction that I was not expecting. My intent was to communicate some info to a new user about a situation that is preexisting and that most people in this thread have already discussed over and over. It is true that the use of this feature is discouraged. It is also true that it is still needed by many users. Finally, it is true that it would have already been removed if it hadn't been the case (there is no intent to remove it at this time: I even removed the deprecation warning it emitted!). The only thing I said and that was not true is that Coq developers have no interest in fixing bugs related to nested lemmas. Some Coq developers actually do. But some other developers think that they are more useful to the user community as a whole (not just the math applications, I don't know what makes you believe this) by putting their efforts on something else.

Thanks to Maxime for the very thoughtful reply. I want to emphasize the point on funding. You may be under the impression that verification applications have driven a lot of funding to the development of Coq. So far, it isn't the case as far as I can see. It has only paid for few postdocs, plus this recent money that some of you put in the Coq consortium. This amounts to a ridiculously small figure if you compare it to what the French taxpayer has invested since the beginning (and is still investing). A significantly larger funding effort from those industrial users and abroad academic institutions would be quite appreciated. You are also very welcome to participate to the roadmap: as Maxime said, the development is open. People inside Inria have no more power on the roadmap than people outside it.

Apart from this, I also wanted to say that I found the allegation that the Coq development team was stuck in the 20th century really hurtful given all the efforts that have been made so that it's precisely not the case (e.g. opening of the development). I don't know what you were trying to achieve with this claim, except to disgust me and some others. Fortunately, most users are more grateful.

Peace,

Théo

Le mer. 23 janv. 2019 à 16:05, Adam Chlipala <adamc AT csail.mit.edu> a écrit :

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.