Essentially it's defunct.  Isabelle 2014 uses some of the messages e.g.,
for configuring options on start up.  But if we're dropping support for
older Isabelle versions then it can be removed.

I would be sad to see support for other provers being taken away though.
 We put a lot of effort into making it easy to configure Proof General
to use with CLI tools (even bash).  Maybe the script management code
could be refactored into a standalone mode.  I still see people in
conferences cutting and pasting text into command lines!

 - D.

On 26/07/2016 21:55, Paul A. Steckler wrote:
> What is the status of the PGIP code in Proof General?
> Are there any provers that use the protocol?
> -- Paul
> _______________________________________________
> ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

ProofGeneral-devel mailing list

Reply via email to