# HG changeset patch # User wenzelm # Date 1475662160 -7200 # Node ID 68fcd61b87aebdeb7fd89619d792f409ca31b628 # Parent ac3ed62c53c3172f56efeed006fa97584094042e tuned; diff -r ac3ed62c53c3 -r 68fcd61b87ae src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Wed Oct 05 11:43:00 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Wed Oct 05 12:09:20 2016 +0200 @@ -13,12 +13,15 @@ object Build_History { - /* other Isabelle environment */ + /** other Isabelle environment **/ 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, @@ -32,46 +35,112 @@ def resolve_components(echo: Boolean): Unit = other_isabelle("components -a", redirect = true, echo = echo).check - val isabelle_home_user = + 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") + + + /* 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) + + Isabelle_System.mkdirs(etc_settings.dir) + File.write(etc_settings, + "# generated by Isabelle " + Calendar.getInstance.getTime + "\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" + Library.terminate_lines(component_settings)) + } + + + /* augment settings */ + + def augment_settings( + threads: Int, + arch_64: Boolean = false, + heap: Int = default_heap, + max_heap: Option[Int] = None, + more_settings: List[String]) + { + val 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 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 "") + + List( + "ML_HOME=" + File.bash_path(ml_home(ml_platform)), + "ML_PLATFORM=" + quote(ml_platform), + "ML_OPTIONS=" + quote(ml_options)) + } + + 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(Library.terminate_lines(_)))) + } } - /* settings environment */ - private def init_settings( - isabelle_home_user: Path, components_base: String, nonfree: Boolean): Path = - { - val etc_settings = isabelle_home_user + Path.explode("etc/settings") - - 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 " + Calendar.getInstance.getTime + "\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" + Library.terminate_lines(component_settings)) - - etc_settings - } - - - /* build_history */ + /** build_history **/ private val default_rev = "tip" private val default_threads = 1 @@ -118,74 +187,14 @@ progress.echo_if(verbose, hg.log(rev, options = "-l1")) - /* init settings */ + /* init other Isabelle */ val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier) - val etc_settings = init_settings(other_isabelle.isabelle_home_user, components_base, nonfree) + other_isabelle.reset_settings(components_base, nonfree) other_isabelle.resolve_components(verbose) - - /* augmented settings */ - - val 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 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 "") - - List( - "ML_HOME=" + File.bash_path(ml_home(ml_platform)), - "ML_PLATFORM=" + quote(ml_platform), - "ML_OPTIONS=" + quote(ml_options)) - } - - val thread_settings = - List( - "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", - "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") - - File.append(etc_settings, "\n" + - cat_lines(List(ml_settings, thread_settings).map(Library.terminate_lines(_)))) - - if (more_settings.nonEmpty) - File.append(etc_settings, "\n" + Library.terminate_lines(more_settings)) - - + other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings) other_isabelle.resolve_components(verbose)