Re: [PG-devel] Status of PGIP?

2016-07-27 Thread David Aspinall
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 mak

Re: [PG-devel] Status of PGIP?

2016-07-27 Thread Clément Pit--Claudel
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 standalo