--- 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)