--- 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:
- \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono
+ \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono
* Command-line tool "isabelle update_then" expands old Isar command
conflations:
--- 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)"
--- 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>\<open>env ISABELLE_FULL_TEST=true\<close> 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>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
- threads=4"\<close>. Moreover, the environment of system build options may be
- augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>,
- which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple
- occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given order.
+ additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
+ Moreover, the environment of system build options may be augmented on the
+ command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
+ \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
+ the command-line are applied in the given order.
\<^medskip>
Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
--- 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
--- 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