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
