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@mailbroy.informatik.tu-muenchen.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev