[isabelle-dev] Option type for auto tools timeout
makarius at sketis.net
Wed Dec 15 21:21:49 CET 2010
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
But this would also mean to abandon PG 184.108.40.206 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.
More information about the isabelle-dev