338 def terminate: Unit = thread.interrupt |
338 def terminate: Unit = thread.interrupt |
339 def is_finished: Boolean = result.is_finished |
339 def is_finished: Boolean = result.is_finished |
340 def join: (String, String, Int) = { val res = result.join; args_file.delete; res } |
340 def join: (String, String, Int) = { val res = result.join; args_file.delete; res } |
341 } |
341 } |
342 |
342 |
343 private def start_job(save: Boolean, name: String, info: Session.Info): Job = |
343 private def start_job(name: String, info: Session.Info, output: Option[String]): Job = |
344 { |
344 { |
345 val parent = info.parent.getOrElse("") |
345 val parent = info.parent.getOrElse("") |
346 |
346 |
347 val cwd = info.dir.file |
347 val cwd = info.dir.file |
348 val env = Map("INPUT" -> parent, "TARGET" -> name) |
348 val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse("")) |
349 val script = |
349 val script = |
350 if (is_pure(name)) "./build " + (if (save) "-b " else "") + name |
350 if (is_pure(name)) "./build " + name + " \"$OUTPUT\"" |
351 else { |
351 else { |
352 """ |
352 """ |
353 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
353 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
354 """ + |
354 """ + |
355 (if (save) |
355 (if (output.isDefined) |
356 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """ |
356 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """ |
357 else |
357 else |
358 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) + |
358 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) + |
359 """ |
359 """ |
360 RC="$?" |
360 RC="$?" |
361 |
361 |
370 } |
370 } |
371 val args_xml = |
371 val args_xml = |
372 { |
372 { |
373 import XML.Encode._ |
373 import XML.Encode._ |
374 pair(bool, pair(string, pair(string, list(string))))( |
374 pair(bool, pair(string, pair(string, list(string))))( |
375 save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode)))) |
375 output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode)))) |
376 } |
376 } |
377 new Job(cwd, env, script, YXML.string_of_body(args_xml)) |
377 new Job(cwd, env, script, YXML.string_of_body(args_xml)) |
378 } |
378 } |
379 |
379 |
380 |
380 |
382 |
382 |
383 private def echo(msg: String) { java.lang.System.out.println(msg) } |
383 private def echo(msg: String) { java.lang.System.out.println(msg) } |
384 private def sleep(): Unit = Thread.sleep(500) |
384 private def sleep(): Unit = Thread.sleep(500) |
385 |
385 |
386 def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int, |
386 def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int, |
387 list_only: Boolean, verbose: Boolean, |
387 list_only: Boolean, system_mode: Boolean, verbose: Boolean, |
388 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = |
388 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = |
389 { |
389 { |
390 val options = (Options.init() /: more_options)(_.define_simple(_)) |
390 val options = (Options.init() /: more_options)(_.define_simple(_)) |
391 val queue = find_sessions(options, all_sessions, sessions, more_dirs) |
391 val queue = find_sessions(options, all_sessions, sessions, more_dirs) |
392 val deps = dependencies(queue) |
392 val deps = dependencies(queue) |
393 |
393 |
|
394 val (output_dir, browser_info) = |
|
395 if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info")) |
|
396 else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO")) |
394 |
397 |
395 // prepare browser info dir |
398 // prepare browser info dir |
396 if (options.bool("browser_info") && |
399 if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) |
397 !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile) |
400 { |
398 { |
401 browser_info.file.mkdirs() |
399 Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs() |
402 File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
400 File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"), |
403 browser_info + Path.explode("isabelle.gif")) |
401 Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif")) |
404 File.write(browser_info + Path.explode("index.html"), |
402 File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"), |
405 File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
403 File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) + |
406 File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
404 File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) + |
407 File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
405 File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template"))) |
|
406 } |
408 } |
407 |
409 |
408 // prepare log dir |
410 // prepare log dir |
409 val log_dir = Path.explode("$ISABELLE_OUTPUT/log") |
411 val log_dir = output_dir + Path.explode("log") |
410 log_dir.file.mkdirs() |
412 log_dir.file.mkdirs() |
411 |
413 |
412 // scheduler loop |
414 // scheduler loop |
413 @tailrec def loop( |
415 @tailrec def loop( |
414 pending: Session.Queue, |
416 pending: Session.Queue, |
445 if (list_only) { |
447 if (list_only) { |
446 echo(name + " in " + info.dir) |
448 echo(name + " in " + info.dir) |
447 loop(pending - name, running, results + (name -> 0)) |
449 loop(pending - name, running, results + (name -> 0)) |
448 } |
450 } |
449 else if (info.parent.map(results(_)).forall(_ == 0)) { |
451 else if (info.parent.map(results(_)).forall(_ == 0)) { |
450 val save = build_images || queue.is_inner(name) |
452 val output = |
451 echo((if (save) "Building " else "Running ") + name + " ...") |
453 if (build_images || queue.is_inner(name)) |
452 val job = start_job(save, name, info) |
454 Some(Isabelle_System.standard_path(output_dir + Path.basic(name))) |
|
455 else None |
|
456 echo((if (output.isDefined) "Building " else "Running ") + name + " ...") |
|
457 val job = start_job(name, info, output) |
453 loop(pending, running + (name -> job), results) |
458 loop(pending, running + (name -> job), results) |
454 } |
459 } |
455 else { |
460 else { |
456 echo(name + " CANCELLED") |
461 echo(name + " CANCELLED") |
457 loop(pending - name, running, results + (name -> 1)) |
462 loop(pending - name, running, results + (name -> 1)) |
475 case |
480 case |
476 Properties.Value.Boolean(all_sessions) :: |
481 Properties.Value.Boolean(all_sessions) :: |
477 Properties.Value.Boolean(build_images) :: |
482 Properties.Value.Boolean(build_images) :: |
478 Properties.Value.Int(max_jobs) :: |
483 Properties.Value.Int(max_jobs) :: |
479 Properties.Value.Boolean(list_only) :: |
484 Properties.Value.Boolean(list_only) :: |
|
485 Properties.Value.Boolean(system_mode) :: |
480 Properties.Value.Boolean(verbose) :: |
486 Properties.Value.Boolean(verbose) :: |
481 Command_Line.Chunks(more_dirs, options, sessions) => |
487 Command_Line.Chunks(more_dirs, options, sessions) => |
482 build(all_sessions, build_images, max_jobs, list_only, verbose, |
488 build(all_sessions, build_images, max_jobs, list_only, system_mode, |
483 more_dirs.map(Path.explode), options, sessions) |
489 verbose, more_dirs.map(Path.explode), options, sessions) |
484 case _ => error("Bad arguments:\n" + cat_lines(args)) |
490 case _ => error("Bad arguments:\n" + cat_lines(args)) |
485 } |
491 } |
486 } |
492 } |
487 } |
493 } |
488 } |
494 } |