| author | paulson | 
| Thu, 19 Oct 2017 17:16:13 +0100 | |
| changeset 66885 | d3d508b23d1d | 
| parent 65594 | 659305708959 | 
| child 67067 | 02729ced9b1e | 
| permissions | -rw-r--r-- | 
| 64161 | 1 | /* Title: Pure/Admin/remote_dmg.scala | 
| 64143 | 2 | Author: Makarius | 
| 3 | ||
| 4 | Build dmg on remote Mac OS X system. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | object Remote_DMG | |
| 11 | {
 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 12 | def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "") | 
| 64143 | 13 |   {
 | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 14 | ssh.with_tmp_dir(remote_dir => | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 15 |       {
 | 
| 64304 | 16 | val cd = "cd " + ssh.bash_path(remote_dir) + "; " | 
| 64143 | 17 | |
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 18 |         ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 19 | ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 20 | ssh.execute( | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 21 | cd + "hdiutil create -srcfolder root" + | 
| 64304 | 22 | (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) + | 
| 64256 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 23 | " dmg.dmg").check | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 24 |         ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
 | 
| 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 wenzelm parents: 
64233diff
changeset | 25 | }) | 
| 64143 | 26 | } | 
| 27 | ||
| 28 | ||
| 29 | /* Isabelle tool wrapper */ | |
| 30 | ||
| 64161 | 31 | val isabelle_tool = | 
| 32 |     Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
 | |
| 33 |     {
 | |
| 34 |       Command_Line.tool0 {
 | |
| 65594 | 35 | var port = 0 | 
| 64161 | 36 | var volume_name = "" | 
| 64143 | 37 | |
| 64161 | 38 |         val getopts = Getopts("""
 | 
| 64143 | 39 | Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE | 
| 40 | ||
| 41 | Options are: | |
| 65594 | 42 | -p PORT alternative SSH port | 
| 64143 | 43 | -V NAME specify volume name | 
| 44 | ||
| 45 | Turn the contents of a tar.gz file into a dmg file -- produced on a remote | |
| 46 | Mac OS X system. | |
| 47 | """, | |
| 64161 | 48 | "p:" -> (arg => port = Value.Int.parse(arg)), | 
| 49 | "V:" -> (arg => volume_name = arg)) | |
| 64143 | 50 | |
| 64161 | 51 | val more_args = getopts(args) | 
| 52 | val (user, host, tar_gz_file, dmg_file) = | |
| 53 |           more_args match {
 | |
| 64185 | 54 | case List(SSH.Target(user, host), tar_gz_file, dmg_file) => | 
| 64161 | 55 | (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file)) | 
| 56 | case _ => getopts.usage() | |
| 57 | } | |
| 64143 | 58 | |
| 64257 | 59 | val ssh = SSH.init_context(Options.init) | 
| 64161 | 60 | using(ssh.open_session(user = user, host = host, port = port))( | 
| 61 | remote_dmg(_, tar_gz_file, dmg_file, volume_name)) | |
| 62 | } | |
| 63 | }, admin = true) | |
| 64143 | 64 | } |