12 /** release info **/ |
12 /** release info **/ |
13 |
13 |
14 sealed case class Bundle_Info( |
14 sealed case class Bundle_Info( |
15 platform: Platform.Family.Value, |
15 platform: Platform.Family.Value, |
16 platform_description: String, |
16 platform_description: String, |
17 main: String, |
17 name: String) |
18 fallback: Option[String]) |
18 { |
19 { |
19 def path: Path = Path.explode(name) |
20 def names: List[String] = main :: fallback.toList |
|
21 } |
20 } |
22 |
21 |
23 class Release private[Build_Release]( |
22 class Release private[Build_Release]( |
24 progress: Progress, |
23 progress: Progress, |
25 val date: Date, |
24 val date: Date, |
37 isabelle_identifier = dist_name + "-build", |
36 isabelle_identifier = dist_name + "-build", |
38 progress = progress) |
37 progress = progress) |
39 |
38 |
40 def bundle_info(platform: Platform.Family.Value): Bundle_Info = |
39 def bundle_info(platform: Platform.Family.Value): Bundle_Info = |
41 platform match { |
40 platform match { |
42 case Platform.Family.linux => |
41 case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") |
43 Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz", None) |
42 case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz") |
44 case Platform.Family.macos => |
43 case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") |
45 Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_macos.tar.gz")) |
|
46 case Platform.Family.windows => |
|
47 Bundle_Info(platform, "Windows", dist_name + ".exe", None) |
|
48 } |
44 } |
49 } |
45 } |
50 |
46 |
51 |
47 |
52 |
48 |
236 proper_release_name: Option[String] = None, |
232 proper_release_name: Option[String] = None, |
237 platform_families: List[Platform.Family.Value] = default_platform_families, |
233 platform_families: List[Platform.Family.Value] = default_platform_families, |
238 more_components: List[Path] = Nil, |
234 more_components: List[Path] = Nil, |
239 website: Option[Path] = None, |
235 website: Option[Path] = None, |
240 build_library: Boolean = false, |
236 build_library: Boolean = false, |
241 parallel_jobs: Int = 1, |
237 parallel_jobs: Int = 1): Release = |
242 remote_mac: String = ""): Release = |
|
243 { |
238 { |
244 val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) |
239 val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) |
245 |
240 |
246 val release = |
241 val release = |
247 { |
242 { |
390 /* make application bundles */ |
385 /* make application bundles */ |
391 |
386 |
392 val bundle_infos = platform_families.map(release.bundle_info) |
387 val bundle_infos = platform_families.map(release.bundle_info) |
393 |
388 |
394 for (bundle_info <- bundle_infos) { |
389 for (bundle_info <- bundle_infos) { |
395 val bundle = |
390 val bundle_archive = release.dist_dir + bundle_info.path |
396 (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main |
|
397 val bundle_archive = release.dist_dir + Path.explode(bundle) |
|
398 if (bundle_archive.is_file && more_components.isEmpty) |
391 if (bundle_archive.is_file && more_components.isEmpty) |
399 progress.echo_warning("Application bundle already exists: " + bundle_archive) |
392 progress.echo_warning("Application bundle already exists: " + bundle_archive) |
400 else { |
393 else { |
401 val isabelle_name = release.dist_name |
394 val isabelle_name = release.dist_name |
402 val platform = bundle_info.platform |
395 val platform = bundle_info.platform |
485 progress.echo("Packaging " + archive_name + " ...") |
478 progress.echo("Packaging " + archive_name + " ...") |
486 execute_tar(tmp_dir, |
479 execute_tar(tmp_dir, |
487 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + |
480 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + |
488 Bash.string(isabelle_name)) |
481 Bash.string(isabelle_name)) |
489 |
482 |
|
483 |
490 case Platform.Family.macos => |
484 case Platform.Family.macos => |
491 File.write(isabelle_target + jedit_props, |
485 File.write(isabelle_target + jedit_props, |
492 File.read(isabelle_target + jedit_props) |
486 File.read(isabelle_target + jedit_props) |
493 .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") |
487 .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") |
494 .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") |
488 .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") |
497 |
491 |
498 |
492 |
499 // MacOS application bundle |
493 // MacOS application bundle |
500 |
494 |
501 File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) |
495 File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) |
502 val dmg_dir = tmp_dir + Path.explode("macos_app/dmg") |
|
503 |
496 |
504 val isabelle_app = Path.explode(isabelle_name + ".app") |
497 val isabelle_app = Path.explode(isabelle_name + ".app") |
505 val app_dir = dmg_dir + isabelle_app |
498 val app_dir = tmp_dir + isabelle_app |
506 File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir) |
499 File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir) |
507 |
500 |
508 val app_contents = app_dir + Path.explode("Contents") |
501 val app_contents = app_dir + Path.explode("Contents") |
509 val app_resources = app_contents + Path.explode("Resources") |
502 val app_resources = app_contents + Path.explode("Resources") |
510 File.move(tmp_dir + Path.explode(isabelle_name), app_resources) |
503 File.move(tmp_dir + Path.explode(isabelle_name), app_resources) |
511 |
504 |
537 Path.explode("Contents/Resources/" + isabelle_name), |
530 Path.explode("Contents/Resources/" + isabelle_name), |
538 app_dir + Path.explode("Isabelle"), |
531 app_dir + Path.explode("Isabelle"), |
539 force = true) |
532 force = true) |
540 |
533 |
541 |
534 |
542 // application archive: dmg or .tar.gz |
535 // application archive |
543 |
536 |
544 val isabelle_dmg = Path.explode(isabelle_name + ".dmg") |
537 val archive_name = isabelle_name + "_macos.tar.gz" |
545 (release.dist_dir + isabelle_dmg).file.delete |
538 progress.echo("Packaging " + archive_name + " ...") |
546 |
539 execute_tar(tmp_dir, |
547 remote_mac match { |
540 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + |
548 case SSH.Target(user, host) => |
541 File.bash_path(isabelle_app)) |
549 progress.echo("Packaging " + isabelle_dmg + " (via host " + quote(host) + ") ...") |
542 |
550 using(SSH.open_session(options, host = host, user = user))(ssh => |
|
551 { |
|
552 val dmg_archive = Path.explode("dmg.tar") |
|
553 execute_tar(dmg_dir, "-cf " + File.bash_path(tmp_dir + dmg_archive) + " .") |
|
554 |
|
555 ssh.with_tmp_dir(remote_dir => |
|
556 { |
|
557 val cd = "cd " + ssh.bash_path(remote_dir) + "; " |
|
558 ssh.write_file(remote_dir + dmg_archive, tmp_dir + dmg_archive) |
|
559 ssh.execute( |
|
560 cd + "mkdir dmg && tar -C dmg -xf " + ssh.bash_path(dmg_archive)).check |
|
561 ssh.execute( |
|
562 cd + "hdiutil create -srcfolder dmg -volname Isabelle " + |
|
563 ssh.bash_path(isabelle_dmg)).check |
|
564 ssh.read_file(remote_dir + isabelle_dmg, release.dist_dir + isabelle_dmg) |
|
565 }) |
|
566 }) |
|
567 case _ => |
|
568 val archive_name = isabelle_name + "_macos.tar.gz" |
|
569 progress.echo("Packaging " + archive_name + " ...") |
|
570 execute_tar(dmg_dir, |
|
571 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + |
|
572 File.bash_path(isabelle_app)) |
|
573 } |
|
574 |
543 |
575 case Platform.Family.windows => |
544 case Platform.Family.windows => |
576 File.write(isabelle_target + jedit_props, |
545 File.write(isabelle_target + jedit_props, |
577 File.read(isabelle_target + jedit_props) |
546 File.read(isabelle_target + jedit_props) |
578 .replaceAll("lookAndFeel=.*", |
547 .replaceAll("lookAndFeel=.*", |
676 |
645 |
677 for (dir <- website) { |
646 for (dir <- website) { |
678 val website_platform_bundles = |
647 val website_platform_bundles = |
679 for { |
648 for { |
680 bundle_info <- bundle_infos |
649 bundle_info <- bundle_infos |
681 bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file) |
650 if (release.dist_dir + bundle_info.path).is_file |
682 } yield (bundle, bundle_info) |
651 } yield (bundle_info.name, bundle_info) |
683 |
652 |
684 val afp_link = |
653 val afp_link = |
685 HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) |
654 HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) |
686 |
655 |
687 HTML.write_document(dir, "index.html", |
656 HTML.write_document(dir, "index.html", |
739 def main(args: Array[String]) |
708 def main(args: Array[String]) |
740 { |
709 { |
741 Command_Line.tool0 { |
710 Command_Line.tool0 { |
742 var afp_rev = "" |
711 var afp_rev = "" |
743 var components_base: Option[Path] = None |
712 var components_base: Option[Path] = None |
744 var remote_mac = "" |
|
745 var official_release = false |
713 var official_release = false |
746 var proper_release_name: Option[String] = None |
714 var proper_release_name: Option[String] = None |
747 var website: Option[Path] = None |
715 var website: Option[Path] = None |
748 var more_components: List[Path] = Nil |
716 var more_components: List[Path] = Nil |
749 var parallel_jobs = 1 |
717 var parallel_jobs = 1 |
756 Usage: Admin/build_release [OPTIONS] BASE_DIR |
724 Usage: Admin/build_release [OPTIONS] BASE_DIR |
757 |
725 |
758 Options are: |
726 Options are: |
759 -A REV corresponding AFP changeset id |
727 -A REV corresponding AFP changeset id |
760 -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) |
728 -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) |
761 -M USER@HOST remote Mac OS X for dmg build |
|
762 -O official release (not release-candidate) |
729 -O official release (not release-candidate) |
763 -R RELEASE proper release with name |
730 -R RELEASE proper release with name |
764 -W WEBSITE produce minimal website in given directory |
731 -W WEBSITE produce minimal website in given directory |
765 -c ARCHIVE clean bundling with additional component .tar.gz archive |
732 -c ARCHIVE clean bundling with additional component .tar.gz archive |
766 -j INT maximum number of parallel jobs (default 1) |
733 -j INT maximum number of parallel jobs (default 1) |
771 |
738 |
772 Build Isabelle release in base directory, using the local repository clone. |
739 Build Isabelle release in base directory, using the local repository clone. |
773 """, |
740 """, |
774 "A:" -> (arg => afp_rev = arg), |
741 "A:" -> (arg => afp_rev = arg), |
775 "C:" -> (arg => components_base = Some(Path.explode(arg))), |
742 "C:" -> (arg => components_base = Some(Path.explode(arg))), |
776 "M:" -> (arg => remote_mac = arg), |
|
777 "O" -> (_ => official_release = true), |
743 "O" -> (_ => official_release = true), |
778 "R:" -> (arg => proper_release_name = Some(arg)), |
744 "R:" -> (arg => proper_release_name = Some(arg)), |
779 "W:" -> (arg => website = Some(Path.explode(arg))), |
745 "W:" -> (arg => website = Some(Path.explode(arg))), |
780 "c:" -> (arg => |
746 "c:" -> (arg => |
781 { |
747 { |
802 proper_release_name = proper_release_name, website = website, |
768 proper_release_name = proper_release_name, website = website, |
803 platform_families = |
769 platform_families = |
804 if (platform_families.isEmpty) default_platform_families |
770 if (platform_families.isEmpty) default_platform_families |
805 else platform_families, |
771 else platform_families, |
806 more_components = more_components, build_library = build_library, |
772 more_components = more_components, build_library = build_library, |
807 parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
773 parallel_jobs = parallel_jobs) |
808 } |
774 } |
809 } |
775 } |
810 } |
776 } |