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
environments.
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.
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
