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