On Wed, 15 Dec 2010, David Aspinall wrote:
PGIP is supposed to be a typed protocol. There perhaps aren't many
users of those other tools which check messages strictly, but it would
be better to upgrade the protocol rather than break it crudely.
In the classic time of Proof General I always spent a lot of creativity on
extending the functionality of the prover without breaking the protocol.
This has become increasingly difficult, and the protocol has legacy status
for many years already, so I stopped such extra efforts at some point.
PS it seems like a fine time to do this, a patch in Proof General would
be easy and a 4.1 release will be made soon to support latest Coq.
The dealine for the next Isabelle release is shortly after the start of
the year 2011. If PG 4.1 is available by then, and works on Linux, Mac
OS, Cygwin with the usual Emacsen, I see no problem emit "pgreal" for
real-valued preferences.
But this would also mean to abandon PG 3.7.1.1 and PG 4.0, so the 4.1
version needs to be beyond any doubt.
I am myself hooked on the PG CVS for several weeks already. It looks
fine, but I am not using it a lot. I did not hear anything from
elsewhere, which means it works perfectly well, or nobody has tried it.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
