makarius at sketis.net
Fri Oct 29 17:32:56 CEST 2010
On Fri, 29 Oct 2010, Lukas Bulwahn wrote:
> * Quickcheck now has a configurable time limit which is set to 30
> seconds by default. This can be changed by adding [timeout = n] to the
> quickcheck command. The time limit for auto quickcheck is still set
> independently, by default to 5 seconds.
I am a bit puzzled about the unit of seconds here. When time is
represented as plain integer in Isabelle, it is usually done in
milliseconds. This is motivated by simplicity and portability.
Milliseconds basically give 3 digits of fixed-point representation without
venturing on floating point numbers or SML's complicated time datatype, or
even more complicated languages for time spans (like the Babylonians
invented a long time ago to make life more interesting). Also note that
configuration options are often correlated with preferences, which need to
be manageable outside the ML process (e.g. in PG/Emacs or Isabelle/Scala).
So any extra complications of ML time formats would also affect other
The JVM normally observes our milliseconds standard as well, and jEdit
properties follow the same. This makes Isabelle/ML, Isabelle/Scala,
Isabelle/jEdit agree nicely without any further ado.
More information about the isabelle-dev