On 2016-05-07 13:44, Paul A. Steckler wrote:
> Well, we're asking Proof General to work in a fundamentally
> different way than it has so far. Adding support for the XML mode
> significantly increases the complexity of the software, and that mode
> would not be used by other provers. Imagine that we fork PG, remove
> its prompt mode stuff, and we strip out the legacy support for the
> -emacs mode in Coq.

I think this is a good plan in the long run. However, most of the complexity in 
the Coq part of proof-general is protocol-agnostic; ideally, I don't want to be 
fixing bugs in two separate copies of that code. In addition, being able to 
update people in place is a significant win for us, given the current 
installation medium (git clones).

> (...) If someone is using an old version of Coq, the old versions of
> PG are still available, of  course.

The problem here is that switching between both versions is going to be 
unpleasant at best, and that we'll make the lives of people porting 8.4 
software to 8.5 much more painful. 

I'm all for a cleanup of the PG codebase, of course. But I think we can do it 
slightly differently: starting with the current code, we can:

* Tag a last-known good version (the current HEAD) for obsolete provers
* Remove obsolete provers
* Rename the "generic/" folder to "REPL/"
* Ensure that the separation between the "coq/" subfolder and the "generic/" 
subfolder is clean; that is, check which functions in "generic/" the "coq/" 
part calls (this is our "implicit API"), and ensure that nothing on the "coq/" 
side depends on the REPL model; anything that does is probably a mistake.
* Create an "XML/" folder and implement support for the new Coq API there, 
implementing the implicit API that we identified on the previous step.
* Make sure that the "coq/" folder loads one or the other depending on the 
version of Coq that it is being used with.

It other words, my claim is that as part of a hypothetical fork we would 
already have to clean up the "coq/" subdirectory. Once this is done, it should 
be relatively easy to have support for both the REPL and the XML model in the 
same codebase. My hunch is that a very significant majority of the "coq/" 
subfolder does not depend on PG internals, since it uses clean interface 
functions to ask questions to the prover.

What do you think?

Attachment: signature.asc
Description: OpenPGP digital signature

ProofGeneral-devel mailing list

Reply via email to