[isabelle-dev] NEWS

[Sascha Boehme]

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