timeout for session build job;
authorwenzelm
Fri Aug 03 14:52:45 2012 +0200 (2012-08-03)
changeset 486619149ebdd0241
parent 48660 730ca503e955
child 48662 b171bcd5dd86
timeout for session build job;
tuned error messages;
etc/options
src/Pure/System/build.scala
     1.1 --- a/etc/options	Fri Aug 03 13:55:51 2012 +0200
     1.2 +++ b/etc/options	Fri Aug 03 14:52:45 2012 +0200
     1.3 @@ -63,3 +63,6 @@
     1.4  declare timing : bool = false
     1.5    -- "global timing of toplevel command execution and theory processing"
     1.6  
     1.7 +declare timeout : real = 0
     1.8 +  -- "timeout for session build job (seconds > 0)"
     1.9 +
     2.1 --- a/src/Pure/System/build.scala	Fri Aug 03 13:55:51 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Fri Aug 03 14:52:45 2012 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.util.{Timer, TimerTask}
     2.8  import java.io.{BufferedInputStream, FileInputStream,
     2.9    BufferedReader, InputStreamReader, IOException}
    2.10  import java.util.zip.GZIPInputStream
    2.11 @@ -331,7 +332,7 @@
    2.12    /* jobs */
    2.13  
    2.14    private class Job(dir: Path, env: Map[String, String], script: String, args: String,
    2.15 -    val parent_heap: String, output: Path, do_output: Boolean)
    2.16 +    val parent_heap: String, output: Path, do_output: Boolean, time: Time)
    2.17    {
    2.18      private val args_file = File.tmp_file("args")
    2.19      private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    2.20 @@ -342,7 +343,29 @@
    2.21  
    2.22      def terminate: Unit = thread.interrupt
    2.23      def is_finished: Boolean = result.is_finished
    2.24 -    def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    2.25 +
    2.26 +    @volatile private var timeout = false
    2.27 +    private val timer: Option[Timer] =
    2.28 +      if (time.seconds > 0.0) {
    2.29 +        val t = new Timer("build", true)
    2.30 +        t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
    2.31 +        Some(t)
    2.32 +      }
    2.33 +      else None
    2.34 +
    2.35 +    def join: (String, String, Int) = {
    2.36 +      val (out, err, rc) = result.join
    2.37 +      args_file.delete
    2.38 +      timer.map(_.cancel())
    2.39 +
    2.40 +      val err1 =
    2.41 +        if (rc == 130)
    2.42 +          (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
    2.43 +          (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
    2.44 +        else err
    2.45 +      (out, err1, rc)
    2.46 +    }
    2.47 +
    2.48      def output_path: Option[Path] = if (do_output) Some(output) else None
    2.49    }
    2.50  
    2.51 @@ -402,7 +425,8 @@
    2.52            (do_output, (options, (verbose, (browser_info, (parent,
    2.53              (name, info.theories)))))))
    2.54      }
    2.55 -    new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap, output, do_output)
    2.56 +    new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap,
    2.57 +      output, do_output, Time.seconds(options.real("timeout")))
    2.58    }
    2.59  
    2.60  
    2.61 @@ -525,10 +549,12 @@
    2.62  
    2.63                  File.write(output_dir + log(name), out)
    2.64                  echo(name + " FAILED")
    2.65 -                echo("(see also " + (output_dir + log(name)).file.toString + ")")
    2.66 -                val lines = split_lines(out)
    2.67 -                val tail = lines.drop(lines.length - 20 max 0)
    2.68 -                echo("\n" + cat_lines(tail))
    2.69 +                if (rc != 130) {
    2.70 +                  echo("(see also " + (output_dir + log(name)).file.toString + ")")
    2.71 +                  val lines = split_lines(out)
    2.72 +                  val tail = lines.drop(lines.length - 20 max 0)
    2.73 +                  echo("\n" + cat_lines(tail))
    2.74 +                }
    2.75  
    2.76                  no_heap
    2.77                }