1/* Title: Pure/Admin/build_release.scala 2 Author: Makarius 3 4Build full Isabelle distribution from repository. 5*/ 6 7package isabelle 8 9 10object Build_Release 11{ 12 /** release info **/ 13 14 sealed case class Bundle_Info( 15 platform: Platform.Family.Value, 16 platform_description: String, 17 name: String) 18 { 19 def path: Path = Path.explode(name) 20 } 21 22 class Release private[Build_Release]( 23 progress: Progress, 24 val date: Date, 25 val dist_name: String, 26 val dist_dir: Path, 27 val dist_version: String, 28 val ident: String) 29 { 30 val isabelle_dir: Path = dist_dir + Path.explode(dist_name) 31 val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") 32 val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") 33 34 def other_isabelle(dir: Path): Other_Isabelle = 35 Other_Isabelle(dir + Path.explode(dist_name), 36 isabelle_identifier = dist_name + "-build", 37 progress = progress) 38 39 def bundle_info(platform: Platform.Family.Value): Bundle_Info = 40 platform match { 41 case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") 42 case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") 43 case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") 44 } 45 } 46 47 48 49 /** generated content **/ 50 51 /* patch release */ 52 53 private def change_file(dir: Path, name: String, f: String => String) 54 { 55 val file = dir + Path.explode(name) 56 File.write(file, f(File.read(file))) 57 } 58 59 private val getsettings_file: String = "lib/scripts/getsettings" 60 61 private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r 62 63 def patch_release(release: Release, is_official: Boolean) 64 { 65 val dir = release.isabelle_dir 66 67 for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) 68 { 69 change_file(dir, name, 70 s => 71 s.replaceAllLiterally("val is_identified = false", "val is_identified = true") 72 .replaceAllLiterally("val is_official = false", "val is_official = " + is_official)) 73 } 74 75 change_file(dir, getsettings_file, 76 s => 77 s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) 78 .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"", 79 "ISABELLE_IDENTIFIER=" + quote(release.dist_name))) 80 81 change_file(dir, "lib/html/library_index_header.template", 82 s => s.replaceAllLiterally("{ISABELLE}", release.dist_name)) 83 84 for { 85 name <- 86 List( 87 "src/Pure/System/distribution.ML", 88 "src/Pure/System/distribution.scala", 89 "lib/Tools/version") } 90 { 91 change_file(dir, name, 92 s => s.replaceAllLiterally("repository version", release.dist_version)) 93 } 94 95 change_file(dir, "README", 96 s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version)) 97 } 98 99 100 /* ANNOUNCE */ 101 102 def make_announce(release: Release) 103 { 104 File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), 105""" 106IMPORTANT NOTE 107============== 108 109This is a snapshot of Isabelle/""" + release.ident + """ from the repository. 110 111""") 112 } 113 114 115 /* NEWS */ 116 117 def make_news(other_isabelle: Other_Isabelle, dist_version: String) 118 { 119 val target = other_isabelle.isabelle_home + Path.explode("doc") 120 val target_fonts = target + Path.explode("fonts") 121 Isabelle_System.mkdirs(target_fonts) 122 other_isabelle.copy_fonts(target_fonts) 123 124 HTML.write_document(target, "NEWS.html", 125 List(HTML.title("NEWS (" + dist_version + ")")), 126 List( 127 HTML.chapter("NEWS"), 128 HTML.source( 129 Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) 130 } 131 132 133 /* bundled components */ 134 135 class Bundled(platform: Option[Platform.Family.Value] = None) 136 { 137 def detect(s: String): Boolean = 138 s.startsWith("#bundled") && !s.startsWith("#bundled ") 139 140 def apply(name: String): String = 141 "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name 142 143 private val Pattern1 = ("""^#bundled:(.*)$""").r 144 private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r 145 146 def unapply(s: String): Option[String] = 147 s match { 148 case Pattern1(name) => Some(name) 149 case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) 150 case _ => None 151 } 152 } 153 154 def record_bundled_components(dir: Path) 155 { 156 val catalogs = 157 List("main", "bundled").map((_, new Bundled())) ::: 158 default_platform_families.flatMap(platform => 159 List(platform.toString, "bundled-" + platform.toString). 160 map((_, new Bundled(platform = Some(platform))))) 161 162 File.append(Components.components(dir), 163 terminate_lines("#bundled components" :: 164 (for { 165 (catalog, bundled) <- catalogs.iterator 166 val path = Components.admin(dir) + Path.basic(catalog) 167 if path.is_file 168 line <- split_lines(File.read(path)) 169 if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") 170 } yield bundled(line)).toList)) 171 } 172 173 def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = 174 { 175 val Bundled = new Bundled(platform = Some(platform)) 176 val components = 177 for { 178 Bundled(name) <- Components.read_components(dir) 179 if !name.startsWith("jedit_build") 180 } yield name 181 val jdk_component = 182 components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") 183 (components, jdk_component) 184 } 185 186 def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) 187 { 188 def contrib_name(name: String): String = 189 Components.contrib(name = name).implode 190 191 val Bundled = new Bundled(platform = Some(platform)) 192 Components.write_components(dir, 193 Components.read_components(dir).flatMap(line => 194 line match { 195 case Bundled(name) => 196 if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) 197 else None 198 case _ => if (Bundled.detect(line)) None else Some(line) 199 }) ::: more_names.map(contrib_name(_))) 200 } 201 202 def make_contrib(dir: Path) 203 { 204 Isabelle_System.mkdirs(Components.contrib(dir)) 205 File.write(Components.contrib(dir, "README"), 206"""This directory contains add-on components that contribute to the main 207Isabelle distribution. Separate licensing conditions apply, see each 208directory individually. 209""") 210 } 211 212 213 214 /** build release **/ 215 216 private def execute(dir: Path, script: String): Unit = 217 Isabelle_System.bash(script, cwd = dir.file).check 218 219 private def execute_tar(dir: Path, args: String): Unit = 220 Isabelle_System.gnutar(args, dir = dir).check 221 222 223 /* build heaps on remote server */ 224 225 private def remote_build_heaps( 226 options: Options, 227 platform: Platform.Family.Value, 228 build_sessions: List[String], 229 local_dir: Path) 230 { 231 val server_option = "build_release_server_" + platform.toString 232 options.string(server_option) match { 233 case SSH.Target(user, host) => 234 using(SSH.open_session(options, host = host, user = user))(ssh => 235 { 236 Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar => 237 { 238 execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") 239 ssh.with_tmp_dir(remote_dir => 240 { 241 val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") 242 ssh.write_file(remote_tmp_tar, local_tmp_tar) 243 val remote_commands = 244 List( 245 "cd " + File.bash_path(remote_dir), 246 "tar -xf tmp.tar", 247 "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), 248 "tar -cf tmp.tar heaps") 249 ssh.execute(remote_commands.mkString(" && ")).check 250 ssh.read_file(remote_tmp_tar, local_tmp_tar) 251 }) 252 execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) 253 }) 254 }) 255 case s => error("Bad " + server_option + ": " + quote(s)) 256 } 257 } 258 259 260 /* main */ 261 262 private val default_platform_families: List[Platform.Family.Value] = 263 List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) 264 265 def build_release(base_dir: Path, 266 options: Options, 267 components_base: Path = Components.default_components_base, 268 progress: Progress = No_Progress, 269 rev: String = "", 270 afp_rev: String = "", 271 official_release: Boolean = false, 272 proper_release_name: Option[String] = None, 273 platform_families: List[Platform.Family.Value] = default_platform_families, 274 more_components: List[Path] = Nil, 275 website: Option[Path] = None, 276 build_sessions: List[String] = Nil, 277 build_library: Boolean = false, 278 parallel_jobs: Int = 1): Release = 279 { 280 val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) 281 282 val release = 283 { 284 val date = Date.now() 285 val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) 286 val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute 287 288 val version = proper_string(rev) orElse proper_release_name getOrElse "tip" 289 val ident = 290 try { hg.id(version) } 291 catch { case ERROR(_) => error("Bad repository version: " + version) } 292 293 val dist_version = 294 proper_release_name match { 295 case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) 296 case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) 297 } 298 299 new Release(progress, date, dist_name, dist_dir, dist_version, ident) 300 } 301 302 303 /* make distribution */ 304 305 if (release.isabelle_archive.is_file) { 306 progress.echo_warning("Release archive already exists: " + release.isabelle_archive) 307 308 val archive_ident = 309 Isabelle_System.with_tmp_dir("build_release")(tmp_dir => 310 { 311 val getsettings = Path.explode(release.dist_name + "/" + getsettings_file) 312 execute_tar(tmp_dir, "-xzf " + 313 File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) 314 split_lines(File.read(tmp_dir + getsettings)) 315 .collectFirst({ case ISABELLE_ID(ident) => ident }) 316 .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive)) 317 }) 318 319 if (release.ident != archive_ident) { 320 error("Mismatch of release identification " + release.ident + 321 " vs. archive " + archive_ident) 322 } 323 } 324 else { 325 progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...") 326 327 Isabelle_System.mkdirs(release.dist_dir) 328 329 if (release.isabelle_dir.is_dir) 330 error("Directory " + release.isabelle_dir + " already exists") 331 332 333 progress.echo_warning("Retrieving Mercurial repository version " + release.ident) 334 335 hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") 336 337 for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { 338 (release.isabelle_dir + Path.explode(name)).file.delete 339 } 340 341 342 progress.echo_warning("Preparing distribution " + quote(release.dist_name)) 343 344 patch_release(release, proper_release_name.isDefined && official_release) 345 346 if (proper_release_name.isEmpty) make_announce(release) 347 348 make_contrib(release.isabelle_dir) 349 350 execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") 351 352 record_bundled_components(release.isabelle_dir) 353 354 355 /* build tools and documentation */ 356 357 val other_isabelle = release.other_isabelle(release.dist_dir) 358 359 other_isabelle.init_settings( 360 other_isabelle.init_components(components_base = components_base, catalogs = List("main"))) 361 other_isabelle.resolve_components(echo = true) 362 363 try { 364 val export_classpath = 365 "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" 366 other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check 367 other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check 368 } 369 catch { case ERROR(_) => error("Failed to build tools") } 370 371 try { 372 other_isabelle.bash( 373 "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check 374 } 375 catch { case ERROR(_) => error("Failed to build documentation") } 376 377 make_news(other_isabelle, release.dist_version) 378 379 for (name <- List("Admin", "browser_info", "heaps")) { 380 Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) 381 } 382 383 other_isabelle.cleanup() 384 385 386 progress.echo_warning("Creating distribution archive " + release.isabelle_archive) 387 388 def execute_dist_name(script: String): Unit = 389 Isabelle_System.bash(script, cwd = release.dist_dir.file, 390 env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check 391 392 execute_dist_name(""" 393set -e 394 395chmod -R a+r "$DIST_NAME" 396chmod -R u+w "$DIST_NAME" 397chmod -R g=o "$DIST_NAME" 398find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w 399""") 400 401 execute_tar(release.dist_dir, "-czf " + 402 File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) 403 404 execute_dist_name(""" 405set -e 406 407mv "$DIST_NAME" "${DIST_NAME}-old" 408mkdir "$DIST_NAME" 409 410mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ 411 "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" 412mkdir "$DIST_NAME/doc" 413mv "${DIST_NAME}-old/doc/"*.pdf \ 414 "${DIST_NAME}-old/doc/"*.html \ 415 "${DIST_NAME}-old/doc/"*.css \ 416 "${DIST_NAME}-old/doc/fonts" \ 417 "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" 418 419rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle 420 421rm -rf "${DIST_NAME}-old" 422""") 423 } 424 425 426 /* make application bundles */ 427 428 val bundle_infos = platform_families.map(release.bundle_info) 429 430 for (bundle_info <- bundle_infos) { 431 val bundle_archive = release.dist_dir + bundle_info.path 432 val isabelle_name = release.dist_name 433 val platform = bundle_info.platform 434 435 progress.echo("\nApplication bundle for " + platform) 436 437 Isabelle_System.with_tmp_dir("build_release")(tmp_dir => 438 { 439 // release archive 440 441 execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive)) 442 val other_isabelle = release.other_isabelle(tmp_dir) 443 val isabelle_target = other_isabelle.isabelle_home 444 445 446 // bundled components 447 448 progress.echo("Bundled components:") 449 450 val contrib_dir = Components.contrib(isabelle_target) 451 452 val (bundled_components, jdk_component) = 453 get_bundled_components(isabelle_target, platform) 454 455 Components.resolve(components_base, bundled_components, 456 target_dir = Some(contrib_dir), 457 copy_dir = Some(release.dist_dir + Path.explode("contrib")), 458 progress = progress) 459 460 val more_components_names = 461 more_components.map(Components.unpack(contrib_dir, _, progress = progress)) 462 463 Components.purge(contrib_dir, platform) 464 465 activate_components(isabelle_target, platform, more_components_names) 466 467 468 // Java parameters 469 470 val java_options_title = "# Java runtime options" 471 val java_options: List[String] = 472 (for { 473 variable <- 474 List( 475 "ISABELLE_JAVA_SYSTEM_OPTIONS", 476 "JEDIT_JAVA_SYSTEM_OPTIONS", 477 "JEDIT_JAVA_OPTIONS") 478 opt <- Word.explode(other_isabelle.getenv(variable)) 479 } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name) 480 481 val classpath: List[Path] = 482 { 483 val base = isabelle_target.absolute 484 Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path => 485 { 486 val abs_path = path.absolute 487 File.relative_path(base, abs_path) match { 488 case Some(rel_path) => rel_path 489 case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path) 490 } 491 }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) 492 } 493 494 val jedit_options = Path.explode("src/Tools/jEdit/etc/options") 495 val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") 496 497 498 // build heaps 499 500 if (build_sessions.nonEmpty) { 501 progress.echo("Building heaps ...") 502 remote_build_heaps(options, platform, build_sessions, isabelle_target) 503 } 504 505 506 // application bundling 507 508 platform match { 509 case Platform.Family.linux => 510 File.write(isabelle_target + jedit_options, 511 File.read(isabelle_target + jedit_options) 512 .replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) 513 514 File.write(isabelle_target + jedit_props, 515 File.read(isabelle_target + jedit_props) 516 .replaceAll("console.fontsize=.*", "console.fontsize=18") 517 .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") 518 .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") 519 .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") 520 .replaceAll("view.fontsize=.*", "view.fontsize=24") 521 .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) 522 523 File.write(isabelle_target + Path.explode("Isabelle.options"), 524 terminate_lines(java_options_title :: java_options)) 525 526 val isabelle_app = isabelle_target + Path.explode("lib/scripts/Isabelle_app") 527 File.write(isabelle_app, 528 File.read(Path.explode("~~/Admin/Linux/Isabelle_app")) 529 .replaceAllLiterally("{CLASSPATH}", 530 classpath.map("$ISABELLE_HOME/" + _).mkString(":")) 531 .replaceAllLiterally("/jdk/", "/" + jdk_component + "/")) 532 File.set_executable(isabelle_app, true) 533 534 val linux_app = isabelle_target + Path.explode("contrib/linux_app") 535 File.move(linux_app + Path.explode("Isabelle"), 536 isabelle_target + Path.explode(isabelle_name)) 537 Isabelle_System.rm_tree(linux_app) 538 539 val archive_name = isabelle_name + "_linux.tar.gz" 540 progress.echo("Packaging " + archive_name + " ...") 541 execute_tar(tmp_dir, 542 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + 543 Bash.string(isabelle_name)) 544 545 546 case Platform.Family.macos => 547 File.write(isabelle_target + jedit_props, 548 File.read(isabelle_target + jedit_props) 549 .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") 550 .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") 551 .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d") 552 .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar=")) 553 554 555 // MacOS application bundle 556 557 File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) 558 559 val isabelle_app = Path.explode(isabelle_name + ".app") 560 val app_dir = tmp_dir + isabelle_app 561 File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir) 562 563 val app_contents = app_dir + Path.explode("Contents") 564 val app_resources = app_contents + Path.explode("Resources") 565 File.move(tmp_dir + Path.explode(isabelle_name), app_resources) 566 567 File.write(app_contents + Path.explode("Info.plist"), 568 File.read(Path.explode("~~/Admin/MacOS/Info.plist")) 569 .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) 570 .replaceAllLiterally("{JAVA_OPTIONS}", 571 terminate_lines(java_options.map(opt => "<string>" + opt + "</string>")))) 572 573 for (cp <- classpath) { 574 File.link( 575 Path.explode("../Resources/" + isabelle_name + "/") + cp, 576 app_contents + Path.explode("Java"), 577 force = true) 578 } 579 580 File.link( 581 Path.explode("../Resources/" + isabelle_name + "/contrib/" + 582 jdk_component + "/x86_64-darwin"), 583 app_contents + Path.explode("PlugIns/bundled.jdk"), 584 force = true) 585 586 File.link( 587 Path.explode("../../Info.plist"), 588 app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"), 589 force = true) 590 591 File.link( 592 Path.explode("Contents/Resources/" + isabelle_name), 593 app_dir + Path.explode("Isabelle"), 594 force = true) 595 596 597 // application archive 598 599 val archive_name = isabelle_name + "_macos.tar.gz" 600 progress.echo("Packaging " + archive_name + " ...") 601 execute_tar(tmp_dir, 602 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + 603 File.bash_path(isabelle_app)) 604 605 606 case Platform.Family.windows => 607 File.write(isabelle_target + jedit_props, 608 File.read(isabelle_target + jedit_props) 609 .replaceAll("lookAndFeel=.*", 610 "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel") 611 .replaceAll("foldPainter=.*", "foldPainter=Square")) 612 613 614 // application launcher 615 616 File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) 617 618 val app_template = Path.explode("~~/Admin/Windows/launch4j") 619 620 File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), 621 (java_options_title :: java_options).map(_ + "\r\n").mkString) 622 623 val isabelle_xml = Path.explode("isabelle.xml") 624 val isabelle_exe = Path.explode(isabelle_name + ".exe") 625 626 File.write(tmp_dir + isabelle_xml, 627 File.read(app_template + isabelle_xml) 628 .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) 629 .replaceAllLiterally("{OUTFILE}", 630 File.platform_path(isabelle_target + isabelle_exe)) 631 .replaceAllLiterally("{ICON}", 632 File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) 633 .replaceAllLiterally("{SPLASH}", 634 File.platform_path(app_template + Path.explode("isabelle.bmp"))) 635 .replaceAllLiterally("{CLASSPATH}", 636 cat_lines(classpath.map(cp => 637 " <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>"))) 638 .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\")) 639 640 execute(tmp_dir, 641 "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") 642 643 File.copy(app_template + Path.explode("manifest.xml"), 644 isabelle_target + isabelle_exe.ext("manifest")) 645 646 647 // Cygwin setup 648 649 val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") 650 651 File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) 652 653 val cygwin_mirror = 654 File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) 655 656 val cygwin_bat = Path.explode("Cygwin-Setup.bat") 657 File.write(isabelle_target + cygwin_bat, 658 File.read(cygwin_template + cygwin_bat) 659 .replaceAllLiterally("{MIRROR}", cygwin_mirror)) 660 File.set_executable(isabelle_target + cygwin_bat, true) 661 662 for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { 663 val path = Path.explode(name) 664 File.copy(cygwin_template + path, 665 isabelle_target + Path.explode("contrib/cygwin") + path) 666 } 667 668 execute(isabelle_target, 669 """find . -type f -not -name "*.exe" -not -name "*.dll" """ + 670 (if (Platform.is_macos) "-perm +100" else "-executable") + 671 " -print0 > contrib/cygwin/isabelle/executables") 672 673 execute(isabelle_target, 674 """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + 675 """> contrib/cygwin/isabelle/symlinks""") 676 677 execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) 678 679 File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") 680 681 682 // executable archive (self-extracting 7z) 683 684 val archive_name = isabelle_name + ".7z" 685 val exe_archive = tmp_dir + Path.explode(archive_name) 686 exe_archive.file.delete 687 688 progress.echo("Packaging " + archive_name + " ...") 689 execute(tmp_dir, 690 "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) 691 if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) 692 693 val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") 694 val sfx_txt = 695 File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")). 696 replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) 697 698 Bytes.write(release.dist_dir + isabelle_exe, 699 Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) 700 File.set_executable(release.dist_dir + isabelle_exe, true) 701 } 702 }) 703 progress.echo("DONE") 704 } 705 706 707 /* minimal website */ 708 709 for (dir <- website) { 710 val website_platform_bundles = 711 for { 712 bundle_info <- bundle_infos 713 if (release.dist_dir + bundle_info.path).is_file 714 } yield (bundle_info.name, bundle_info) 715 716 val isabelle_link = 717 HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident, 718 HTML.text("Isabelle/" + release.ident)) 719 val afp_link = 720 HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) 721 722 HTML.write_document(dir, "index.html", 723 List(HTML.title(release.dist_name)), 724 List( 725 HTML.section(release.dist_name + " (" + release.ident + ")"), 726 HTML.subsection("Platforms"), 727 HTML.itemize( 728 website_platform_bundles.map({ case (bundle, bundle_info) => 729 List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), 730 HTML.subsection("Repositories"), 731 HTML.itemize( 732 List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) 733 734 for ((bundle, _) <- website_platform_bundles) 735 File.copy(release.dist_dir + Path.explode(bundle), dir) 736 } 737 738 739 /* HTML library */ 740 741 if (build_library) { 742 if (release.isabelle_library_archive.is_file) { 743 progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive) 744 } 745 else { 746 Isabelle_System.with_tmp_dir("build_release")(tmp_dir => 747 { 748 val bundle = 749 release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz") 750 execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) 751 752 val other_isabelle = release.other_isabelle(tmp_dir) 753 754 Isabelle_System.mkdirs(other_isabelle.etc) 755 File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") 756 757 other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + 758 " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + 759 " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check 760 other_isabelle.isabelle_home_user.file.delete 761 762 execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) 763 execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) 764 execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) + 765 " " + Bash.string(release.dist_name + "/browser_info")) 766 }) 767 } 768 } 769 770 release 771 } 772 773 774 775 /** command line entry point **/ 776 777 def main(args: Array[String]) 778 { 779 Command_Line.tool0 { 780 var afp_rev = "" 781 var components_base: Path = Components.default_components_base 782 var official_release = false 783 var proper_release_name: Option[String] = None 784 var website: Option[Path] = None 785 var build_sessions: List[String] = Nil 786 var more_components: List[Path] = Nil 787 var parallel_jobs = 1 788 var build_library = false 789 var options = Options.init() 790 var platform_families = default_platform_families 791 var rev = "" 792 793 val getopts = Getopts(""" 794Usage: Admin/build_release [OPTIONS] BASE_DIR 795 796 Options are: 797 -A REV corresponding AFP changeset id 798 -C DIR base directory for Isabelle components (default: """ + 799 Components.default_components_base + """) 800 -O official release (not release-candidate) 801 -R RELEASE proper release with name 802 -W WEBSITE produce minimal website in given directory 803 -b SESSIONS build platform-specific session images (separated by commas) 804 -c ARCHIVE clean bundling with additional component .tar.gz archive 805 -j INT maximum number of parallel jobs (default 1) 806 -l build library 807 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 808 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) 809 -r REV Mercurial changeset id (default: RELEASE or tip) 810 811 Build Isabelle release in base directory, using the local repository clone. 812""", 813 "A:" -> (arg => afp_rev = arg), 814 "C:" -> (arg => components_base = Path.explode(arg)), 815 "O" -> (_ => official_release = true), 816 "R:" -> (arg => proper_release_name = Some(arg)), 817 "W:" -> (arg => website = Some(Path.explode(arg))), 818 "b:" -> (arg => build_sessions = space_explode(',', arg)), 819 "c:" -> (arg => 820 { 821 val path = Path.explode(arg) 822 Components.Archive.get_name(path.file_name) 823 more_components = more_components ::: List(path) 824 }), 825 "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), 826 "l" -> (_ => build_library = true), 827 "o:" -> (arg => options = options + arg), 828 "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), 829 "r:" -> (arg => rev = arg)) 830 831 val more_args = getopts(args) 832 val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } 833 834 val progress = new Console_Progress() 835 836 if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) 837 error("Building for windows requires 7z") 838 839 build_release(Path.explode(base_dir), options, components_base = components_base, 840 progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, 841 proper_release_name = proper_release_name, website = website, 842 platform_families = 843 if (platform_families.isEmpty) default_platform_families 844 else platform_families, 845 more_components = more_components, build_sessions = build_sessions, 846 build_library = build_library, parallel_jobs = parallel_jobs) 847 } 848 } 849} 850