The Coq mailing list

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

Sorry for any offense given, Theo.  My only intention was to clarify 
that nested lemmas are an essential feature for production-scale use of 
Coq ATM as far as I can tell, so their implied deprecation by the Coq 
team, without a named replacement with the same strengths, is scary.  
(Earlier messages in this thread may or may not deserve to be 
interpreted in that way.  I'm devoting limited attention to watching 
coq-club, and I could easily misinterpret statements after quick 
reading.) However, I'm interested which replacements the Coq team is 
working on!  I only ask that the feature remain until the replacement(s) 
are ready.  Coq really would be unusable without some feature of this 
kind, to work on a lemma during proof of another, without forcing 
replaying of parts of the original lemma's proof script each time a new 
lemma is added.

On 1/23/19 3:38 PM, Maxime Dénès wrote:
> 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).

Absolutely.  Amping up the baseline performance would help remove the 
need to economize on rerunning proof scripts.  I'm just skeptical that 
the baseline performance can be pushed high enough any time soon that it 
stops mattering that scripts need to be rerun.  (You're probably also 
not claiming that holy grail is attainable any time soon.)

> 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.
A caching mechanism for in-progress proofs could do the same job more 
elegantly, with the right IDE support!  That is, if I can edit a lemma 
before the current proof, but somehow the state of the current proof is 
saved well enough that I can jump right back in later, then, AFAIK, that 
would satisfy everyone.  It would look nicer in the work-in-progress .v 
file, too, and save time on prettifying finished scripts.