src/Pure/System/build.scala
changeset 48511 37999ee01156
parent 48509 4854ced3e9d7
child 48528 784c6f63d79c
     1.1 --- a/src/Pure/System/build.scala	Thu Jul 26 12:32:25 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 26 12:59:09 2012 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4    /* jobs */
     1.5  
     1.6    private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
     1.7 -    val output_path: Option[Path])
     1.8 +    output: Path, do_output: Boolean)
     1.9    {
    1.10      private val args_file = File.tmp_file("args")
    1.11      private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    1.12 @@ -332,9 +332,10 @@
    1.13      def terminate: Unit = thread.interrupt
    1.14      def is_finished: Boolean = result.is_finished
    1.15      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    1.16 +    def output_path: Option[Path] = if (do_output) Some(output) else None
    1.17    }
    1.18  
    1.19 -  private def start_job(name: String, info: Session.Info, output_path: Option[Path],
    1.20 +  private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
    1.21      options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
    1.22    {
    1.23      // global browser info dir
    1.24 @@ -352,21 +353,26 @@
    1.25      val parent = info.parent.getOrElse("")
    1.26      val parent_base_name = info.parent_base_name.getOrElse("")
    1.27  
    1.28 -    val output =
    1.29 -      output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" }
    1.30 -
    1.31      val cwd = info.dir.file
    1.32 -    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output)
    1.33 +    val env =
    1.34 +      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
    1.35      val script =
    1.36 -      if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
    1.37 +      if (is_pure(name)) {
    1.38 +        if (do_output) "./build " + name + " \"$OUTPUT\""
    1.39 +        else """ rm -f "$OUTPUT"; ./build """ + name
    1.40 +      }
    1.41        else {
    1.42          """
    1.43          . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    1.44          """ +
    1.45 -          (if (output_path.isDefined)
    1.46 -            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
    1.47 +          (if (do_output)
    1.48 +            """
    1.49 +            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
    1.50 +            """
    1.51            else
    1.52 -            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
    1.53 +            """
    1.54 +            rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
    1.55 +            """) +
    1.56          """
    1.57          RC="$?"
    1.58  
    1.59 @@ -384,10 +390,10 @@
    1.60        import XML.Encode._
    1.61            pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    1.62              pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
    1.63 -          (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
    1.64 +          (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    1.65              (name, (info.base_name, info.theories)))))))))
    1.66      }
    1.67 -    new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path)
    1.68 +    new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
    1.69    }
    1.70  
    1.71  
    1.72 @@ -431,7 +437,7 @@
    1.73  
    1.74    def build(
    1.75      all_sessions: Boolean = false,
    1.76 -    build_images: Boolean = false,
    1.77 +    build_heap: Boolean = false,
    1.78      more_dirs: List[Path] = Nil,
    1.79      session_groups: List[String] = Nil,
    1.80      max_jobs: Int = 1,
    1.81 @@ -496,17 +502,15 @@
    1.82        { // check/start next job
    1.83          pending.dequeue(running.isDefinedAt(_)) match {
    1.84            case Some((name, info)) =>
    1.85 -            val output =
    1.86 -              if (build_images || queue.is_inner(name))
    1.87 -                Some(output_dir + Path.basic(name))
    1.88 -              else None
    1.89 +            val output = output_dir + Path.basic(name)
    1.90 +            val do_output = build_heap || queue.is_inner(name)
    1.91  
    1.92              val current =
    1.93              {
    1.94                input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
    1.95                  case Some(dir) =>
    1.96                    check_stamps(dir, name) match {
    1.97 -                    case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty)
    1.98 +                    case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
    1.99                      case None => false
   1.100                    }
   1.101                  case None => false
   1.102 @@ -515,8 +519,9 @@
   1.103              if (current || no_build)
   1.104                loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
   1.105              else if (info.parent.map(results(_)).forall(_ == 0)) {
   1.106 -              echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
   1.107 -              val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
   1.108 +              echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.109 +              val job =
   1.110 +                start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)
   1.111                loop(pending, running + (name -> job), results)
   1.112              }
   1.113              else {
   1.114 @@ -547,14 +552,14 @@
   1.115        args.toList match {
   1.116          case
   1.117            Properties.Value.Boolean(all_sessions) ::
   1.118 -          Properties.Value.Boolean(build_images) ::
   1.119 +          Properties.Value.Boolean(build_heap) ::
   1.120            Properties.Value.Int(max_jobs) ::
   1.121            Properties.Value.Boolean(no_build) ::
   1.122            Properties.Value.Boolean(system_mode) ::
   1.123            Properties.Value.Boolean(timing) ::
   1.124            Properties.Value.Boolean(verbose) ::
   1.125            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   1.126 -            build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
   1.127 +            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
   1.128                max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
   1.129          case _ => error("Bad arguments:\n" + cat_lines(args))
   1.130        }