570 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path, |
570 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path, |
571 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |
571 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |
572 File.standard_path(args_file)) |
572 File.standard_path(args_file)) |
573 |
573 |
574 private val script = |
574 private val script = |
575 if (is_pure(name)) { |
575 """ |
576 if (do_output) "./build " + name + " \"$OUTPUT\"" |
576 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
577 else "./build " + name |
577 """ + |
578 } |
578 (if (is_pure(name)) { |
579 else { |
579 val ml_system = Isabelle_System.getenv("ML_SYSTEM") |
|
580 val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system |
|
581 val ml_root = |
|
582 List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML"). |
|
583 find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse |
|
584 error("Missing compatibility file for ML system " + quote(ml_system)) |
|
585 |
|
586 if (name == "RAW") { |
|
587 """ |
|
588 rm -f "$OUTPUT" |
|
589 "$ISABELLE_PROCESS" \ |
|
590 -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \ |
|
591 -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ |
|
592 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
|
593 """ |
|
594 } |
|
595 else { |
|
596 """ |
|
597 rm -f "$OUTPUT" |
|
598 "$ISABELLE_PROCESS" \ |
|
599 -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \ |
|
600 -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ |
|
601 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
|
602 """ |
|
603 } |
|
604 } |
|
605 else if (do_output) |
580 """ |
606 """ |
581 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
607 rm -f "$OUTPUT" |
582 """ + |
608 "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT" |
583 (if (do_output) |
|
584 """ |
|
585 rm -f "$OUTPUT" |
|
586 "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT" |
|
587 """ |
|
588 else |
|
589 """ |
|
590 rm -f "$OUTPUT" |
|
591 "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" |
|
592 """) + |
|
593 """ |
609 """ |
594 RC="$?" |
610 else |
595 |
|
596 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
|
597 |
|
598 if [ "$RC" -eq 0 ]; then |
|
599 echo "Finished $TARGET ($TIMES_REPORT)" >&2 |
|
600 fi |
|
601 |
|
602 exit "$RC" |
|
603 """ |
611 """ |
604 } |
612 rm -f "$OUTPUT" |
|
613 "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" |
|
614 """) + |
|
615 """ |
|
616 RC="$?" |
|
617 |
|
618 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
|
619 |
|
620 if [ "$RC" -eq 0 ]; then |
|
621 echo "Finished $TARGET ($TIMES_REPORT)" >&2 |
|
622 fi |
|
623 |
|
624 exit "$RC" |
|
625 """ |
605 |
626 |
606 private val result = |
627 private val result = |
607 Future.thread("build") { |
628 Future.thread("build") { |
608 Isabelle_System.bash(script, info.dir.file, env, |
629 Isabelle_System.bash(script, info.dir.file, env, |
609 progress_stdout = (line: String) => |
630 progress_stdout = (line: String) => |
921 info.parent match { |
942 info.parent match { |
922 case None => Result(true, no_heap, Some(Process_Result(0))) |
943 case None => Result(true, no_heap, Some(Process_Result(0))) |
923 case Some(parent) => results(parent) |
944 case Some(parent) => results(parent) |
924 } |
945 } |
925 val output = output_dir + Path.basic(name) |
946 val output = output_dir + Path.basic(name) |
926 val do_output = build_heap || queue.is_inner(name) |
947 val do_output = build_heap || is_pure(name) || queue.is_inner(name) |
927 |
948 |
928 val (current, heap) = |
949 val (current, heap) = |
929 { |
950 { |
930 find_log(name + ".gz") match { |
951 find_log(name + ".gz") match { |
931 case Some((dir, path)) => |
952 case Some((dir, path)) => |