coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- Re: [Coq-Club] proving a lemma in a proof, (continued)
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, James McKinna, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Christian Doczkal, 01/23/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Laurent Thery, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Ralf Jung, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Beta Ziliani, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
Archive powered by MHonArc 2.6.18.