565 object State { |
565 object State { |
566 def empty: State = new State(Map.empty, Map.empty) |
566 def empty: State = new State(Map.empty, Map.empty) |
567 } |
567 } |
568 |
568 |
569 class State private( |
569 class State private( |
570 process_futures: Map[String, Future[Bash.Process]], |
570 process_futures: Map[String, Future[Build_Process]], |
571 result_futures: Map[String, Future[Process_Result]] |
571 result_futures: Map[String, Future[Process_Result]] |
572 ) { |
572 ) { |
573 def is_empty = process_futures.isEmpty && result_futures.isEmpty |
573 def is_empty = process_futures.isEmpty && result_futures.isEmpty |
574 |
574 |
575 def init(build_config: Build_Config, job: Job, context: Context): State = { |
575 def init(build_config: Build_Config, job: Job, context: Context): State = { |
576 val process_future = Future.fork(context.process(build_config)) |
576 val process_future = Future.fork(Build_Process.open(build_config, context)) |
577 val result_future = |
577 val result_future = |
578 Future.fork( |
578 Future.fork( |
579 process_future.join_result match { |
579 process_future.join_result match { |
580 case Exn.Res(process) => context.run(process) |
580 case Exn.Res(process) => process.run() |
581 case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt) |
581 case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt) |
582 }) |
582 }) |
583 new State( |
583 new State( |
584 process_futures + (job.name -> process_future), |
584 process_futures + (job.name -> process_future), |
585 result_futures + (job.name -> result_future)) |
585 result_futures + (job.name -> result_future)) |
598 } |
598 } |
599 |
599 |
600 def cancel(cancelled: List[String]): State = { |
600 def cancel(cancelled: List[String]): State = { |
601 for (name <- cancelled) { |
601 for (name <- cancelled) { |
602 val process_future = process_futures(name) |
602 val process_future = process_futures(name) |
603 if (process_future.is_finished) process_future.join.interrupt() |
603 if (process_future.is_finished) process_future.join.cancel() |
604 else process_future.cancel() |
604 else process_future.cancel() |
605 } |
605 } |
606 |
606 |
607 new State(process_futures.filterNot((name, _) => cancelled.contains(name)), result_futures) |
607 new State(process_futures.filterNot((name, _) => cancelled.contains(name)), result_futures) |
608 } |
608 } |
1072 def apply(store: Store, elem: T, build_hosts: List[Build_Cluster.Host] = Nil): Context = |
1072 def apply(store: Store, elem: T, build_hosts: List[Build_Cluster.Host] = Nil): Context = |
1073 new Context(store, store.dir(elem), build_hosts) |
1073 new Context(store, store.dir(elem), build_hosts) |
1074 } |
1074 } |
1075 |
1075 |
1076 class Context private(store: Store, val dir: Path, val build_hosts: List[Build_Cluster.Host]) { |
1076 class Context private(store: Store, val dir: Path, val build_hosts: List[Build_Cluster.Host]) { |
|
1077 def isabelle_identifier: String = store.identifier |
|
1078 |
1077 private val log_file = dir + Path.basic("log") |
1079 private val log_file = dir + Path.basic("log") |
1078 val progress = new File_Progress(log_file, verbose = true) |
1080 val progress = new File_Progress(log_file, verbose = true) |
1079 def log: String = |
1081 def log: String = |
1080 Exn.capture(File.read(log_file)) match { |
1082 Exn.capture(File.read(log_file)) match { |
1081 case Exn.Exn(_) => "" |
1083 case Exn.Exn(_) => "" |
1094 other |
1096 other |
1095 } |
1097 } |
1096 |
1098 |
1097 def remove(): Unit = Isabelle_System.rm_tree(dir) |
1099 def remove(): Unit = Isabelle_System.rm_tree(dir) |
1098 |
1100 |
1099 lazy val ssh = store.open_ssh() |
1101 def ssh = store.open_ssh() |
1100 |
1102 } |
1101 def process(build_config: Build_Config): Bash.Process = { |
1103 |
1102 val isabelle = Other_Isabelle(dir, store.identifier, ssh, progress) |
1104 |
1103 |
1105 /* build process */ |
1104 val init_components = |
1106 |
1105 for { |
1107 object Build_Process { |
1106 component <- build_config.components |
1108 def open(build_config: Build_Config, context: Context): Build_Process = |
1107 target = dir + Sync.DIRS + Path.basic(component.name) |
1109 new Build_Process(context.ssh, build_config, context) |
1108 if Components.is_component_dir(target) |
1110 } |
1109 } yield "init_component " + quote(target.absolute.implode) |
1111 |
1110 |
1112 class Build_Process(ssh: SSH.Session, build_config: Build_Config, context: Context) { |
1111 isabelle.init(other_settings = isabelle.init_components() ::: init_components, |
1113 private val _dir = ssh.tmp_dir() |
1112 fresh = build_config.fresh_build, echo = true) |
1114 private val _progress = context.progress |
1113 |
1115 |
1114 val cmd = build_config.command(build_hosts) |
1116 private val _isabelle = |
1115 progress.echo("isabelle" + cmd) |
1117 try { |
1116 |
1118 val rsync_context = Rsync.Context(ssh = ssh) |
1117 val script = File.bash_path(Isabelle_Tool.exe(isabelle.isabelle_home)) + cmd |
1119 val source = File.standard_path(context.dir) |
1118 ssh.bash_process(isabelle.bash_context(script), settings = false) |
1120 Rsync.exec(rsync_context, clean = true, args = List("--", Url.direct_path(source), |
1119 } |
1121 rsync_context.target(_dir))).check |
1120 |
1122 |
1121 def run(process: Bash.Process): Process_Result = { |
1123 Other_Isabelle(_dir, context.isabelle_identifier, ssh, _progress) |
|
1124 } |
|
1125 catch { case exn: Throwable => close(); throw exn } |
|
1126 |
|
1127 private val _process = |
|
1128 try { |
|
1129 val init_components = |
|
1130 for { |
|
1131 component <- build_config.components |
|
1132 target = _dir + Sync.DIRS + Path.basic(component.name) |
|
1133 if Components.is_component_dir(target) |
|
1134 } yield "init_component " + quote(target.absolute.implode) |
|
1135 |
|
1136 _isabelle.init( |
|
1137 other_settings = _isabelle.init_components() ::: init_components, |
|
1138 fresh = build_config.fresh_build, echo = true) |
|
1139 |
|
1140 val cmd = build_config.command(context.build_hosts) |
|
1141 _progress.echo("isabelle" + cmd) |
|
1142 |
|
1143 val script = File.bash_path(Isabelle_Tool.exe(_isabelle.isabelle_home)) + cmd |
|
1144 ssh.bash_process(_isabelle.bash_context(script), settings = false) |
|
1145 } |
|
1146 catch { case exn: Throwable => close(); throw exn } |
|
1147 |
|
1148 def run(): Process_Result = { |
1122 val process_result = |
1149 val process_result = |
1123 process.result(progress_stdout = progress.echo(_), progress_stderr = progress.echo(_)) |
1150 _process.result(progress_stdout = _progress.echo(_), progress_stderr = _progress.echo(_)) |
|
1151 close() |
|
1152 process_result |
|
1153 } |
|
1154 |
|
1155 def cancel(): Unit = Option(_process).foreach(_.interrupt()) |
|
1156 |
|
1157 def close(): Unit = { |
|
1158 Option(_dir).foreach(ssh.rm_tree) |
1124 ssh.close() |
1159 ssh.close() |
1125 process_result |
|
1126 } |
1160 } |
1127 } |
1161 } |
1128 |
1162 |
1129 |
1163 |
1130 /* build manager store */ |
1164 /* build manager store */ |