[isabelle-dev] NEWS

[Tobias Nipkow]

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