Unless I have a lapse of memory, the timeout specifications for s/h and Nitpick are also in seconds, possibly with an "s" appended. As a user I am glad about that, because I do not think in ms and would not like to write 30000 instead of 30.
Tobias Makarius schrieb: > 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 _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
