# HG changeset patch # User wenzelm # Date 1343300349 -7200 # Node ID 37999ee01156fe3e48ff8215ee8fdfc911185776 # Parent 8f3069015441db73efc0faac2fc3ee154dbcaf00 remove old output heaps, to ensure that result is valid wrt. check_stamps; tuned signature; diff -r 8f3069015441 -r 37999ee01156 lib/Tools/build --- a/lib/Tools/build Thu Jul 26 12:32:25 2012 +0200 +++ b/lib/Tools/build Thu Jul 26 12:59:09 2012 +0200 @@ -27,7 +27,7 @@ echo echo " Options are:" echo " -a all sessions" - echo " -b build target images" + echo " -b build heap images" echo " -d DIR include session directory with ROOT file" echo " -g NAME include session group NAME" echo " -j INT maximum number of jobs (default 1)" @@ -58,7 +58,7 @@ ## process command line ALL_SESSIONS=false -BUILD_IMAGES=false +BUILD_HEAP=false declare -a MORE_DIRS=() declare -a SESSION_GROUPS=() MAX_JOBS=1 @@ -75,7 +75,7 @@ ALL_SESSIONS="true" ;; b) - BUILD_IMAGES="true" + BUILD_HEAP="true" ;; d) MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" @@ -126,7 +126,7 @@ fi "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ + "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?" diff -r 8f3069015441 -r 37999ee01156 src/Pure/System/build.ML --- a/src/Pure/System/build.ML Thu Jul 26 12:32:25 2012 +0200 +++ b/src/Pure/System/build.ML Thu Jul 26 12:59:09 2012 +0200 @@ -50,7 +50,7 @@ fun build args_file = let - val (save, (options, (timing, (verbose, (browser_info, (parent_base_name, + val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, (name, (base_name, theories)))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in @@ -59,7 +59,7 @@ end; val _ = - Session.init save false + Session.init do_output false (Options.bool options "browser_info") browser_info (Options.string options "document") (Options.bool options "document_graph") @@ -70,7 +70,7 @@ verbose; val _ = Session.with_timing name timing (List.app use_theories) theories; val _ = Session.finish (); - val _ = if save then () else quit (); + val _ = if do_output then () else quit (); in () end handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); diff -r 8f3069015441 -r 37999ee01156 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Thu Jul 26 12:32:25 2012 +0200 +++ b/src/Pure/System/build.scala Thu Jul 26 12:59:09 2012 +0200 @@ -320,7 +320,7 @@ /* jobs */ private class Job(cwd: JFile, env: Map[String, String], script: String, args: String, - val output_path: Option[Path]) + output: Path, do_output: Boolean) { private val args_file = File.tmp_file("args") private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) @@ -332,9 +332,10 @@ def terminate: Unit = thread.interrupt def is_finished: Boolean = result.is_finished def join: (String, String, Int) = { val res = result.join; args_file.delete; res } + def output_path: Option[Path] = if (do_output) Some(output) else None } - private def start_job(name: String, info: Session.Info, output_path: Option[Path], + private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean, options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = { // global browser info dir @@ -352,21 +353,26 @@ val parent = info.parent.getOrElse("") val parent_base_name = info.parent_base_name.getOrElse("") - val output = - output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" } - val cwd = info.dir.file - val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output) + val env = + Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output)) val script = - if (is_pure(name)) "./build " + name + " \"$OUTPUT\"" + if (is_pure(name)) { + if (do_output) "./build " + name + " \"$OUTPUT\"" + else """ rm -f "$OUTPUT"; ./build """ + name + } else { """ . "$ISABELLE_HOME/lib/scripts/timestart.bash" """ + - (if (output_path.isDefined) - """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """ + (if (do_output) + """ + "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" + """ else - """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) + + """ + rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" + """) + """ RC="$?" @@ -384,10 +390,10 @@ import XML.Encode._ pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( - (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name, + (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, (name, (info.base_name, info.theories))))))))) } - new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path) + new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output) } @@ -431,7 +437,7 @@ def build( all_sessions: Boolean = false, - build_images: Boolean = false, + build_heap: Boolean = false, more_dirs: List[Path] = Nil, session_groups: List[String] = Nil, max_jobs: Int = 1, @@ -496,17 +502,15 @@ { // check/start next job pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => - val output = - if (build_images || queue.is_inner(name)) - Some(output_dir + Path.basic(name)) - else None + val output = output_dir + Path.basic(name) + val do_output = build_heap || queue.is_inner(name) val current = { input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match { case Some(dir) => check_stamps(dir, name) match { - case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty) + case Some((s, h)) => s == make_stamp(name) && (h || !do_output) case None => false } case None => false @@ -515,8 +519,9 @@ if (current || no_build) loop(pending - name, running, results + (name -> (if (current) 0 else 1))) else if (info.parent.map(results(_)).forall(_ == 0)) { - echo((if (output.isDefined) "Building " else "Running ") + name + " ...") - val job = start_job(name, info, output, info.options, timing, verbose, browser_info) + echo((if (do_output) "Building " else "Running ") + name + " ...") + val job = + start_job(name, info, output, do_output, info.options, timing, verbose, browser_info) loop(pending, running + (name -> job), results) } else { @@ -547,14 +552,14 @@ args.toList match { case Properties.Value.Boolean(all_sessions) :: - Properties.Value.Boolean(build_images) :: + Properties.Value.Boolean(build_heap) :: Properties.Value.Int(max_jobs) :: Properties.Value.Boolean(no_build) :: Properties.Value.Boolean(system_mode) :: Properties.Value.Boolean(timing) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) => - build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups, + build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups, max_jobs, no_build, build_options, system_mode, timing, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } diff -r 8f3069015441 -r 37999ee01156 src/Pure/build --- a/src/Pure/build Thu Jul 26 12:32:25 2012 +0200 +++ b/src/Pure/build Thu Jul 26 12:59:09 2012 +0200 @@ -12,7 +12,7 @@ function usage() { echo - echo "Usage: $PRG TARGET OUTPUT" + echo "Usage: $PRG TARGET [OUTPUT]" echo exit 1 } @@ -30,7 +30,10 @@ # args -if [ "$#" -eq 2 ]; then +if [ "$#" -eq 1 ]; then + TARGET="$1"; shift + OUTPUT=""; shift +elif [ "$#" -eq 2 ]; then TARGET="$1"; shift OUTPUT="$1"; shift else