[isabelle-dev] Option type for auto tools timeout

[Makarius]

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