[isabelle-dev] NEWS

[Tobias Nipkow]

Or timeout is universally in seconds, as an integer w/o unit.
Simpler or more flexible. I have no strong view.

Tobias

Sascha Boehme schrieb:
> 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