The Coq mailing list

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

On Wed, Jun 15, 2016 at 04:18:14PM -0400, Jonathan Leivent wrote:
> 
> On 06/15/2016 03:59 PM, Paul A. Steckler wrote:
> >I'm in the process of reworking Proof General to support async
> >processing in coqtop.
> >
> >As part of that exercise, I'll be doing quite a bit of code
> >reorganization. In particular, I'll be discarding support for the Coq
> >REPL (as well as other REPLs). This may be a good time to consider
> >adding other features, or at least accommodating their future
> >implementation.
> >
> >One such feature might be the ability to run multiple coqtop's.
> >
> >Anything else that others can suggest?
> >
> >-- Paul
> 
> I requested some time ago a mode like CoqIDE's "-async-proofs lazy" mode,
> which is useful for editing the end of an existing script without having to
> waste compute resources on the beginning of the script.

This is already in there, but not exposed to CoqIDE.  For example
Coqoon tells Coq which part of the document the user is looking at
(perspective) and Coq computes only what's on the screen.  Proof tasks
live in a priority queue, the UI has the option to set the order relation.

> Also, it would be awesome if the async processing could really be delayed
> until absolutely necessary.  For instance, don't bother forcing a Defined
> definition until it is unfolded or reduced. 

I think there are two "kind" of definitions in Coq.
Definitions like "I define plus on nat" and definitions like in HoTT,
ie "proofs I will later reason about".  For the first kind of definition,
I think your request makes little sense, since one proves stuff on plus
immediately after it is defined.  For the latter use case, I
think the way to go is provide a Command to make these proofs
transparent later on.  I mean, you use Qed and when you really need to
open the proof you make it explicit in the document.  This makes things
quite simpler, since synchronization points become statically
detectable.

Would that work for your?  Is your use case different?

> And don't have Extraction force
> unextracted definitions.  

I don't understand that.  Could you elaborate?

> But, I gather those are probably both async
> improvements for Coq, not PG...

Yes, I fully agree with you and Clement on this point.

Best,
-- 
Enrico Tassi