On 11/06/16 21:29, Paul A. Steckler wrote: > On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel > <[email protected]> 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
