On 11/06/16 21:29, Paul A. Steckler wrote:
> On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel
> <clement....@gmail.com> wrote:
>> My proposal was to dump the entire proof-shell part, indeed. I agree with 
>> you that it would make everything much easier, and I think that would be 
>> nice. We'd write a semi-working shim to not leave out 8.4 entirely, and drop 
>> the generic aspects. It would probably make your/our lives simpler, at no 
>> significant loss, I think.
> 
> I'm with you, as long as none of the other provers mind that PG will
> no longer be available to them.

I would say: go ahead and make Proof General a Coq-only system.
De-facto, it has been that already for some years.

The various README files in the prover-specific directories on
https://github.com/ProofGeneral/PG make me nostalgic. Most of that is
from the late 1990s and no longer relevant.

Isabelle has moved away from PG in 2011, and Isabelle2014 (August 2014)
is the last version that can in principle use PG. Afterwards, all
remains of the TTY loop have been dismantled: Isabelle operates directly
on multiple versions of the proof document.


        Makarius

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to