221 } |
221 } |
222 |
222 |
223 |
223 |
224 /** build release **/ |
224 /** build release **/ |
225 |
225 |
226 /* build heaps on remote server */ |
226 /* build heaps */ |
227 |
227 |
228 private def remote_build_heaps( |
228 private def build_heaps( |
229 options: Options, |
229 options: Options, |
230 platform: Platform.Family.Value, |
230 platform: Platform.Family.Value, |
231 build_sessions: List[String], |
231 build_sessions: List[String], |
232 local_dir: Path): Unit = |
232 local_dir: Path): Unit = |
233 { |
233 { |
234 val server_option = "build_host_" + platform.toString |
234 val server_option = "build_host_" + platform.toString |
235 options.string(server_option) match { |
235 val ssh = |
236 case SSH.Target(user, host) => |
236 options.string(server_option) match { |
237 using(SSH.open_session(options, host = host, user = user))(ssh => |
237 case "" => |
238 Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar => |
238 if (Platform.family == platform) SSH.Local |
239 { |
239 else error("Undefined option " + server_option + ": cannot build heaps") |
240 execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") |
240 case SSH.Target(user, host) => |
241 ssh.with_tmp_dir(remote_dir => |
241 SSH.open_session(options, host = host, user = user) |
242 { |
242 case s => error("Malformed option " + server_option + ": " + quote(s)) |
243 val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") |
243 } |
244 ssh.write_file(remote_tmp_tar, local_tmp_tar) |
244 try { |
245 val remote_commands = |
245 Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar => |
246 List( |
246 { |
247 "cd " + File.bash_path(remote_dir), |
247 execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") |
248 "tar -xf tmp.tar", |
248 ssh.with_tmp_dir(remote_dir => |
249 "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), |
249 { |
250 "tar -cf tmp.tar heaps") |
250 val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") |
251 ssh.execute(remote_commands.mkString(" && ")).check |
251 ssh.write_file(remote_tmp_tar, local_tmp_tar) |
252 ssh.read_file(remote_tmp_tar, local_tmp_tar) |
252 val remote_commands = |
253 }) |
253 List( |
254 execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) |
254 "cd " + File.bash_path(remote_dir), |
255 }) |
255 "tar -xf tmp.tar", |
256 ) |
256 "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), |
257 case s => error("Bad " + server_option + ": " + quote(s)) |
257 "tar -cf tmp.tar heaps") |
258 } |
258 ssh.execute(remote_commands.mkString(" && "), settings = false).check |
|
259 ssh.read_file(remote_tmp_tar, local_tmp_tar) |
|
260 }) |
|
261 execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) |
|
262 }) |
|
263 } |
|
264 finally { ssh.close() } |
259 } |
265 } |
260 |
266 |
261 |
267 |
262 /* Isabelle application */ |
268 /* Isabelle application */ |
263 |
269 |
899 if (more_args.nonEmpty) getopts.usage() |
905 if (more_args.nonEmpty) getopts.usage() |
900 |
906 |
901 if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) |
907 if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) |
902 error("Building for windows requires 7z") |
908 error("Building for windows requires 7z") |
903 |
909 |
|
910 val progress = new Console_Progress() |
904 def make_context(name: String): Release_Context = |
911 def make_context(name: String): Release_Context = |
905 Release_Context(target_dir, |
912 Release_Context(target_dir, |
906 release_name = name, |
913 release_name = name, |
907 components_base = components_base, |
914 components_base = components_base, |
908 progress = new Console_Progress()) |
915 progress = progress) |
909 |
916 |
910 val context = |
917 val context = |
911 if (source_archive.isEmpty) { |
918 if (source_archive.isEmpty) { |
912 val context = make_context(release_name) |
919 val context = make_context(release_name) |
913 val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" |
920 val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" |
914 build_release_archive(context, version, parallel_jobs = parallel_jobs) |
921 build_release_archive(context, version, parallel_jobs = parallel_jobs) |
915 context |
922 context |
916 } |
923 } |
917 else { |
924 else { |
918 val archive = Release_Archive.get(source_archive, rename = release_name) |
925 val archive = |
|
926 Release_Archive.get(source_archive, rename = release_name, progress = progress) |
919 val context = make_context(archive.identifier) |
927 val context = make_context(archive.identifier) |
920 Isabelle_System.new_directory(context.dist_dir) |
928 Isabelle_System.make_directory(context.dist_dir) |
921 use_release_archive(context, archive, id = rev) |
929 use_release_archive(context, archive, id = rev) |
922 context |
930 context |
923 } |
931 } |
924 |
932 |
925 build_release(options, context, afp_rev = afp_rev, platform_families = platform_families, |
933 build_release(options, context, afp_rev = afp_rev, platform_families = platform_families, |