[isabelle-dev] time specifications
makarius at sketis.net
Tue Nov 2 14:08:34 CET 2010
Concerning the question how to specify timeouts etc. in Isabelle, I have
spent some time investigating the situation of how
Isabelle/PGIP/ProofGeneral treat preferences, which is important here
since common configuration options often become system preferences at some
It has turned out resonably easy to support floating point numbers in
addition to integers. These changes are already published, see
Isabelle/ac4d75f86d97 and a few earlier changesets. Note that floats are
useful independently of the current issue of time.
We can now move forward to standardize time specifications as follows:
* Time is in seconds, as double precision floating point; users can
write 1 or 1.0 or 1.5 etc.
* A one-line function ML seconds: real -> Time.time deflates the
many variations of Time.fromFoo (typical bulky NJ library design).
* ISABELLE_HOME_USER acquires an extra prefix for *named* distributions,
i.e. official releases or bightly builds (not compilations from the
repository) to allow changing the meaning of former
settings in milliseconds. (This helps robustness of installations in
general, not just for timeouts.)
The scheme of seconds as float addresses the intuition of at least 3
others on this thread, as well as Jasmin's requirement to re-scale
It only makes sense to make this move, if we arrive at a single standard
in the end, instead of four of them.
More information about the isabelle-dev