# HG changeset patch # User blanchet # Date 1288819613 -3600 # Node ID 03156257040f6491bf6b159548a16a7ec9961923 # Parent d1c14898fd04e8804fea44f41b816c60c4d82869 standardize on seconds for Nitpick and Sledgehammer timeouts diff -r d1c14898fd04 -r 03156257040f NEWS --- a/NEWS Wed Nov 03 20:19:24 2010 +0100 +++ b/NEWS Wed Nov 03 22:26:53 2010 +0100 @@ -325,6 +325,14 @@ - Renamed options: sledgehammer [atps = ...] ~> sledgehammer [provers = ...] sledgehammer [atp = ...] ~> sledgehammer [prover = ...] + sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77] + (and "ms" and "min" are no longer supported) + INCOMPATIBILITY. + +* Nitpick: + - Renamed options: + nitpick [timeout = 77 s] ~> nitpick [timeout = 77] + nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777] INCOMPATIBILITY. * Changed SMT configuration options: diff -r d1c14898fd04 -r 03156257040f doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Nov 03 20:19:24 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Nov 03 22:26:53 2010 +0100 @@ -261,7 +261,7 @@ \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount] -Total time: 768 ms. +Total time: 0.76 s. \postw Nitpick found a counterexample in which $'a$ has cardinality 3. (For @@ -797,7 +797,7 @@ Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \\[2\smallskipamount] Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount] -Total time: 1439 ms. +Total time: 1.43 s. \postw No genuine counterexample is possible because Nitpick cannot rule out the @@ -850,7 +850,7 @@ & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt] & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt] & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount] -Total time: 2420 ms. +Total time: 2.42 s. \postw Nitpick's output is very instructive. First, it tells us that the predicate is @@ -1012,7 +1012,7 @@ \hbox{}\qquad\qquad $\textit{b} = a_2$ \\ \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\ \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount] -Total time: 1027 ms. +Total time: 1.02 s. \postw The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas @@ -1160,7 +1160,7 @@ 4 := \textit{Var}~0,\> 5 := \textit{Var}~0)\end{aligned}$ \\ \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount] -Total time: $3560$ ms. +Total time: 3.56 s. \postw Using \textit{eval}, we find out that $\textit{subst}~\sigma~t = @@ -1255,7 +1255,7 @@ \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\ \hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount] -Total time: 1636 ms. +Total time: 1.63 s. \postw In theory, it should be sufficient to test a single scope: @@ -1849,7 +1849,7 @@ using \textbf{nitpick\_\allowbreak params}. For example: \prew -\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$] +\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60] \postw The options are categorized as follows:\ mode of operation @@ -1887,10 +1887,10 @@ \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\}. - \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8). -\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms} -(milliseconds), or the keyword \textit{none} ($\infty$ years). +\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number +(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} +($\infty$ seconds). \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant. \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$''). \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g., @@ -2510,8 +2510,8 @@ \label{timeouts} \begin{enum} -\opdefault{timeout}{time}{$\mathbf{30}$ s} -Specifies the maximum amount of time that the \textbf{nitpick} command should +\opdefault{timeout}{time}{$\mathbf{30}$} +Specifies the maximum number of seconds that the \textbf{nitpick} command should spend looking for a counterexample. Nitpick tries to honor this constraint as well as it can but offers no guarantees. For automatic runs, \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share @@ -2521,8 +2521,8 @@ \nopagebreak {\small See also \textit{max\_threads} (\S\ref{optimizations}).} -\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms} -Specifies the maximum amount of time that the \textit{auto} tactic should use +\opdefault{tac\_timeout}{time}{$\mathbf{0.5}$} +Specifies the maximum number of seconds that the \textit{auto} tactic should use when checking a counterexample, and similarly that \textit{lexicographic\_order} and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive predicate is well-founded. Nitpick tries to honor this constraint as well as it @@ -2863,7 +2863,7 @@ which can become invalid if you change the definition of an inductive predicate that is registered in the cache. To clear the cache, run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g., -501$\,\textit{ms}$). +$0.51$). \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a \textbf{guess} command in a structured proof. diff -r d1c14898fd04 -r 03156257040f doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 03 20:19:24 2010 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 03 22:26:53 2010 +0100 @@ -378,9 +378,9 @@ \textit{smart}. \item[$\bullet$] \qtybf{int\/}: An integer. \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. -\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), -$s$ (seconds), or \textit{ms} -(milliseconds), or the keyword \textit{none} ($\infty$ years). +\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number +(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} +($\infty$ seconds). \end{enum} Default values are indicated in square brackets. Boolean options have a negated @@ -457,8 +457,8 @@ \opnodefault{atp}{string} Legacy alias for \textit{provers}. -\opdefault{timeout}{time}{$\mathbf{30}$ s} -Specifies the maximum amount of time that the automatic provers should spend +\opdefault{timeout}{time}{$\mathbf{30}$} +Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. For historical reasons, the default value of this option can be overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof General. diff -r d1c14898fd04 -r 03156257040f src/HOL/Mutabelle/MutabelleExtra.thy --- a/src/HOL/Mutabelle/MutabelleExtra.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy Wed Nov 03 22:26:53 2010 +0100 @@ -27,7 +27,7 @@ quickcheck_params [size = 5, iterations = 1000] (* -nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] +nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat] *) ML {* Auto_Tools.time_limit := 10 *} diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\6, unary_ints, max_potential = 0, - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] subsection {* Curry in a Hurry *} diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\8, max_potential = 0, - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] primrec rot where "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Hotel_Nits.thy --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -13,7 +13,7 @@ begin nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, - timeout = 120 s] + timeout = 120] typedecl guest typedecl key diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\8, unary_ints, sat_solver = MiniSat_JNI, - max_threads = 1, timeout = 60 s] + max_threads = 1, timeout = 60] inductive p1 :: "nat \ bool" where "p1 0" | diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\5, bits = 1,2,3,4,6, - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "Suc x = x + 1" nitpick [unary_ints, expect = none] diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -17,7 +17,7 @@ chapter {* 3. First Steps *} -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] subsection {* 3.1. Propositional Logic *} diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Pattern_Nits.thy --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI, - max_threads = 1, timeout = 60 s] + max_threads = 1, timeout = 60] lemma "x = (case u of () \ y)" nitpick [expect = genuine] diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Record_Nits.thy --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\6, max_potential = 0, - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] record point2d = xc :: int diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\6, max_potential = 0, - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "P \ Q" apply (rule conjI) diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1, - timeout = 60 s] + timeout = 60] fun f1 :: "nat \ nat \ nat \ nat \ nat \ nat" where "f1 a b c d e = a + b + c + d + e" diff -r d1c14898fd04 -r 03156257040f src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 03 22:26:53 2010 +0100 @@ -12,7 +12,7 @@ begin nitpick_params [card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, - timeout = 60 s] + timeout = 60] typedef three = "{0\nat, 1, 2}" by blast diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Nov 03 22:26:53 2010 +0100 @@ -980,9 +980,9 @@ | Exn.Interrupt => if auto orelse debug then raise Interrupt else error (excipit "was interrupted after checking") - val _ = print_v (fn () => "Total time: " ^ - signed_string_of_int (Time.toMilliseconds - (Timer.checkRealTimer timer)) ^ " ms.") + val _ = print_v (fn () => + "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ + ".") in (outcome_code, !state_ref) end handle Exn.Interrupt => if auto orelse #debug params then diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Nov 03 22:26:53 2010 +0100 @@ -61,8 +61,8 @@ ("peephole_optim", "true"), ("datatype_sym_break", "5"), ("kodkod_sym_break", "15"), - ("timeout", "30 s"), - ("tac_timeout", "500 ms"), + ("timeout", "30"), + ("tac_timeout", "0.5"), ("max_threads", "0"), ("debug", "false"), ("verbose", "false"), @@ -297,8 +297,10 @@ val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " val parse_value = Scan.repeat1 (Parse.minus >> single - || Scan.repeat1 (Scan.unless Parse.minus Parse.name) - || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat + || Scan.repeat1 (Scan.unless Parse.minus + (Parse.name || Parse.float_number)) + || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) + >> flat val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] val parse_params = Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") [] diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Nov 03 22:26:53 2010 +0100 @@ -52,6 +52,7 @@ val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val string_from_time : Time.time -> string val nat_subscript : int -> string val flip_polarity : polarity -> polarity val prop_T : typ @@ -237,6 +238,7 @@ val parse_bool_option = Sledgehammer_Util.parse_bool_option val parse_time_option = Sledgehammer_Util.parse_time_option +val string_from_time = Sledgehammer_Util.string_from_time val i_subscript = implode o map (prefix "\<^isub>") o explode fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 03 22:26:53 2010 +0100 @@ -411,11 +411,12 @@ (proof_banner auto, full_types, minimize_command, tstplike_proof, fact_names, goal, subgoal) |>> (fn message => - message ^ (if verbose then - "\nATP real CPU time: " ^ - string_of_int (the msecs) ^ " ms." - else - "") ^ + message ^ + (if verbose then + "\nATP real CPU time: " ^ + string_from_time (Time.fromMilliseconds (the msecs)) ^ "." + else + "") ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 03 22:26:53 2010 +0100 @@ -177,7 +177,7 @@ ("full_types", [if !full_types then "true" else "false"]), ("timeout", let val timeout = !timeout in [if timeout <= 0 then "none" - else string_of_int timeout ^ " s"] + else string_of_int timeout] end)] end @@ -322,7 +322,7 @@ end)) val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " -val parse_value = Scan.repeat1 Parse.xname +val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number) val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_fact_refs = diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 22:26:53 2010 +0100 @@ -124,13 +124,13 @@ | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") + string_of_int (10 + msecs div 1000) ^ "\").") | {outcome = SOME UnknownError, ...} => (* Failure sometimes mean timeout, unfortunately. *) (NONE, "Failure: No proof was found with the current time limit. You \ \can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") + string_of_int (10 + msecs div 1000) ^ "\").") | {message, ...} => (NONE, "ATP error: " ^ message)) handle ERROR msg => (NONE, "Error: " ^ msg) end diff -r d1c14898fd04 -r 03156257040f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 03 20:19:24 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 03 22:26:53 2010 +0100 @@ -11,6 +11,7 @@ val simplify_spaces : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val string_from_time : Time.time -> string val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string @@ -49,23 +50,22 @@ space_implode " " (serial_commas "or" ss) ^ ".") end +val has_junk = + exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o explode + fun parse_time_option _ "none" = NONE | parse_time_option name s = - let - val msecs = - case space_explode " " s of - [s1, "min"] => 60000 * the (Int.fromString s1) - | [s1, "s"] => 1000 * the (Int.fromString s1) - | [s1, "ms"] => the (Int.fromString s1) - | _ => 0 - in - if msecs <= 0 then - error ("Parameter " ^ quote name ^ " must be assigned a positive time \ - \value (e.g., \"60 s\", \"200 ms\") or \"none\".") + let val secs = if has_junk s then NONE else Real.fromString s in + if is_none secs orelse Real.<= (the secs, 0.0) then + error ("Parameter " ^ quote name ^ " must be assigned a positive \ + \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") else - SOME (Time.fromMilliseconds msecs) + SOME (seconds (the secs)) end +fun string_from_time t = + string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s" + val subscript = implode o map (prefix "\<^isub>") o explode fun nat_subscript n = n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript