The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Aug 08, 2013 at 01:35:38AM -0400, Kristopher Micinski wrote:
> The problem with this is that sometimes my files get pretty big, and use a
> lot of automation (not by necessity, but just because I'll be toying around
> with ideas and don't want to code up more elaborate Ltac specific to the
> proofs).  Unfortunately, this leads to the problem that I may refine some
> definition at the beginning of the file (say, adding another case to a
> definition) and the whole buffer has to be reprocessed.  The same thing
> happens even if you back up and repeat steps in ProofGeneral.

Sorry about the late answer, but I did miss this message.

Currently the development version of Coq allows, in some circumstances,
to skip proofs, and jump immediately to the place the user is interested
in.  Proofs left on the side are checked in the background.

But are still checked, and always.  There is no decent dependency
analysis to understand if a proof needs to be re-checked or not.
IMO, this is a very hard task and some people in PPS, like M.Puech
and Y.Regis cited in this thread, started working on it.

The development version of Coq represents the document as a dag, where
proofs (text between Proof and Qed) are in branches parallel to the
main one.  This model allows not only to skip proofs and to process
them in background/parallel but also to fix a proof that is
broken without undoing/redoing everything (but there is no code yet for
this, still in my TODO list), since a proof branch can be modified
without altering the main branch.
But as I said, if a new toplevel command (Definition, Notation,
Lemma or even a comment) is added before a proof, that proof is
always rechecked.

So this work would definitely benefit from some sort of dependency
analysis.

Cheers
-- 
Enrico Tassi