added option timeout_scale;
authorwenzelm
Sun Nov 08 14:41:07 2015 +0100 (2015-11-08)
changeset 61602a2f0f659a3c2
parent 61601 15952a05133c
child 61603 2abbe7d700e9
added option timeout_scale;
NEWS
etc/options
src/Doc/System/Sessions.thy
src/Pure/General/time.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Sat Nov 07 20:04:09 2015 +0100
     1.2 +++ b/NEWS	Sun Nov 08 14:41:07 2015 +0100
     1.3 @@ -543,10 +543,14 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* Global session timeout is multiplied by timeout_scale factor. This
     1.8 +allows to adjust large-scale tests (e.g. AFP) to overall hardware
     1.9 +performance.
    1.10 +
    1.11  * Property values in etc/symbols may contain spaces, if written with the
    1.12  replacement character "␣" (Unicode point 0x2324).  For example:
    1.13  
    1.14 -  \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
    1.15 +    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
    1.16  
    1.17  * Command-line tool "isabelle update_then" expands old Isar command
    1.18  conflations:
     2.1 --- a/etc/options	Sat Nov 07 20:04:09 2015 +0100
     2.2 +++ b/etc/options	Sun Nov 08 14:41:07 2015 +0100
     2.3 @@ -92,6 +92,9 @@
     2.4  option timeout : real = 0
     2.5    -- "timeout for session build job (seconds > 0)"
     2.6  
     2.7 +option timeout_scale : real = 1.0
     2.8 +  -- "scale factor for session timeout"
     2.9 +
    2.10  option process_output_limit : int = 100
    2.11    -- "build process output limit in million characters (0 = unlimited)"
    2.12  
     3.1 --- a/src/Doc/System/Sessions.thy	Sat Nov 07 20:04:09 2015 +0100
     3.2 +++ b/src/Doc/System/Sessions.thy	Sun Nov 08 14:41:07 2015 +0100
     3.3 @@ -202,11 +202,16 @@
     3.4      extraordinary theories, which are meant to be enabled explicitly via some
     3.5      shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> before invoking @{tool build}.
     3.6  
     3.7 -    \<^item> @{system_option_def "timeout"} specifies a real wall-clock timeout (in
     3.8 -    seconds) for the session as a whole. The timer is controlled outside the
     3.9 -    ML process by the JVM that runs Isabelle/Scala. Thus it is relatively
    3.10 -    reliable in canceling processes that get out of control, even if there is
    3.11 -    a deadlock without CPU time usage.
    3.12 +    \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
    3.13 +    specify a real wall-clock timeout for the session as a whole: the two
    3.14 +    values are multiplied and taken as the number of seconds. Typically,
    3.15 +    @{system_option "timeout"} is given for individual sessions, and
    3.16 +    @{system_option "timeout_scale"} as global adjustment to overall hardware
    3.17 +    performance.
    3.18 +
    3.19 +    The timer is controlled outside the ML process by the JVM that runs
    3.20 +    Isabelle/Scala. Thus it is relatively reliable in canceling processes that
    3.21 +    get out of control, even if there is a deadlock without CPU time usage.
    3.22  
    3.23    The @{tool_def options} tool prints Isabelle system options. Its
    3.24    command-line usage is:
    3.25 @@ -315,11 +320,11 @@
    3.26    The build process depends on additional options
    3.27    (\secref{sec:system-options}) that are passed to the prover eventually. The
    3.28    settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
    3.29 -  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
    3.30 -  threads=4"\<close>. Moreover, the environment of system build options may be
    3.31 -  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>,
    3.32 -  which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple
    3.33 -  occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given order.
    3.34 +  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
    3.35 +  Moreover, the environment of system build options may be augmented on the
    3.36 +  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
    3.37 +  \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
    3.38 +  the command-line are applied in the given order.
    3.39  
    3.40    \<^medskip>
    3.41    Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
     4.1 --- a/src/Pure/General/time.scala	Sat Nov 07 20:04:09 2015 +0100
     4.2 +++ b/src/Pure/General/time.scala	Sun Nov 08 14:41:07 2015 +0100
     4.3 @@ -31,6 +31,7 @@
     4.4    def + (t: Time): Time = new Time(ms + t.ms)
     4.5    def - (t: Time): Time = new Time(ms - t.ms)
     4.6  
     4.7 +  def compare(t: Time): Int = ms compare t.ms
     4.8    def < (t: Time): Boolean = ms < t.ms
     4.9    def <= (t: Time): Boolean = ms <= t.ms
    4.10    def > (t: Time): Boolean = ms > t.ms
     5.1 --- a/src/Pure/Tools/build.scala	Sat Nov 07 20:04:09 2015 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Sun Nov 08 14:41:07 2015 +0100
     5.3 @@ -50,6 +50,9 @@
     5.4      files: List[Path],
     5.5      document_files: List[(Path, Path)],
     5.6      entry_digest: SHA1.Digest)
     5.7 +  {
     5.8 +    def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
     5.9 +  }
    5.10  
    5.11    def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    5.12  
    5.13 @@ -342,7 +345,6 @@
    5.14          Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
    5.15  
    5.16        def outdegree(name: String): Int = graph.imm_succs(name).size
    5.17 -      def timeout(name: String): Double = tree(name).options.real("timeout")
    5.18  
    5.19        object Ordering extends scala.math.Ordering[String]
    5.20        {
    5.21 @@ -359,7 +361,7 @@
    5.22              case 0 =>
    5.23                compare_timing(name2, name1) match {
    5.24                  case 0 =>
    5.25 -                  timeout(name2) compare timeout(name1) match {
    5.26 +                  tree(name2).timeout compare tree(name1).timeout match {
    5.27                      case 0 => name1 compare name2
    5.28                      case ord => ord
    5.29                    }
    5.30 @@ -620,7 +622,7 @@
    5.31      @volatile private var was_timeout = false
    5.32      private val timeout_request: Option[Event_Timer.Request] =
    5.33      {
    5.34 -      val timeout = info.options.seconds("timeout")
    5.35 +      val timeout = info.timeout
    5.36        if (timeout > Time.zero)
    5.37          Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true })
    5.38        else None