# HG changeset patch # User wenzelm # Date 1446990067 -3600 # Node ID a2f0f659a3c2c7076b59e5a72b215821d3d7e2f4 # Parent 15952a05133c8b05eeadd7697333a6e70f58aeeb added option timeout_scale; diff -r 15952a05133c -r a2f0f659a3c2 NEWS --- a/NEWS Sat Nov 07 20:04:09 2015 +0100 +++ b/NEWS Sun Nov 08 14:41:07 2015 +0100 @@ -543,10 +543,14 @@ *** System *** +* Global session timeout is multiplied by timeout_scale factor. This +allows to adjust large-scale tests (e.g. AFP) to overall hardware +performance. + * Property values in etc/symbols may contain spaces, if written with the replacement character "␣" (Unicode point 0x2324). For example: - \ code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono + \ code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono * Command-line tool "isabelle update_then" expands old Isar command conflations: diff -r 15952a05133c -r a2f0f659a3c2 etc/options --- a/etc/options Sat Nov 07 20:04:09 2015 +0100 +++ b/etc/options Sun Nov 08 14:41:07 2015 +0100 @@ -92,6 +92,9 @@ option timeout : real = 0 -- "timeout for session build job (seconds > 0)" +option timeout_scale : real = 1.0 + -- "scale factor for session timeout" + option process_output_limit : int = 100 -- "build process output limit in million characters (0 = unlimited)" diff -r 15952a05133c -r a2f0f659a3c2 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Sat Nov 07 20:04:09 2015 +0100 +++ b/src/Doc/System/Sessions.thy Sun Nov 08 14:41:07 2015 +0100 @@ -202,11 +202,16 @@ extraordinary theories, which are meant to be enabled explicitly via some shell prefix \<^verbatim>\env ISABELLE_FULL_TEST=true\ before invoking @{tool build}. - \<^item> @{system_option_def "timeout"} specifies a real wall-clock timeout (in - seconds) for the session as a whole. The timer is controlled outside the - ML process by the JVM that runs Isabelle/Scala. Thus it is relatively - reliable in canceling processes that get out of control, even if there is - a deadlock without CPU time usage. + \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"} + specify a real wall-clock timeout for the session as a whole: the two + values are multiplied and taken as the number of seconds. Typically, + @{system_option "timeout"} is given for individual sessions, and + @{system_option "timeout_scale"} as global adjustment to overall hardware + performance. + + The timer is controlled outside the ML process by the JVM that runs + Isabelle/Scala. Thus it is relatively reliable in canceling processes that + get out of control, even if there is a deadlock without CPU time usage. The @{tool_def options} tool prints Isabelle system options. Its command-line usage is: @@ -315,11 +320,11 @@ The build process depends on additional options (\secref{sec:system-options}) that are passed to the prover eventually. The settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide - additional defaults, e.g.\ \<^verbatim>\ISABELLE_BUILD_OPTIONS="document=pdf - threads=4"\. Moreover, the environment of system build options may be - augmented on the command line via \<^verbatim>\-o\~\name\\<^verbatim>\=\\value\ or \<^verbatim>\-o\~\name\, - which abbreviates \<^verbatim>\-o\~\name\\<^verbatim>\=true\ for Boolean options. Multiple - occurrences of \<^verbatim>\-o\ on the command-line are applied in the given order. + additional defaults, e.g.\ \<^verbatim>\ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\. + Moreover, the environment of system build options may be augmented on the + command line via \<^verbatim>\-o\~\name\\<^verbatim>\=\\value\ or \<^verbatim>\-o\~\name\, which abbreviates + \<^verbatim>\-o\~\name\\<^verbatim>\=true\ for Boolean options. Multiple occurrences of \<^verbatim>\-o\ on + the command-line are applied in the given order. \<^medskip> Option \<^verbatim>\-b\ ensures that heap images are produced for all selected diff -r 15952a05133c -r a2f0f659a3c2 src/Pure/General/time.scala --- a/src/Pure/General/time.scala Sat Nov 07 20:04:09 2015 +0100 +++ b/src/Pure/General/time.scala Sun Nov 08 14:41:07 2015 +0100 @@ -31,6 +31,7 @@ def + (t: Time): Time = new Time(ms + t.ms) def - (t: Time): Time = new Time(ms - t.ms) + def compare(t: Time): Int = ms compare t.ms def < (t: Time): Boolean = ms < t.ms def <= (t: Time): Boolean = ms <= t.ms def > (t: Time): Boolean = ms > t.ms diff -r 15952a05133c -r a2f0f659a3c2 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Nov 07 20:04:09 2015 +0100 +++ b/src/Pure/Tools/build.scala Sun Nov 08 14:41:07 2015 +0100 @@ -50,6 +50,9 @@ files: List[Path], document_files: List[(Path, Path)], entry_digest: SHA1.Digest) + { + def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) + } def is_pure(name: String): Boolean = name == "RAW" || name == "Pure" @@ -342,7 +345,6 @@ Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0) def outdegree(name: String): Int = graph.imm_succs(name).size - def timeout(name: String): Double = tree(name).options.real("timeout") object Ordering extends scala.math.Ordering[String] { @@ -359,7 +361,7 @@ case 0 => compare_timing(name2, name1) match { case 0 => - timeout(name2) compare timeout(name1) match { + tree(name2).timeout compare tree(name1).timeout match { case 0 => name1 compare name2 case ord => ord } @@ -620,7 +622,7 @@ @volatile private var was_timeout = false private val timeout_request: Option[Event_Timer.Request] = { - val timeout = info.options.seconds("timeout") + val timeout = info.timeout if (timeout > Time.zero) Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true }) else None