[isabelle-dev] NEWS

[Tobias Nipkow]

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