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