--- a/src/Pure/Tools/build_history.scala Mon Oct 03 21:55:41 2016 +0200
+++ b/src/Pure/Tools/build_history.scala Tue Oct 04 13:56:02 2016 +0200
@@ -16,6 +16,8 @@
/* build_history */
private val default_rev = "tip"
+ private val default_threads = 1
+ private val default_heap = 500
private val default_isabelle_identifier = "build_history"
def build_history(
@@ -25,9 +27,16 @@
components_base: String = "",
fresh: Boolean = false,
nonfree: Boolean = false,
+ threads: Int = default_threads,
+ arch_64: Boolean = false,
+ heap: Int = default_heap,
+ more_settings: List[String] = Nil,
verbose: Boolean = false,
build_args: List[String] = Nil): Process_Result =
{
+ if (threads < 1) error("Bad threads value < 1: " + threads)
+ if (heap < 100) error("Bad heap value < 100: " + heap)
+
hg.update(rev = rev, clean = true)
if (verbose) Output.writeln(hg.log(rev, options = "-l1"))
@@ -36,19 +45,27 @@
" " + script, cwd = hg.root.file, env = null)
def isabelle(cmdline: String): Process_Result = bash("bin/isabelle " + cmdline)
-
val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out)
- /* init settings */
+ /* reset settings */
+
+ val etc_settings: Path = 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")
+
+
+ /* component settings */
+
+ val component_settings =
{
- val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
- if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
- error("User settings file already exists: " + etc_settings)
-
- Isabelle_System.mkdirs(etc_settings.dir)
-
val components_base_path =
if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
else Path.explode(components_base).expand
@@ -56,19 +73,74 @@
val catalogs =
if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
- val settings =
- catalogs.map(catalog =>
- "init_components " + File.bash_path(components_base_path) +
- " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
+ 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))
+
+
+ /* ML settings */
+
+ val ml_settings =
+ {
+ val windows_32 = "x86-windows"
+ val windows_64 = "x86_64-windows"
+ val platform_32 = isabelle("getenv -b ISABELLE_PLATFORM32").check.out
+ val platform_64 = isabelle("getenv -b ISABELLE_PLATFORM64").check.out
+ val platform_family = isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
+
+ val polyml_home = Path.explode(isabelle("getenv -b ML_HOME").check.out).dir
+ def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
+
+ def err(platform: String): Nothing =
+ error("Platform " + platform + " unavailable on this machine")
- File.write(etc_settings,
- "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
- "#-*- shell-script -*- :mode=shellscript:\n\n" +
- Library.terminate_lines(settings))
+ 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 =
+ "-H " + heap + " --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))
}
- /* components */
+ /* thread settings */
+
+ val thread_settings =
+ List(
+ "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
+ "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
+
+
+ /* build */
+
+ 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))
isabelle("components -a").check.print_if(verbose)
isabelle("jedit -b" + (if (fresh) " -f" else "")).check.print_if(verbose)
@@ -84,8 +156,12 @@
Command_Line.tool0 {
var allow = false
var components_base = ""
+ var heap: Option[Int] = None
+ var threads = default_threads
var isabelle_identifier = default_isabelle_identifier
+ var more_settings: List[String] = Nil
var fresh = false
+ var arch_64 = false
var nonfree = false
var rev = default_rev
var verbose = false
@@ -94,10 +170,14 @@
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
Options are:
- -A allow irreversible cleanup of REPOSITORY clone
+ -A allow irreversible cleanup of REPOSITORY clone (required)
-C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+ -H HEAP minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
+ -M THREADS number of threads for Poly/ML RTS and Isabelle/ML (default: """ + default_threads + """)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
+ -e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
+ -m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-n include nonfree components
-r REV update to revision (default: """ + default_rev + """)
-v verbose
@@ -107,8 +187,17 @@
""",
"A" -> (_ => allow = true),
"C:" -> (arg => components_base = arg),
+ "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
+ "M:" -> (arg => threads = Value.Int.parse(arg)),
"N:" -> (arg => isabelle_identifier = arg),
+ "e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
+ "m:" ->
+ {
+ case "32" | "x86" => arch_64 = false
+ case "64" | "x86_64" => arch_64 = true
+ case bad => error("Bad processor architecture: " + quote(bad))
+ },
"n" -> (_ => nonfree = true),
"r:" -> (arg => rev = arg),
"v" -> (_ => verbose = true))
@@ -129,7 +218,9 @@
val res =
build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier,
components_base = components_base, fresh = fresh, nonfree = nonfree,
- verbose = verbose, build_args = build_args)
+ threads = threads, arch_64 = arch_64,
+ heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
+ more_settings = more_settings, verbose = verbose, build_args = build_args)
res.print
if (!res.ok) sys.exit(res.rc)
})