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.
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneralfirstname.lastname@example.org http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel