On Sat, May 7, 2016 at 3:33 PM, Clément Pit--Claudel
<clement....@gmail.com> wrote:
> I don't think we should give it a different name yet; I think it would create 
> a lot of confusion.
> We can phrase this differently: what you are currently writing is a library 
> that implements the protocol spoken by Coq. Ideally, we would be able to plug 
> that library straight into proof general. Unfortunately, that isn't the case 
> today. So, we'll have to modify PG. That's fine :)
> One particular strong point of proof general is its ability to talk to 
> multiple versions of Coq. A full fork would be problematic, because it would 
> loose this ability.

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.
Then we have simpler code at both ends. I'm told that PG become de
facto Coq-only, so if Coq commits to XML, there's little reason to
support the prompt mode in PG for the sake of other provers.

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

I see your points, of course.

> Regarding the other part (coqserver), I think a coqdev thread would be more 
> appropriate.

Yes, just musing out loud on related topics.

-- Paul
ProofGeneral-devel mailing list

Reply via email to