src/Pure/Build/build_manager.scala
changeset 80279 02424b81472a
parent 80278 21b30f1fa331
child 80280 7987b33fb6c5
equal deleted inserted replaced
80278:21b30f1fa331 80279:02424b81472a
   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 */