# HG changeset patch
# User wenzelm
# Date 1554905892 -7200
# Node ID 77f978dd8ffb00f66e702b3bd37eabfd8eccc27e
# Parent 4005298550a69e1af773eb4da784ede61b3e7037# Parent 491453ea09bb2b3027fe4780e236ee5340af7150
merged;
diff -r 4005298550a6 -r 77f978dd8ffb ANNOUNCE
--- a/ANNOUNCE Wed Apr 10 13:34:55 2019 +0100
+++ b/ANNOUNCE Wed Apr 10 16:18:12 2019 +0200
@@ -18,7 +18,8 @@
* HOL: various syntax and library improvements.
-* HOL-Analysis: more material and better organization.
+* HOL libraries: better organization and much more material in HOL-Algebra,
+HOL-Analysis, HOL-Homology.
* Isabelle/ML environments for separate SML applications.
diff -r 4005298550a6 -r 77f978dd8ffb Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST Wed Apr 10 13:34:55 2019 +0100
+++ b/Admin/Release/CHECKLIST Wed Apr 10 16:18:12 2019 +0200
@@ -73,11 +73,11 @@
- fully-automated packaging (e.g. on lxcisa0):
- hg up -r DISTNAME && Admin/build_release -O -l -R DISTNAME -C ~/tmp/isadist/contrib /home/isabelle/dist
+ hg up -r DISTNAME && Admin/build_release -b HOL -l -O -R DISTNAME /home/isabelle/dist
- Docker image:
- isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2018 Isabelle2018_app.tar.gz
+ isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2019 Isabelle2019_linux.tar.gz
https://hub.docker.com/r/makarius/isabelle
https://docs.docker.com/docker-cloud/builds/push-images
diff -r 4005298550a6 -r 77f978dd8ffb Admin/etc/options
--- a/Admin/etc/options Wed Apr 10 13:34:55 2019 +0100
+++ b/Admin/etc/options Wed Apr 10 16:18:12 2019 +0200
@@ -10,3 +10,13 @@
option isabelle_components_contrib_dir : string = "/home/isabelle/contrib"
-- "unpacked components for remote build services"
+
+
+option build_release_server_linux : string = ""
+ -- "SSH user@host for remote build of heaps"
+
+option build_release_server_macos : string = ""
+ -- "SSH user@host for remote build of heaps"
+
+option build_release_server_windows : string = ""
+ -- "SSH user@host for remote build of heaps"
diff -r 4005298550a6 -r 77f978dd8ffb NEWS
--- a/NEWS Wed Apr 10 13:34:55 2019 +0100
+++ b/NEWS Wed Apr 10 16:18:12 2019 +0200
@@ -90,6 +90,16 @@
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".
+* The Isabelle/jEdit desktop application uses the same options as
+"isabelle jedit" for its internal "isabelle build" process: the implicit
+option "-o system_heaps" (or "-s") has been discontinued. This reduces
+the potential for surprise wrt. command-line tools.
+
+* The official download of the Isabelle/jEdit application already
+contains heap images for Isabelle/HOL within its main directory: thus
+the first encounter becomes faster and more robust (e.g. when run from a
+read-only directory).
+
* Isabelle DejaVu fonts are available with hinting by default, which is
relevant for low-resolution displays. This may be disabled via system
option "isabelle_fonts_hinted = false" in
diff -r 4005298550a6 -r 77f978dd8ffb src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala Wed Apr 10 13:34:55 2019 +0100
+++ b/src/Pure/Admin/afp.scala Wed Apr 10 16:18:12 2019 +0200
@@ -41,7 +41,7 @@
def get(prop: String): Option[String] = Properties.get(metadata, prop)
def get_string(prop: String): String = get(prop).getOrElse("")
def get_strings(prop: String): List[String] =
- Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
+ space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
def title: String = get_string("title")
def authors: List[String] = get_strings("author")
diff -r 4005298550a6 -r 77f978dd8ffb src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala Wed Apr 10 13:34:55 2019 +0100
+++ b/src/Pure/Admin/build_release.scala Wed Apr 10 16:18:12 2019 +0200
@@ -211,7 +211,7 @@
- /** build_release **/
+ /** build release **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
@@ -219,6 +219,46 @@
private def execute_tar(dir: Path, args: String): Unit =
Isabelle_System.gnutar(args, dir = dir).check
+
+ /* build heaps on remote server */
+
+ private def remote_build_heaps(
+ options: Options,
+ platform: Platform.Family.Value,
+ build_sessions: List[String],
+ local_dir: Path)
+ {
+ val server_option = "build_release_server_" + platform.toString
+ options.string(server_option) match {
+ case SSH.Target(user, host) =>
+ using(SSH.open_session(options, host = host, user = user))(ssh =>
+ {
+ Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
+ {
+ execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
+ ssh.with_tmp_dir(remote_dir =>
+ {
+ val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
+ ssh.write_file(remote_tmp_tar, local_tmp_tar)
+ val remote_commands =
+ List(
+ "cd " + File.bash_path(remote_dir),
+ "tar -xf tmp.tar",
+ "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
+ "tar -cf tmp.tar heaps")
+ ssh.execute(remote_commands.mkString(" && ")).check
+ ssh.read_file(remote_tmp_tar, local_tmp_tar)
+ })
+ execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
+ })
+ })
+ case s => error("Bad " + server_option + ": " + quote(s))
+ }
+ }
+
+
+ /* main */
+
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
@@ -233,6 +273,7 @@
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
+ build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Release =
{
@@ -388,258 +429,264 @@
for (bundle_info <- bundle_infos) {
val bundle_archive = release.dist_dir + bundle_info.path
- if (bundle_archive.is_file && more_components.isEmpty)
- progress.echo_warning("Application bundle already exists: " + bundle_archive)
- else {
- val isabelle_name = release.dist_name
- val platform = bundle_info.platform
+ val isabelle_name = release.dist_name
+ val platform = bundle_info.platform
- progress.echo("\nApplication bundle for " + platform)
+ progress.echo("\nApplication bundle for " + platform)
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
- {
- // release archive
+ Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
+ {
+ // release archive
- execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
- val other_isabelle = release.other_isabelle(tmp_dir)
- val isabelle_target = other_isabelle.isabelle_home
+ execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
+ val other_isabelle = release.other_isabelle(tmp_dir)
+ val isabelle_target = other_isabelle.isabelle_home
- // bundled components
+ // bundled components
- progress.echo("Bundled components:")
+ progress.echo("Bundled components:")
- val contrib_dir = Components.contrib(isabelle_target)
+ val contrib_dir = Components.contrib(isabelle_target)
- val (bundled_components, jdk_component) =
- get_bundled_components(isabelle_target, platform)
+ val (bundled_components, jdk_component) =
+ get_bundled_components(isabelle_target, platform)
- Components.resolve(components_base, bundled_components,
- target_dir = Some(contrib_dir), progress = progress)
+ Components.resolve(components_base, bundled_components,
+ target_dir = Some(contrib_dir),
+ copy_dir = Some(release.dist_dir + Path.explode("contrib")),
+ progress = progress)
- val more_components_names =
- more_components.map(Components.unpack(contrib_dir, _, progress = progress))
+ val more_components_names =
+ more_components.map(Components.unpack(contrib_dir, _, progress = progress))
- Components.purge(contrib_dir, platform)
+ Components.purge(contrib_dir, platform)
- activate_components(isabelle_target, platform, more_components_names)
+ activate_components(isabelle_target, platform, more_components_names)
- // Java parameters
+ // Java parameters
- val java_options_title = "# Java runtime options"
- val java_options: List[String] =
- (for {
- variable <-
- List(
- "ISABELLE_JAVA_SYSTEM_OPTIONS",
- "JEDIT_JAVA_SYSTEM_OPTIONS",
- "JEDIT_JAVA_OPTIONS")
- opt <- Word.explode(other_isabelle.getenv(variable))
- } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
+ val java_options_title = "# Java runtime options"
+ val java_options: List[String] =
+ (for {
+ variable <-
+ List(
+ "ISABELLE_JAVA_SYSTEM_OPTIONS",
+ "JEDIT_JAVA_SYSTEM_OPTIONS",
+ "JEDIT_JAVA_OPTIONS")
+ opt <- Word.explode(other_isabelle.getenv(variable))
+ } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
- val classpath: List[Path] =
+ val classpath: List[Path] =
+ {
+ val base = isabelle_target.absolute
+ Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
- val base = isabelle_target.absolute
- Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
- {
- val abs_path = path.absolute
- File.relative_path(base, abs_path) match {
- case Some(rel_path) => rel_path
- case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
- }
- }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
- }
+ val abs_path = path.absolute
+ File.relative_path(base, abs_path) match {
+ case Some(rel_path) => rel_path
+ case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
+ }
+ }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
+ }
- val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
+ val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
- // application bundling
-
- platform match {
- case Platform.Family.linux =>
- File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
- terminate_lines(java_options_title :: java_options))
+ // build heaps
- val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
- File.write(isabelle_run,
- File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
- .replaceAllLiterally("{CLASSPATH}",
- classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
- .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
- File.set_executable(isabelle_run, true)
-
- val linux_app = isabelle_target + Path.explode("contrib/linux_app")
- File.move(linux_app + Path.explode("Isabelle"),
- isabelle_target + Path.explode(isabelle_name))
- Isabelle_System.rm_tree(linux_app)
-
- val archive_name = isabelle_name + "_linux.tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- Bash.string(isabelle_name))
+ if (build_sessions.nonEmpty) {
+ progress.echo("Building heaps ...")
+ remote_build_heaps(options, platform, build_sessions, isabelle_target)
+ }
- case Platform.Family.macos =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
- .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
- .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
- .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
+ // application bundling
+
+ platform match {
+ case Platform.Family.linux =>
+ File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
+ terminate_lines(java_options_title :: java_options))
+
+ val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
+ File.write(isabelle_run,
+ File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
+ .replaceAllLiterally("{CLASSPATH}",
+ classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
+ .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
+ File.set_executable(isabelle_run, true)
+
+ val linux_app = isabelle_target + Path.explode("contrib/linux_app")
+ File.move(linux_app + Path.explode("Isabelle"),
+ isabelle_target + Path.explode(isabelle_name))
+ Isabelle_System.rm_tree(linux_app)
+
+ val archive_name = isabelle_name + "_linux.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ Bash.string(isabelle_name))
+
+
+ case Platform.Family.macos =>
+ File.write(isabelle_target + jedit_props,
+ File.read(isabelle_target + jedit_props)
+ .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
+ .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+ .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
+ .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
- // MacOS application bundle
+ // MacOS application bundle
- File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
+ File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
- val isabelle_app = Path.explode(isabelle_name + ".app")
- val app_dir = tmp_dir + isabelle_app
- File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
+ val isabelle_app = Path.explode(isabelle_name + ".app")
+ val app_dir = tmp_dir + isabelle_app
+ File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
- val app_contents = app_dir + Path.explode("Contents")
- val app_resources = app_contents + Path.explode("Resources")
- File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
+ val app_contents = app_dir + Path.explode("Contents")
+ val app_resources = app_contents + Path.explode("Resources")
+ File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
- File.write(app_contents + Path.explode("Info.plist"),
- File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
- .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- .replaceAllLiterally("{JAVA_OPTIONS}",
- terminate_lines(java_options.map(opt => "" + opt + ""))))
+ File.write(app_contents + Path.explode("Info.plist"),
+ File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
+ .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ .replaceAllLiterally("{JAVA_OPTIONS}",
+ terminate_lines(java_options.map(opt => "" + opt + ""))))
- for (cp <- classpath) {
- File.link(
- Path.explode("../Resources/" + isabelle_name + "/") + cp,
- app_contents + Path.explode("Java"),
- force = true)
- }
-
+ for (cp <- classpath) {
File.link(
- Path.explode("../Resources/" + isabelle_name + "/contrib/" +
- jdk_component + "/x86_64-darwin"),
- app_contents + Path.explode("PlugIns/bundled.jdk"),
+ Path.explode("../Resources/" + isabelle_name + "/") + cp,
+ app_contents + Path.explode("Java"),
force = true)
+ }
- File.link(
- Path.explode("../../Info.plist"),
- app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
- force = true)
+ File.link(
+ Path.explode("../Resources/" + isabelle_name + "/contrib/" +
+ jdk_component + "/x86_64-darwin"),
+ app_contents + Path.explode("PlugIns/bundled.jdk"),
+ force = true)
- File.link(
- Path.explode("Contents/Resources/" + isabelle_name),
- app_dir + Path.explode("Isabelle"),
- force = true)
+ File.link(
+ Path.explode("../../Info.plist"),
+ app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
+ force = true)
+
+ File.link(
+ Path.explode("Contents/Resources/" + isabelle_name),
+ app_dir + Path.explode("Isabelle"),
+ force = true)
- // application archive
+ // application archive
- val archive_name = isabelle_name + "_macos.tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- File.bash_path(isabelle_app))
+ val archive_name = isabelle_name + "_macos.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ File.bash_path(isabelle_app))
- case Platform.Family.windows =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*",
- "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
- .replaceAll("foldPainter=.*", "foldPainter=Square"))
+ case Platform.Family.windows =>
+ File.write(isabelle_target + jedit_props,
+ File.read(isabelle_target + jedit_props)
+ .replaceAll("lookAndFeel=.*",
+ "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
+ .replaceAll("foldPainter=.*", "foldPainter=Square"))
- // application launcher
+ // application launcher
- File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+ File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
- val app_template = Path.explode("~~/Admin/Windows/launch4j")
+ val app_template = Path.explode("~~/Admin/Windows/launch4j")
- File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
- (java_options_title :: java_options).map(_ + "\r\n").mkString)
+ File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
+ (java_options_title :: java_options).map(_ + "\r\n").mkString)
- val isabelle_xml = Path.explode("isabelle.xml")
- val isabelle_exe = Path.explode(isabelle_name + ".exe")
+ val isabelle_xml = Path.explode("isabelle.xml")
+ val isabelle_exe = Path.explode(isabelle_name + ".exe")
- File.write(tmp_dir + isabelle_xml,
- File.read(app_template + isabelle_xml)
- .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- .replaceAllLiterally("{OUTFILE}",
- File.platform_path(isabelle_target + isabelle_exe))
- .replaceAllLiterally("{ICON}",
- File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
- .replaceAllLiterally("{SPLASH}",
- File.platform_path(app_template + Path.explode("isabelle.bmp")))
- .replaceAllLiterally("{CLASSPATH}",
- cat_lines(classpath.map(cp =>
- " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
- .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
+ File.write(tmp_dir + isabelle_xml,
+ File.read(app_template + isabelle_xml)
+ .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ .replaceAllLiterally("{OUTFILE}",
+ File.platform_path(isabelle_target + isabelle_exe))
+ .replaceAllLiterally("{ICON}",
+ File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
+ .replaceAllLiterally("{SPLASH}",
+ File.platform_path(app_template + Path.explode("isabelle.bmp")))
+ .replaceAllLiterally("{CLASSPATH}",
+ cat_lines(classpath.map(cp =>
+ " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
+ .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
- execute(tmp_dir,
- "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+ execute(tmp_dir,
+ "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
- File.copy(app_template + Path.explode("manifest.xml"),
- isabelle_target + isabelle_exe.ext("manifest"))
+ File.copy(app_template + Path.explode("manifest.xml"),
+ isabelle_target + isabelle_exe.ext("manifest"))
- // Cygwin setup
+ // Cygwin setup
- val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
+ val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
- File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+ File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
- val cygwin_mirror =
- File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
+ val cygwin_mirror =
+ File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
- val cygwin_bat = Path.explode("Cygwin-Setup.bat")
- File.write(isabelle_target + cygwin_bat,
- File.read(cygwin_template + cygwin_bat)
- .replaceAllLiterally("{MIRROR}", cygwin_mirror))
- File.set_executable(isabelle_target + cygwin_bat, true)
+ val cygwin_bat = Path.explode("Cygwin-Setup.bat")
+ File.write(isabelle_target + cygwin_bat,
+ File.read(cygwin_template + cygwin_bat)
+ .replaceAllLiterally("{MIRROR}", cygwin_mirror))
+ File.set_executable(isabelle_target + cygwin_bat, true)
- for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
- val path = Path.explode(name)
- File.copy(cygwin_template + path,
- isabelle_target + Path.explode("contrib/cygwin") + path)
- }
+ for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
+ val path = Path.explode(name)
+ File.copy(cygwin_template + path,
+ isabelle_target + Path.explode("contrib/cygwin") + path)
+ }
- execute(isabelle_target,
- """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
- (if (Platform.is_macos) "-perm +100" else "-executable") +
- " -print0 > contrib/cygwin/isabelle/executables")
+ execute(isabelle_target,
+ """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
+ (if (Platform.is_macos) "-perm +100" else "-executable") +
+ " -print0 > contrib/cygwin/isabelle/executables")
- execute(isabelle_target,
- """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
- """> contrib/cygwin/isabelle/symlinks""")
+ execute(isabelle_target,
+ """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
+ """> contrib/cygwin/isabelle/symlinks""")
- execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
+ execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
- File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
+ File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
- // executable archive (self-extracting 7z)
+ // executable archive (self-extracting 7z)
- val archive_name = isabelle_name + ".7z"
- val exe_archive = tmp_dir + Path.explode(archive_name)
- exe_archive.file.delete
+ val archive_name = isabelle_name + ".7z"
+ val exe_archive = tmp_dir + Path.explode(archive_name)
+ exe_archive.file.delete
- progress.echo("Packaging " + archive_name + " ...")
- execute(tmp_dir,
- "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
- if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
+ progress.echo("Packaging " + archive_name + " ...")
+ execute(tmp_dir,
+ "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
+ if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
- val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
- val sfx_txt =
- File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
- replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
+ val sfx_txt =
+ File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
+ replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- Bytes.write(release.dist_dir + isabelle_exe,
- Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
- File.set_executable(release.dist_dir + isabelle_exe, true)
- }
- })
- progress.echo("DONE")
- }
+ Bytes.write(release.dist_dir + isabelle_exe,
+ Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
+ File.set_executable(release.dist_dir + isabelle_exe, true)
+ }
+ })
+ progress.echo("DONE")
}
@@ -715,6 +762,7 @@
var official_release = false
var proper_release_name: Option[String] = None
var website: Option[Path] = None
+ var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
@@ -732,6 +780,7 @@
-O official release (not release-candidate)
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
+ -b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
@@ -746,6 +795,7 @@
"O" -> (_ => official_release = true),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
+ "b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
@@ -772,8 +822,8 @@
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
- more_components = more_components, build_library = build_library,
- parallel_jobs = parallel_jobs)
+ more_components = more_components, build_sessions = build_sessions,
+ build_library = build_library, parallel_jobs = parallel_jobs)
}
}
}
diff -r 4005298550a6 -r 77f978dd8ffb src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala Wed Apr 10 13:34:55 2019 +0100
+++ b/src/Pure/Admin/components.scala Wed Apr 10 16:18:12 2019 +0200
@@ -55,6 +55,7 @@
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
+ copy_dir: Option[Path] = None,
progress: Progress = No_Progress)
{
Isabelle_System.mkdirs(base_dir)
@@ -66,6 +67,10 @@
progress.echo("Getting " + remote)
Bytes.write(archive, Url.read_bytes(Url(remote)))
}
+ for (dir <- copy_dir) {
+ Isabelle_System.mkdirs(dir)
+ File.copy(archive, dir)
+ }
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
diff -r 4005298550a6 -r 77f978dd8ffb src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala Wed Apr 10 13:34:55 2019 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala Wed Apr 10 16:18:12 2019 +0200
@@ -61,7 +61,9 @@
Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
website_dir =>
Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
- parallel_jobs = parallel_jobs, website = Some(website_dir)))
+ parallel_jobs = parallel_jobs,
+ build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
+ website = Some(website_dir)))
})
}
diff -r 4005298550a6 -r 77f978dd8ffb src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Apr 10 13:34:55 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Apr 10 16:18:12 2019 +0200
@@ -29,7 +29,7 @@
val options1 =
Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
case "default" => options
- case mode => options.bool.update("system_heaps", mode == "" | mode == "system")
+ case mode => options.bool.update("system_heaps", mode == "system")
}
val options2 =