The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Thanks Jonathan :)

On 2016-06-15 16:18, Jonathan Leivent wrote:
> 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.

Yup, that's the main reason for this port :) You can see a demo of a working 
prototype at https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9 btw (see 
https://github.com/cpitclaudel/elcoq for the code)

> 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.  And
> don't have Extraction force unextracted definitions.  But, I gather
> those are probably both async improvements for Coq, not PG...

Indeed, these are improvements to the async mode; there's plenty of 
discussion going on about this and about simplifications of the current 
protocol to make implementation easier (Emilio's SerAPI looks really 
promising).  Once PG is ported, most work for these improvements will be on 
the Coq side; they'll become available in Proof General with minimal changes.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature