# HG changeset patch # User wenzelm # Date 1476353623 -7200 # Node ID f88bae1922c4a26c817046d1ab2235241abf9c4b # Parent 450e06dabdd9e6dfddefe6f362dfb71fe63f798f clarified modules; diff -r 450e06dabdd9 -r f88bae1922c4 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Thu Oct 13 12:04:48 2016 +0200 +++ b/src/Pure/Admin/build_history.scala Thu Oct 13 12:13:43 2016 +0200 @@ -20,137 +20,75 @@ val META_INFO_MARKER = "\fmeta_info = " - - /** other Isabelle environment **/ - - private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) - { - other_isabelle => - - - /* static system */ + /* augment settings */ - def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = - Isabelle_System.bash( - "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, - env = null, cwd = isabelle_home.file, redirect = redirect, - progress_stdout = progress.echo_if(echo, _), - progress_stderr = progress.echo_if(echo, _)) + def augment_settings( + other_isabelle: Other_Isabelle, + threads: Int, + arch_64: Boolean = false, + heap: Int = default_heap, + max_heap: Option[Int] = None, + more_settings: List[String]): String = + { + val (ml_platform, ml_settings) = + { + val windows_32 = "x86-windows" + val windows_64 = "x86_64-windows" + val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out + val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out + val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out - def copy_dir(dir1: Path, dir2: Path): Unit = - bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check - - def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = - bash("bin/isabelle " + cmdline, redirect, echo) + val polyml_home = + try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir } + catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } - def resolve_components(echo: Boolean): Unit = - other_isabelle("components -a", redirect = true, echo = echo).check + def ml_home(platform: String): Path = polyml_home + Path.explode(platform) - val isabelle_home_user: Path = - Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) + def err(platform: String): Nothing = + error("Platform " + platform + " unavailable on this machine") - val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") - val log_dir: Path = isabelle_home_user + Path.explode("log") - - - /* reset settings */ - - def reset_settings(components_base: String, nonfree: Boolean) - { - if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) - error("Cannot proceed with existing user settings file: " + etc_settings) + def check_dir(platform: String): Boolean = + platform != "" && ml_home(platform).is_dir - Isabelle_System.mkdirs(etc_settings.dir) - File.write(etc_settings, - "# generated by Isabelle " + Date.now() + "\n" + - "#-*- shell-script -*- :mode=shellscript:\n") + val ml_platform = + if (Platform.is_windows && arch_64) { + if (check_dir(windows_64)) windows_64 else err(windows_64) + } + else if (Platform.is_windows && !arch_64) { + if (check_dir(windows_32)) windows_32 + else platform_32 // x86-cygwin + } + else { + val (platform, platform_name) = + if (arch_64) (platform_64, "x86_64-" + platform_family) + else (platform_32, "x86-" + platform_family) + if (check_dir(platform)) platform else err(platform_name) + } - val component_settings = - { - val components_base_path = - if (components_base == "") isabelle_home_user.dir + Path.explode("contrib") - else Path.explode(components_base).expand + val ml_options = + "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + + " --gcthreads " + threads + + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") - val catalogs = - if (nonfree) List("main", "optional", "nonfree") else List("main", "optional") - - catalogs.map(catalog => - "init_components " + File.bash_path(components_base_path) + - " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") - } - File.append(etc_settings, "\n" + terminate_lines(component_settings)) + (ml_platform, + List( + "ML_HOME=" + File.bash_path(ml_home(ml_platform)), + "ML_PLATFORM=" + quote(ml_platform), + "ML_OPTIONS=" + quote(ml_options))) } - - /* augment settings */ - - def augment_settings( - threads: Int, - arch_64: Boolean = false, - heap: Int = default_heap, - max_heap: Option[Int] = None, - more_settings: List[String]): String = - { - val (ml_platform, ml_settings) = - { - val windows_32 = "x86-windows" - val windows_64 = "x86_64-windows" - val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out - val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out - val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out - - val polyml_home = - try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir } - catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } - - def ml_home(platform: String): Path = polyml_home + Path.explode(platform) - - def err(platform: String): Nothing = - error("Platform " + platform + " unavailable on this machine") - - def check_dir(platform: String): Boolean = - platform != "" && ml_home(platform).is_dir + val thread_settings = + List( + "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", + "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") - val ml_platform = - if (Platform.is_windows && arch_64) { - if (check_dir(windows_64)) windows_64 else err(windows_64) - } - else if (Platform.is_windows && !arch_64) { - if (check_dir(windows_32)) windows_32 - else platform_32 // x86-cygwin - } - else { - val (platform, platform_name) = - if (arch_64) (platform_64, "x86_64-" + platform_family) - else (platform_32, "x86-" + platform_family) - if (check_dir(platform)) platform else err(platform_name) - } - - val ml_options = - "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + - " --gcthreads " + threads + - (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") + val settings = + List(ml_settings, thread_settings) ::: + (if (more_settings.isEmpty) Nil else List(more_settings)) - (ml_platform, - List( - "ML_HOME=" + File.bash_path(ml_home(ml_platform)), - "ML_PLATFORM=" + quote(ml_platform), - "ML_OPTIONS=" + quote(ml_options))) - } + File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) - val thread_settings = - List( - "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", - "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") - - val settings = - List(ml_settings, thread_settings) ::: - (if (more_settings.isEmpty) Nil else List(more_settings)) - - File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) - - ml_platform - } + ml_platform } @@ -216,10 +154,10 @@ { /* init settings */ - other_isabelle.reset_settings(components_base, nonfree) + other_isabelle.init_settings(components_base, nonfree) other_isabelle.resolve_components(verbose) val ml_platform = - other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings) + augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) val isabelle_output_log = isabelle_output + Path.explode("log") @@ -253,7 +191,7 @@ /* output log */ val log_path = - other_isabelle.log_dir + + other_isabelle.isabelle_home_user + Path.explode("log") + Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() diff -r 450e06dabdd9 -r f88bae1922c4 src/Pure/Admin/other_isabelle.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/other_isabelle.scala Thu Oct 13 12:13:43 2016 +0200 @@ -0,0 +1,66 @@ +/* Title: Pure/Admin/other_isabelle.scala + Author: Makarius + +Manage other Isabelle distributions. +*/ + +package isabelle + + +private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) +{ + other_isabelle => + + + /* static system */ + + def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = + Isabelle_System.bash( + "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, + env = null, cwd = isabelle_home.file, redirect = redirect, + progress_stdout = progress.echo_if(echo, _), + progress_stderr = progress.echo_if(echo, _)) + + def copy_dir(dir1: Path, dir2: Path): Unit = + bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check + + def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = + bash("bin/isabelle " + cmdline, redirect, echo) + + def resolve_components(echo: Boolean): Unit = + other_isabelle("components -a", redirect = true, echo = echo).check + + val isabelle_home_user: Path = + Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) + + val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") + + + /* init settings */ + + def init_settings(components_base: String, nonfree: Boolean) + { + if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) + error("Cannot proceed with existing user settings file: " + etc_settings) + + Isabelle_System.mkdirs(etc_settings.dir) + File.write(etc_settings, + "# generated by Isabelle " + Date.now() + "\n" + + "#-*- shell-script -*- :mode=shellscript:\n") + + val component_settings = + { + val components_base_path = + if (components_base == "") isabelle_home_user.dir + Path.explode("contrib") + else Path.explode(components_base).expand + + val catalogs = + if (nonfree) List("main", "optional", "nonfree") else List("main", "optional") + + catalogs.map(catalog => + "init_components " + File.bash_path(components_base_path) + + " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") + } + File.append(etc_settings, "\n" + terminate_lines(component_settings)) + } +} diff -r 450e06dabdd9 -r f88bae1922c4 src/Pure/build-jars --- a/src/Pure/build-jars Thu Oct 13 12:04:48 2016 +0200 +++ b/src/Pure/build-jars Thu Oct 13 12:13:43 2016 +0200 @@ -17,6 +17,7 @@ Admin/ci_api.scala Admin/ci_profile.scala Admin/isabelle_cronjob.scala + Admin/other_isabelle.scala Admin/remote_dmg.scala Concurrent/consumer_thread.scala Concurrent/counter.scala