SMT's timeout option is also measured in seconds, and this is the case since its beginning. I found this a natural decision, and no one has ever objected to it.
Sascha Tobias Nipkow wrote: > 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 _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev