On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel
> 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
Yes, there is some code there that depends on the REPL model. See, for
example, coq-last-prompt-info in coq/coq.el.
> 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.
A lot of the code in there uses regexps to work out what the prover
has sent, which is not so clean, IMHO. Just a thought, it might be
better if that information was explicit in the XML, by using
particular tags or attributes to flag items of interest. We could
abstract over these approaches, and use regexp-matching for the REPL
approach, and XML parsing in the other approach. That would give a
clean, representation independent interface. The current XML
essentially just wraps the textual output, and so we'd still use
regexp-matching for now.
I think the approach you've outline is do-able, but again, I do have
concerns about the complexity that it brings.
There may still be a generic directory, for PG-wide features that are
independent of the REPL approach.
ProofGeneral-devel mailing list