[isabelle-dev] Option type for auto tools timeout
David.Aspinall at ed.ac.uk
Wed Dec 15 18:02:13 CET 2010
> The Proof General protocol does not understand pgreal, but happens to
> interpret a pgint value in a way that accepts floating point numbers as
> well -- the target language is Emacs LISP where everything is untyped
This is (partially) true for the PGIP implementation in Emacs, but not
true for the Java and Haskell implementations of PGIP, and not true for
the XML Schema that defines the message format.
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.
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 University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev