[isabelle-dev] Option type for auto tools timeout

[David Aspinall]

> 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.

There is a patch now committed in PG CVS for a type "pgipfloat".
Officially syntax should match spec here:
http://www.w3.org/TR/xmlschema-2/#float
Emacs is not going to check but other stricter tools might.

> 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.

For 4.0, there are over 300 direct downloads since 10th Oct, about a
dozen registrations, but I don't know how many correspond to real users
or real Isabelle users.  (How many downloads does Isabelle get per month
out of interest?)

Feedback from bona fide committed Isabelle hackers welcome!
http://proofgeneral.inf.ed.ac.uk/trac/

 - D. 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.