The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi all,

Théo, I think we should be careful when measuring past investment in
Coq. Of course, the French taxpayer has probably brought a lot more than
others in terms of direct funding (essentially, research and development
time). But there are also many indirect ways that Coq has benefited from
other sources (infrastructure, scientific ideas, reports and suggestions
by users, teaching, advertisement, recognition, etc).

Finally, I think we should take no offense from Adam's comment about the
past century. I believe he was specifically saying that back in the
days, large scale verification in an industrial context was less common
than nowadays.

Michael, I don't recall exactly what I mentioned during the Coq
implementors workshop. But surely I must have had in mind that nested
lemmas make the document structure more complicated, and that their
scoping rule is not ideal, since they survive the proof that contain
them (so the syntactic nesting is not reflected by a semantic scoping).

Adam, I understand your remark, but let's not forget that the "cool new
stuff" we have in mind is often closely related to performance (which I
know is dear to your heart). For example, optimizations, delegation
heuristics, caching and invalidation are easier to implement in a
language where the structure of the document, the dependencies between
objects and their scoping are simple. Nested lemmas are making such
analyses more difficult. Which does not mean we should remove them, but
we have to deal with complex trade-offs.

Pierre, maybe I misunderstood, but there are many cases where moving the
nested lemma before the enclosing proof will change the semantics. From
a trivial name shadowing to global universe constraints that can change
the behavior of tactics.

I hope this whole thread has reassured some of our users in that we
don't plan to remove widely used features that have no replacements, or
willingly neglect some common use cases.

Maxime.

On 1/23/19 6:47 PM, Théo Zimmermann wrote:
> 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
> <mailto: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.
>