On 2016-05-07 14:37, Paul A. Steckler wrote: > On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel <clement....@gmail.com> > wrote: >> 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. > > Yes, there is some code there that depends on the REPL model. See, for > example, coq-last-prompt-info in coq/coq.el.
I see, thanks. Although for this particular example, it's mostly last-prompt-info not having an ideal name; in a sense, this is just a function that returns the current state of the proof (how many proofs are currently pending, etc). >> 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. That would be great, and I think your last point is the key. We can just strip the XML code from responses for now. > I think the approach you've outline is do-able, but again, I do have > concerns about the complexity that it brings. Anything that brings in complexity only for backwards compatibility we should avoid. However, if ensuring some level of backwards compatibility helps us reduce our technical debt, then that's good :) Ideally, we'd end up with multiple mostly-independent components: a tree-window display layer with text spans, a generic driver layer that implements basic UI functionality (moving around, etc), an implementation of the Coq API, and coq-specific package that implements syntax highlighting, indentation, and other Coq-only things. Concretely, this won't happen all at once, of course. Cheers, Clément.
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
