1/* Title: Pure/Admin/components.scala 2 Author: Makarius 3 4Isabelle system components. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12 13object Components 14{ 15 /* archive name */ 16 17 object Archive 18 { 19 val suffix: String = ".tar.gz" 20 21 def apply(name: String): String = 22 if (name == "") error("Bad component name: " + quote(name)) 23 else name + suffix 24 25 def unapply(archive: String): Option[String] = 26 { 27 for { 28 name0 <- Library.try_unsuffix(suffix, archive) 29 name <- proper_string(name0) 30 } yield name 31 } 32 33 def get_name(archive: String): String = 34 unapply(archive) getOrElse 35 error("Bad component archive name (expecting .tar.gz): " + quote(archive)) 36 } 37 38 39 /* component collections */ 40 41 val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE") 42 43 def admin(dir: Path): Path = dir + Path.explode("Admin/components") 44 45 def contrib(dir: Path = Path.current, name: String = ""): Path = 46 dir + Path.explode("contrib") + Path.explode(name) 47 48 def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String = 49 { 50 val name = Archive.get_name(archive.file_name) 51 progress.echo("Unpacking " + name) 52 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check 53 name 54 } 55 56 def resolve(base_dir: Path, names: List[String], 57 target_dir: Option[Path] = None, 58 copy_dir: Option[Path] = None, 59 progress: Progress = No_Progress) 60 { 61 Isabelle_System.mkdirs(base_dir) 62 for (name <- names) { 63 val archive_name = Archive(name) 64 val archive = base_dir + Path.explode(archive_name) 65 if (!archive.is_file) { 66 val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name 67 progress.echo("Getting " + remote) 68 Bytes.write(archive, Url.read_bytes(Url(remote))) 69 } 70 for (dir <- copy_dir) { 71 Isabelle_System.mkdirs(dir) 72 File.copy(archive, dir) 73 } 74 unpack(target_dir getOrElse base_dir, archive, progress = progress) 75 } 76 } 77 78 def purge(dir: Path, platform: Platform.Family.Value) 79 { 80 def purge_platforms(platforms: String*): Set[String] = 81 platforms.flatMap(name => List("x86-" + name, "x86_64_32-" + name, "x86_64-" + name)).toSet + 82 "ppc-darwin" 83 val purge_set = 84 platform match { 85 case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows") 86 case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows") 87 case Platform.Family.windows => purge_platforms("linux", "darwin") 88 } 89 90 File.find_files(dir.file, 91 (file: JFile) => file.isDirectory && purge_set(file.getName), 92 include_dirs = true).foreach(Isabelle_System.rm_tree) 93 } 94 95 96 /* component directory content */ 97 98 def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") 99 def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") 100 101 def check_dir(dir: Path): Boolean = 102 settings(dir).is_file || components(dir).is_file 103 104 def read_components(dir: Path): List[String] = 105 split_lines(File.read(components(dir))).filter(_.nonEmpty) 106 107 def write_components(dir: Path, lines: List[String]): Unit = 108 File.write(components(dir), terminate_lines(lines)) 109 110 111 /* component repository content */ 112 113 val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") 114 115 sealed case class SHA1_Digest(sha1: String, file_name: String) 116 { 117 override def toString: String = sha1 + " " + file_name 118 } 119 120 def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = 121 (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => 122 Word.explode(line) match { 123 case Nil => None 124 case List(sha1, name) => Some(SHA1_Digest(sha1, name)) 125 case _ => error("Bad components.sha1 entry: " + quote(line)) 126 }) 127 128 def write_components_sha1(entries: List[SHA1_Digest]) = 129 File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) 130 131 132 133 /** build and publish components **/ 134 135 def build_components( 136 options: Options, 137 components: List[Path], 138 progress: Progress = No_Progress, 139 publish: Boolean = false, 140 force: Boolean = false, 141 update_components_sha1: Boolean = false) 142 { 143 val archives: List[Path] = 144 for (path <- components) yield { 145 path.file_name match { 146 case Archive(_) => path 147 case name => 148 if (!path.is_dir) error("Bad component directory: " + path) 149 else if (!check_dir(path)) { 150 error("Malformed component directory: " + path + 151 "\n (requires " + settings() + " or " + Components.components() + ")") 152 } 153 else { 154 val component_path = path.expand 155 val archive_dir = component_path.dir 156 val archive_name = Archive(name) 157 158 val archive = archive_dir + Path.explode(archive_name) 159 if (archive.is_file && !force) { 160 error("Component archive already exists: " + archive) 161 } 162 163 progress.echo("Packaging " + archive_name) 164 Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), 165 dir = archive_dir).check 166 167 archive 168 } 169 } 170 } 171 172 if ((publish && archives.nonEmpty) || update_components_sha1) { 173 options.string("isabelle_components_server") match { 174 case SSH.Target(user, host) => 175 using(SSH.open_session(options, host = host, user = user))(ssh => 176 { 177 val components_dir = Path.explode(options.string("isabelle_components_dir")) 178 val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) 179 180 for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { 181 error("Bad remote directory: " + dir) 182 } 183 184 if (publish) { 185 for (archive <- archives) { 186 val archive_name = archive.file_name 187 val name = Archive.get_name(archive_name) 188 val remote_component = components_dir + archive.base 189 val remote_contrib = contrib_dir + Path.explode(name) 190 191 // component archive 192 if (ssh.is_file(remote_component) && !force) { 193 error("Remote component archive already exists: " + remote_component) 194 } 195 progress.echo("Uploading " + archive_name) 196 ssh.write_file(remote_component, archive) 197 198 // contrib directory 199 val is_standard_component = 200 Isabelle_System.with_tmp_dir("component")(tmp_dir => 201 { 202 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check 203 check_dir(tmp_dir + Path.explode(name)) 204 }) 205 if (is_standard_component) { 206 if (ssh.is_dir(remote_contrib)) { 207 if (force) ssh.rm_tree(remote_contrib) 208 else error("Remote component directory already exists: " + remote_contrib) 209 } 210 progress.echo("Unpacking remote " + archive_name) 211 ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + 212 ssh.bash_path(remote_component)).check 213 } 214 else { 215 progress.echo_warning("No unpacking of non-standard component: " + archive_name) 216 } 217 } 218 } 219 220 // remote SHA1 digests 221 if (update_components_sha1) { 222 val lines = 223 for { 224 entry <- ssh.read_dir(components_dir) 225 if entry.is_file && entry.name.endsWith(Archive.suffix) 226 } 227 yield { 228 progress.echo("Digesting remote " + entry.name) 229 Library.trim_line( 230 ssh.execute("cd " + ssh.bash_path(components_dir) + 231 "; sha1sum " + Bash.string(entry.name)).check.out) 232 } 233 write_components_sha1(read_components_sha1(lines)) 234 } 235 }) 236 case s => error("Bad isabelle_components_server: " + quote(s)) 237 } 238 } 239 240 // local SHA1 digests 241 { 242 val new_entries = 243 for (archive <- archives) 244 yield { 245 val file_name = archive.file_name 246 progress.echo("Digesting local " + file_name) 247 val sha1 = SHA1.digest(archive).rep 248 SHA1_Digest(sha1, file_name) 249 } 250 val new_names = new_entries.map(_.file_name).toSet 251 252 write_components_sha1( 253 new_entries ::: 254 read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) 255 } 256 } 257 258 259 /* Isabelle tool wrapper */ 260 261 private val relevant_options = 262 List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") 263 264 val isabelle_tool = 265 Isabelle_Tool("build_components", "build and publish Isabelle components", args => 266 { 267 var publish = false 268 var update_components_sha1 = false 269 var force = false 270 var options = Options.init() 271 272 def show_options: String = 273 cat_lines(relevant_options.map(name => options.options(name).print)) 274 275 val getopts = Getopts(""" 276Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... 277 278 Options are: 279 -P publish on SSH server (see options below) 280 -f force: overwrite existing component archives and directories 281 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 282 -u update all SHA1 keys in Isabelle repository Admin/components 283 284 Build and publish Isabelle components as .tar.gz archives on SSH server, 285 depending on system options: 286 287""" + Library.prefix_lines(" ", show_options) + "\n", 288 "P" -> (_ => publish = true), 289 "f" -> (_ => force = true), 290 "o:" -> (arg => options = options + arg), 291 "u" -> (_ => update_components_sha1 = true)) 292 293 val more_args = getopts(args) 294 if (more_args.isEmpty && !update_components_sha1) getopts.usage() 295 296 val progress = new Console_Progress 297 298 build_components(options, more_args.map(Path.explode), progress = progress, 299 publish = publish, force = force, update_components_sha1 = update_components_sha1) 300 }) 301} 302