[isabelle-dev] NEWS

[Sascha Boehme]

How about providing a parse function "time_of_string" which turns
strings like "30s" or "15ms" into proper times, and possibly adding a
configuration option scheme for times (besides the existing bool, int
and string schemes)?  It seems that this could and should be provided
be provided by the system to have a uniform interface and prevent
further confusion.

Sascha

Tobias Nipkow wrote:
> As I said, I was entirely unconfused that it is in seconds, and am glad
> of it. HOWEVER: there is indeed a confusing difference between s/h and
> Nitpick on the one hand and q/c on the other hand:
> 
> quickcheck[timeout=30]
> sledgehammer[timeout=30s]
> 
> And also in their response to the wrong format:
> 
> quickcheck[timeout=30s]
> 
> *** Outer syntax error: end of input expected,
> *** but keyword [ was found
> 
> sledgehammer[timeout=30]
> 
> *** Parameter "timeout" must be assigned a positive time value (e.g.,
> "60 s", "200 ms") or "none".
> *** At command "sledgehammer"
> 
> Unification is appreciated ;-)
> 
> Tobias
> 
> Makarius schrieb:
> > On Fri, 29 Oct 2010, 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.
> > 
> > I have forgotten to say that Jasmin has his own (complicated) time formats.
> > 
> > This is again a question how we invest our own precious time (by keeping
> > things as simple as possible) while minimizing user confusion.
> > 
> > 
> >     Makarius
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev