Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proving a lemma in a proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving a lemma in a proof


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proving a lemma in a proof
  • Date: Wed, 23 Jan 2019 10:04:45 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:hmaiExz9FvNduKzXCy+O+j09IxM/srCxBDY+r6Qd1OgfIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH1likHOT43/mLZhMN+g61Uog6uqRNkzo7IY4yYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YCE/cOMvxdr4LguVYOrR++BQi0BOz1zj9HnGL90Kog3Os8Cw7G2RAvEskSv3TPttr1NaMSXfqwzKnJ0TXPde1Z1irg6IXRdB0qvPKCXapofMbM10UiFBnJg1uMpYD/IT+ZzPoBv3WH4+Z4SO6jlW0qpxt/rzSz3MshjpfFipgLxlza6Cl0xps+K8eiR05he9GkFYNdtyGEOItyRcMvW2ZouDsmyr0Jvp67fS4KyJs+yx7Ed/yIaZSI7Qj5WOmNOjd3nnNleLalixa38Eig1vfwWdep31ZXtiZFk9/MuW4R1xHL98SLVPhw8l2v1DqTzQzf9PtILV4pmabHM5Ihx6Q/lpsXsUTNBC/2n0D2gbeMeUo54Oeo7vjob676qZ+HLYB0iwX+Pr4rmsy+HeQ0KBYBUHWG+eikzr3s4VX5QKlWjv0xiqTWrJfaJd0CqqGlBw9Vz50s5g2kDzam1dQYhWMIIEhEeBKBlYjpOkvBLOr2Dfel0ByQl2JgwOmDNbn8CL3MKGLCmfHvZ+VT8UlZnSM/xNUXzJJQC6kIJPu7Dkb9vdnTJhQiOg2whePmFJNw2p5ICjHHObOQLK6H6QzA3ekoOeTZPNZE6ga4EOAs4rvVtVF8nFYceaez2p5ONSKzBf1nJwOcYGaqj9scQz5T4lgOCdfygVjHagZ9Im6oVvthtDogAYOiS4LCWsagjKHThH7mTK0TXXhPDxW3KVmtd4iAXKxUOiWPPsBmkzoLEKO9QpMokxq1vQ7+jb9mMqzZ9jBK7Z8=

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.




Archive powered by MHonArc 2.6.18.

Top of Page