webertj at in.tum.de
Fri Oct 29 18:09:27 CEST 2010
On Fri, 2010-10-29 at 17:48 +0200, Makarius 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
I find "30 s" and "500 ms" rather intuitive.
Various GNU tools that take time arguments follow a similar convention.
For instance, "man timeout" on my system shows
timeout [OPTION] NUMBER[SUFFIX] COMMAND [ARG]...
Start COMMAND, and kill it if still running after NUMBER seconds. SUF-
FIX may be ‘s’ for seconds (the default), ‘m’ for minutes, ‘h’ for
hours or ‘d’ for days.
Add a 'ms' suffix, and you have a rather flexible and reasonably
user-friendly input format.
Translating every time into milliseconds internally is fine, of course.
But only supporting milliseconds in the user interface would be awkward.
Just my 2 cents ...
More information about the isabelle-dev