35 { |
41 { |
36 override def toString: String = dist_name |
42 override def toString: String = dist_name |
37 |
43 |
38 val isabelle: Path = Path.explode(dist_name) |
44 val isabelle: Path = Path.explode(dist_name) |
39 val isabelle_dir: Path = dist_dir + isabelle |
45 val isabelle_dir: Path = dist_dir + isabelle |
40 val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") |
46 val isabelle_archive: Path = dist_dir + isabelle.tar.gz |
41 val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") |
47 val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") |
42 |
48 |
43 def other_isabelle(dir: Path): Other_Isabelle = |
49 def other_isabelle(dir: Path): Other_Isabelle = |
44 Other_Isabelle(dir + isabelle, |
50 Other_Isabelle(dir + isabelle, |
45 isabelle_identifier = dist_name + "-build", |
51 isabelle_identifier = dist_name + "-build", |
86 |
92 |
87 |
93 |
88 |
94 |
89 /** release archive **/ |
95 /** release archive **/ |
90 |
96 |
|
97 val ISABELLE: Path = Path.basic("Isabelle") |
91 val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID") |
98 val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID") |
92 val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS") |
99 val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS") |
93 val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER") |
100 val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER") |
94 |
101 |
95 object Release_Archive |
102 object Release_Archive |
96 { |
103 { |
97 def make(bytes: Bytes): Release_Archive = |
104 def make(bytes: Bytes, rename: String = ""): Release_Archive = |
98 { |
105 { |
99 Isabelle_System.with_tmp_dir("tmp")(dir => |
106 Isabelle_System.with_tmp_dir("tmp")(dir => |
100 Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => |
107 Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => |
101 { |
108 { |
|
109 val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE) |
|
110 |
102 Bytes.write(archive_path, bytes) |
111 Bytes.write(archive_path, bytes) |
103 Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), |
112 execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1) |
104 dir = dir, original_owner = true, strip = 1).check |
113 |
105 |
114 val id = File.read(isabelle_dir + ISABELLE_ID) |
106 val id = File.read(dir + ISABELLE_ID) |
115 val tags = File.read(isabelle_dir + ISABELLE_TAGS) |
107 val tags = File.read(dir + ISABELLE_TAGS) |
116 val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER) |
108 val identifier = File.read(dir + ISABELLE_IDENTIFIER) |
117 |
109 new Release_Archive(bytes, id, tags, identifier) |
118 val (bytes1, identifier1) = |
|
119 if (rename.isEmpty || rename == identifier) (bytes, identifier) |
|
120 else { |
|
121 File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename) |
|
122 Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename)) |
|
123 execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename)) |
|
124 (Bytes.read(archive_path), rename) |
|
125 } |
|
126 new Release_Archive(bytes1, id, tags, identifier1) |
110 }) |
127 }) |
111 ) |
128 ) |
112 } |
129 } |
113 |
130 |
114 def read(path: Path): Release_Archive = make(Bytes.read(path)) |
131 def read(path: Path, rename: String = ""): Release_Archive = |
|
132 make(Bytes.read(path), rename = rename) |
|
133 |
|
134 def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive = |
|
135 { |
|
136 val bytes = |
|
137 if (Path.is_wellformed(url)) Bytes.read(Path.explode(url)) |
|
138 else Isabelle_System.download(url, progress = progress).bytes |
|
139 make(bytes, rename = rename) |
|
140 } |
115 } |
141 } |
116 |
142 |
117 case class Release_Archive private[Build_Release]( |
143 case class Release_Archive private[Build_Release]( |
118 bytes: Bytes, id: String, tags: String, identifier: String) |
144 bytes: Bytes, id: String, tags: String, identifier: String) |
119 { |
145 { |
365 /* main */ |
384 /* main */ |
366 |
385 |
367 private val default_platform_families: List[Platform.Family.Value] = |
386 private val default_platform_families: List[Platform.Family.Value] = |
368 List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) |
387 List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) |
369 |
388 |
|
389 def use_release_archive( |
|
390 context: Release_Context, |
|
391 archive: Release_Archive, |
|
392 id: String = ""): Unit = |
|
393 { |
|
394 if (id.nonEmpty && id != archive.id) { |
|
395 error("Mismatch of release identification " + id + " vs. archive " + archive.id) |
|
396 } |
|
397 |
|
398 if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) { |
|
399 Bytes.write(context.isabelle_archive, archive.bytes) |
|
400 } |
|
401 } |
|
402 |
370 def build_release_archive( |
403 def build_release_archive( |
371 context: Release_Context, |
404 context: Release_Context, |
372 version: String, |
405 version: String, |
373 parallel_jobs: Int = 1): Release_Archive = |
406 parallel_jobs: Int = 1): Unit = |
374 { |
407 { |
375 val progress = context.progress |
408 val progress = context.progress |
376 |
409 |
377 val hg = Mercurial.repository(Path.ISABELLE_HOME) |
410 val hg = Mercurial.repository(Path.ISABELLE_HOME) |
378 val id = |
411 val id = |
379 try { hg.id(version) } |
412 try { hg.id(version) } |
380 catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } |
413 catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } |
381 |
414 |
382 if (context.isabelle_archive.is_file) { |
415 if (context.isabelle_archive.is_file) { |
383 progress.echo_warning("Found existing release archive: " + context.isabelle_archive) |
416 progress.echo_warning("Found existing release archive: " + context.isabelle_archive) |
384 |
417 use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id) |
385 val archive = Release_Archive.read(context.isabelle_archive) |
|
386 if (id == archive.id) archive |
|
387 else error("Mismatch of release identification " + id + " vs. archive " + archive.id) |
|
388 } |
418 } |
389 else { |
419 else { |
390 progress.echo_warning("Preparing release " + context.dist_name + " ...") |
420 progress.echo_warning("Preparing release " + context.dist_name + " ...") |
391 |
421 |
392 Isabelle_System.new_directory(context.dist_dir) |
422 Isabelle_System.new_directory(context.dist_dir) |
447 execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""") |
477 execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""") |
448 execute(context.dist_dir, |
478 execute(context.dist_dir, |
449 """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""") |
479 """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""") |
450 execute_tar(context.dist_dir, "-czf " + |
480 execute_tar(context.dist_dir, "-czf " + |
451 File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name)) |
481 File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name)) |
452 |
|
453 Release_Archive.read(context.isabelle_archive) |
|
454 } |
482 } |
455 } |
483 } |
456 |
484 |
457 def build_release( |
485 def build_release( |
458 options: Options, |
486 options: Options, |
459 context: Release_Context, |
487 context: Release_Context, |
460 release_archive: Release_Archive, |
|
461 afp_rev: String = "", |
488 afp_rev: String = "", |
462 platform_families: List[Platform.Family.Value] = default_platform_families, |
489 platform_families: List[Platform.Family.Value] = default_platform_families, |
463 more_components: List[Path] = Nil, |
490 more_components: List[Path] = Nil, |
464 website: Option[Path] = None, |
491 website: Option[Path] = None, |
465 build_sessions: List[String] = Nil, |
492 build_sessions: List[String] = Nil, |
469 val progress = context.progress |
496 val progress = context.progress |
470 |
497 |
471 |
498 |
472 /* release directory */ |
499 /* release directory */ |
473 |
500 |
474 for (name <- List(context.dist_name, "Isabelle")) { |
501 val archive = Release_Archive.read(context.isabelle_archive) |
475 Isabelle_System.rm_tree(context.dist_dir + Path.explode(name)) |
502 |
|
503 for (path <- List(context.isabelle, ISABELLE)) { |
|
504 Isabelle_System.rm_tree(context.dist_dir + path) |
476 } |
505 } |
477 |
506 |
478 Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => |
507 Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => |
479 { |
508 { |
480 Bytes.write(archive_path, release_archive.bytes) |
509 Bytes.write(archive_path, archive.bytes) |
481 val extract = |
510 val extract = |
482 List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc"). |
511 List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc"). |
483 map(name => context.dist_name + "/" + name) |
512 map(name => context.release_name + "/" + name) |
484 execute_tar(context.dist_dir, |
513 execute_tar(context.dist_dir, |
485 "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract)) |
514 "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract)) |
486 }) |
515 }) |
487 |
516 |
488 Isabelle_System.symlink( |
517 Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE) |
489 Path.explode(context.dist_name), context.dist_dir + Path.explode("Isabelle")) |
|
490 |
518 |
491 |
519 |
492 /* make application bundles */ |
520 /* make application bundles */ |
493 |
521 |
494 val bundle_infos = platform_families.map(context.bundle_info) |
522 val bundle_infos = platform_families.map(context.bundle_info) |
612 Isabelle_System.copy_file(isabelle_target + Path.explode(icon), |
640 Isabelle_System.copy_file(isabelle_target + Path.explode(icon), |
613 Isabelle_System.make_directory(app_contents + Path.explode("Resources"))) |
641 Isabelle_System.make_directory(app_contents + Path.explode("Resources"))) |
614 } |
642 } |
615 |
643 |
616 make_isabelle_plist( |
644 make_isabelle_plist( |
617 app_contents + Path.explode("Info.plist"), isabelle_name, release_archive.id) |
645 app_contents + Path.explode("Info.plist"), isabelle_name, archive.id) |
618 |
646 |
619 make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, |
647 make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, |
620 classpath, dock_icon = true) |
648 classpath, dock_icon = true) |
621 |
649 |
622 val isabelle_options = Path.explode("Isabelle.options") |
650 val isabelle_options = Path.explode("Isabelle.options") |
745 bundle_info <- bundle_infos |
773 bundle_info <- bundle_infos |
746 if (context.dist_dir + bundle_info.path).is_file |
774 if (context.dist_dir + bundle_info.path).is_file |
747 } yield (bundle_info.name, bundle_info) |
775 } yield (bundle_info.name, bundle_info) |
748 |
776 |
749 val isabelle_link = |
777 val isabelle_link = |
750 HTML.link(Isabelle_System.isabelle_repository.changeset(release_archive.id), |
778 HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id), |
751 HTML.text("Isabelle/" + release_archive.id)) |
779 HTML.text("Isabelle/" + archive.id)) |
752 val afp_link = |
780 val afp_link = |
753 HTML.link(Isabelle_System.afp_repository.changeset(afp_rev), |
781 HTML.link(Isabelle_System.afp_repository.changeset(afp_rev), |
754 HTML.text("AFP/" + afp_rev)) |
782 HTML.text("AFP/" + afp_rev)) |
755 |
783 |
756 HTML.write_document(dir, "index.html", |
784 HTML.write_document(dir, "index.html", |
815 Command_Line.tool { |
843 Command_Line.tool { |
816 var afp_rev = "" |
844 var afp_rev = "" |
817 var components_base: Path = Components.default_components_base |
845 var components_base: Path = Components.default_components_base |
818 var target_dir = Path.current |
846 var target_dir = Path.current |
819 var release_name = "" |
847 var release_name = "" |
|
848 var source_archive = "" |
820 var website: Option[Path] = None |
849 var website: Option[Path] = None |
821 var build_sessions: List[String] = Nil |
850 var build_sessions: List[String] = Nil |
822 var more_components: List[Path] = Nil |
851 var more_components: List[Path] = Nil |
823 var parallel_jobs = 1 |
852 var parallel_jobs = 1 |
824 var build_library = false |
853 var build_library = false |
833 -A REV corresponding AFP changeset id |
862 -A REV corresponding AFP changeset id |
834 -C DIR base directory for Isabelle components (default: """ + |
863 -C DIR base directory for Isabelle components (default: """ + |
835 Components.default_components_base + """) |
864 Components.default_components_base + """) |
836 -D DIR target directory (default ".") |
865 -D DIR target directory (default ".") |
837 -R RELEASE explicit release name |
866 -R RELEASE explicit release name |
|
867 -S ARCHIVE use existing source archive (file or URL) |
838 -W WEBSITE produce minimal website in given directory |
868 -W WEBSITE produce minimal website in given directory |
839 -b SESSIONS build platform-specific session images (separated by commas) |
869 -b SESSIONS build platform-specific session images (separated by commas) |
840 -c ARCHIVE clean bundling with additional component .tar.gz archive |
870 -c ARCHIVE clean bundling with additional component .tar.gz archive |
841 -j INT maximum number of parallel jobs (default 1) |
871 -j INT maximum number of parallel jobs (default 1) |
842 -l build library |
872 -l build library |
843 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
873 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
844 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
874 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
845 -r REV Mercurial changeset id (default: RELEASE or tip) |
875 -r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip) |
846 |
876 |
847 Build Isabelle release in base directory, using the local repository clone. |
877 Build Isabelle release in base directory, using the local repository clone. |
848 """, |
878 """, |
849 "A:" -> (arg => afp_rev = arg), |
879 "A:" -> (arg => afp_rev = arg), |
850 "C:" -> (arg => components_base = Path.explode(arg)), |
880 "C:" -> (arg => components_base = Path.explode(arg)), |
851 "D:" -> (arg => target_dir = Path.explode(arg)), |
881 "D:" -> (arg => target_dir = Path.explode(arg)), |
852 "R:" -> (arg => release_name = arg), |
882 "R:" -> (arg => release_name = arg), |
|
883 "S:" -> (arg => source_archive = arg), |
853 "W:" -> (arg => website = Some(Path.explode(arg))), |
884 "W:" -> (arg => website = Some(Path.explode(arg))), |
854 "b:" -> (arg => build_sessions = space_explode(',', arg)), |
885 "b:" -> (arg => build_sessions = space_explode(',', arg)), |
855 "c:" -> (arg => |
886 "c:" -> (arg => |
856 { |
887 { |
857 val path = Path.explode(arg) |
888 val path = Path.explode(arg) |
865 "r:" -> (arg => rev = arg)) |
896 "r:" -> (arg => rev = arg)) |
866 |
897 |
867 val more_args = getopts(args) |
898 val more_args = getopts(args) |
868 if (more_args.nonEmpty) getopts.usage() |
899 if (more_args.nonEmpty) getopts.usage() |
869 |
900 |
870 val context = |
901 if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) |
|
902 error("Building for windows requires 7z") |
|
903 |
|
904 def make_context(name: String): Release_Context = |
871 Release_Context(target_dir, |
905 Release_Context(target_dir, |
872 release_name = release_name, |
906 release_name = name, |
873 components_base = components_base, |
907 components_base = components_base, |
874 progress = new Console_Progress()) |
908 progress = new Console_Progress()) |
875 |
909 |
876 if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) |
910 val context = |
877 error("Building for windows requires 7z") |
911 if (source_archive.isEmpty) { |
878 |
912 val context = make_context(release_name) |
879 val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" |
913 val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" |
880 val release_archive = build_release_archive(context, version, parallel_jobs = parallel_jobs) |
914 build_release_archive(context, version, parallel_jobs = parallel_jobs) |
881 |
915 context |
882 build_release(options, context, release_archive, afp_rev = afp_rev, |
916 } |
|
917 else { |
|
918 val archive = Release_Archive.get(source_archive, rename = release_name) |
|
919 val context = make_context(proper_string(release_name) getOrElse archive.identifier) |
|
920 Isabelle_System.new_directory(context.dist_dir) |
|
921 use_release_archive(context, archive, id = rev) |
|
922 context |
|
923 } |
|
924 |
|
925 build_release(options, context, afp_rev = afp_rev, |
883 platform_families = |
926 platform_families = |
884 if (platform_families.isEmpty) default_platform_families |
927 if (platform_families.isEmpty) default_platform_families |
885 else platform_families, |
928 else platform_families, |
886 more_components = more_components, build_sessions = build_sessions, |
929 more_components = more_components, build_sessions = build_sessions, |
887 build_library = build_library, parallel_jobs = parallel_jobs, website = website) |
930 build_library = build_library, parallel_jobs = parallel_jobs, website = website) |