Re: [PG-devel] Status of PGIP?
On 2016-07-27 05:24, David Aspinall wrote: > 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! Hi David, In the case of bash, do you have more in mind that what comint-mode already does? In general, I think it'll be possible to reinstate support for REPLs after we make the transition. We're transitioning PG to a more permissive protocol (instead of the current one-question-one prompt-one response), and it shouldn't be too hard to write a wrapper for REPLs further down the line. 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
Re: [PG-devel] Status of PGIP?
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 > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
