The Coq mailing list

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

On Tue, Aug 04, 2015 at 10:46:54PM -0700, Clément Pit--Claudel wrote:
> On 08/04/2015 10:52 AM, Enrico Tassi wrote:
> > (...) Not putting the file in a flat format for performance reasons is
> > debatable: when both the enclosed and enclosing lemmas are top level and
> > complete , Coq is able to process their proofs asynchronously, so you 
> > don't
> > have to wait much (this is what happens if you refactor the script when 
> > you
> > see the warning).
> 
> I think you mean CoqIDE here, not Coq; if I understand correctly, the
> protocol that allows it to do that is still undocumented, and other
> common editors (mostly Proof General) do not have such capabilities.

The api is well documented in stm.mli
The CoqIDE protocol is xml on top of it, see --print-XML-protocol.
The protocol used by PIDE based UIs is not documented, Isabelle
oriented, and I don't recommend using it.

Everything was designed to minimize the requirements on the editor side,
and I believe PG can be as asynchronous as CoqIDE with some work. Thete
was even a sinister plan of mine to push this forward at CoqCS but nor
you nor Pierre C could attend :-(

So let me be a little pushy: Coq has such capabilities, PG is not able
to take advantage of it :-P

best,
> 
> Cheers,
> Clément.
> 



-- 
Enrico Tassi