318 |
318 |
319 |
319 |
320 /* jobs */ |
320 /* jobs */ |
321 |
321 |
322 private class Job(cwd: JFile, env: Map[String, String], script: String, args: String, |
322 private class Job(cwd: JFile, env: Map[String, String], script: String, args: String, |
323 val output_path: Option[Path]) |
323 output: Path, do_output: Boolean) |
324 { |
324 { |
325 private val args_file = File.tmp_file("args") |
325 private val args_file = File.tmp_file("args") |
326 private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) |
326 private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) |
327 File.write(args_file, args) |
327 File.write(args_file, args) |
328 |
328 |
330 Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) } |
330 Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) } |
331 |
331 |
332 def terminate: Unit = thread.interrupt |
332 def terminate: Unit = thread.interrupt |
333 def is_finished: Boolean = result.is_finished |
333 def is_finished: Boolean = result.is_finished |
334 def join: (String, String, Int) = { val res = result.join; args_file.delete; res } |
334 def join: (String, String, Int) = { val res = result.join; args_file.delete; res } |
335 } |
335 def output_path: Option[Path] = if (do_output) Some(output) else None |
336 |
336 } |
337 private def start_job(name: String, info: Session.Info, output_path: Option[Path], |
337 |
|
338 private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean, |
338 options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = |
339 options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = |
339 { |
340 { |
340 // global browser info dir |
341 // global browser info dir |
341 if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) |
342 if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) |
342 { |
343 { |
350 } |
351 } |
351 |
352 |
352 val parent = info.parent.getOrElse("") |
353 val parent = info.parent.getOrElse("") |
353 val parent_base_name = info.parent_base_name.getOrElse("") |
354 val parent_base_name = info.parent_base_name.getOrElse("") |
354 |
355 |
355 val output = |
|
356 output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" } |
|
357 |
|
358 val cwd = info.dir.file |
356 val cwd = info.dir.file |
359 val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output) |
357 val env = |
|
358 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output)) |
360 val script = |
359 val script = |
361 if (is_pure(name)) "./build " + name + " \"$OUTPUT\"" |
360 if (is_pure(name)) { |
|
361 if (do_output) "./build " + name + " \"$OUTPUT\"" |
|
362 else """ rm -f "$OUTPUT"; ./build """ + name |
|
363 } |
362 else { |
364 else { |
363 """ |
365 """ |
364 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
366 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
365 """ + |
367 """ + |
366 (if (output_path.isDefined) |
368 (if (do_output) |
367 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """ |
369 """ |
|
370 "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" |
|
371 """ |
368 else |
372 else |
369 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) + |
373 """ |
|
374 rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" |
|
375 """) + |
370 """ |
376 """ |
371 RC="$?" |
377 RC="$?" |
372 |
378 |
373 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
379 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
374 |
380 |
382 val args_xml = |
388 val args_xml = |
383 { |
389 { |
384 import XML.Encode._ |
390 import XML.Encode._ |
385 pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, |
391 pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, |
386 pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( |
392 pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( |
387 (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name, |
393 (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, |
388 (name, (info.base_name, info.theories))))))))) |
394 (name, (info.base_name, info.theories))))))))) |
389 } |
395 } |
390 new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path) |
396 new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output) |
391 } |
397 } |
392 |
398 |
393 |
399 |
394 /* log files and corresponding heaps */ |
400 /* log files and corresponding heaps */ |
395 |
401 |
429 |
435 |
430 /* build */ |
436 /* build */ |
431 |
437 |
432 def build( |
438 def build( |
433 all_sessions: Boolean = false, |
439 all_sessions: Boolean = false, |
434 build_images: Boolean = false, |
440 build_heap: Boolean = false, |
435 more_dirs: List[Path] = Nil, |
441 more_dirs: List[Path] = Nil, |
436 session_groups: List[String] = Nil, |
442 session_groups: List[String] = Nil, |
437 max_jobs: Int = 1, |
443 max_jobs: Int = 1, |
438 no_build: Boolean = false, |
444 no_build: Boolean = false, |
439 build_options: List[String] = Nil, |
445 build_options: List[String] = Nil, |
494 } |
500 } |
495 else if (running.size < (max_jobs max 1)) |
501 else if (running.size < (max_jobs max 1)) |
496 { // check/start next job |
502 { // check/start next job |
497 pending.dequeue(running.isDefinedAt(_)) match { |
503 pending.dequeue(running.isDefinedAt(_)) match { |
498 case Some((name, info)) => |
504 case Some((name, info)) => |
499 val output = |
505 val output = output_dir + Path.basic(name) |
500 if (build_images || queue.is_inner(name)) |
506 val do_output = build_heap || queue.is_inner(name) |
501 Some(output_dir + Path.basic(name)) |
|
502 else None |
|
503 |
507 |
504 val current = |
508 val current = |
505 { |
509 { |
506 input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match { |
510 input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match { |
507 case Some(dir) => |
511 case Some(dir) => |
508 check_stamps(dir, name) match { |
512 check_stamps(dir, name) match { |
509 case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty) |
513 case Some((s, h)) => s == make_stamp(name) && (h || !do_output) |
510 case None => false |
514 case None => false |
511 } |
515 } |
512 case None => false |
516 case None => false |
513 } |
517 } |
514 } |
518 } |
515 if (current || no_build) |
519 if (current || no_build) |
516 loop(pending - name, running, results + (name -> (if (current) 0 else 1))) |
520 loop(pending - name, running, results + (name -> (if (current) 0 else 1))) |
517 else if (info.parent.map(results(_)).forall(_ == 0)) { |
521 else if (info.parent.map(results(_)).forall(_ == 0)) { |
518 echo((if (output.isDefined) "Building " else "Running ") + name + " ...") |
522 echo((if (do_output) "Building " else "Running ") + name + " ...") |
519 val job = start_job(name, info, output, info.options, timing, verbose, browser_info) |
523 val job = |
|
524 start_job(name, info, output, do_output, info.options, timing, verbose, browser_info) |
520 loop(pending, running + (name -> job), results) |
525 loop(pending, running + (name -> job), results) |
521 } |
526 } |
522 else { |
527 else { |
523 echo(name + " CANCELLED") |
528 echo(name + " CANCELLED") |
524 loop(pending - name, running, results + (name -> 1)) |
529 loop(pending - name, running, results + (name -> 1)) |
545 { |
550 { |
546 Command_Line.tool { |
551 Command_Line.tool { |
547 args.toList match { |
552 args.toList match { |
548 case |
553 case |
549 Properties.Value.Boolean(all_sessions) :: |
554 Properties.Value.Boolean(all_sessions) :: |
550 Properties.Value.Boolean(build_images) :: |
555 Properties.Value.Boolean(build_heap) :: |
551 Properties.Value.Int(max_jobs) :: |
556 Properties.Value.Int(max_jobs) :: |
552 Properties.Value.Boolean(no_build) :: |
557 Properties.Value.Boolean(no_build) :: |
553 Properties.Value.Boolean(system_mode) :: |
558 Properties.Value.Boolean(system_mode) :: |
554 Properties.Value.Boolean(timing) :: |
559 Properties.Value.Boolean(timing) :: |
555 Properties.Value.Boolean(verbose) :: |
560 Properties.Value.Boolean(verbose) :: |
556 Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) => |
561 Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) => |
557 build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups, |
562 build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups, |
558 max_jobs, no_build, build_options, system_mode, timing, verbose, sessions) |
563 max_jobs, no_build, build_options, system_mode, timing, verbose, sessions) |
559 case _ => error("Bad arguments:\n" + cat_lines(args)) |
564 case _ => error("Bad arguments:\n" + cat_lines(args)) |
560 } |
565 } |
561 } |
566 } |
562 } |
567 } |