Hey PG-devel,

Paul is starting to work on porting PG to support new features introduced in 
Coq 8.5 (in particular a new async API). You can see a demo of the new API in 
action at https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9 (note in particular 
how the last proof completes before the other ones are processed; note also 
that this isn't PG, just a prototype that I made hosted at 
https://github.com/cpitclaudel/elcoq/).

We had long on and off-list discussions on how to best do this, wondering how 
much of the existing proof-shell code could be reused and shared. The answer 
was "not much", mostly because Coq's new async protocol isn't compatible with 
the one-prompt-one-response model that PG relies on. Based on this, there were 
essentially three ways to go:

1. Abandon the current Proof General, and start a new Emacs mode entirely, 
gradually merging-in bits and pieces of Proof General (indentation code, syntax 
highlighting, etc).

2. Refactor PG to delimit new interfaces, and somehow support both the old REPL 
mode and the new async mode.

3. Refactor PG to use the new async mode, dropping the REPL and support for old 
proof assistants on the way.

I personally don't like option 1 at all.

Option 2 was considered and partly attempted, but it does turn out to be very 
costly to implement cleanly, and it adds to the complexity without bringing 
much: support for most other provers is partly broken, and the refactoring 
would not fix them.

Option 3 is relatively easy and lets us return quickly to fully supporting Coq 
in PG, thereby hopefully allowing PG to remain the editor of choice for Coq. 
Unfortunately, it also means that the next release of Proof General will not be 
backwards compatible.  We'll mitigate this by tagging a last-good version 
before removing the REPL-management code, and editing the README to clarify how 
to use that version.

For these reasons, we settled on option 3.  It would be useful to hear from 
current users of PG for proof assistants other than Coq, to see if we could 
think of a transition plan for them (in particular, if there exists a newer, 
asynchronous protocol for that proof assistant, it would be good to hear more 
about it with the hope of supporting is as well once the Coq port is 
completed).  It would also be useful to hear from users of less-commonly-used 
features of PG, so that we can make sure that they remain compatible. Proof 
Tree is one; what are the others?

Cheers,
Clément.


Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to