# HG changeset patch # User wenzelm # Date 1475585586 -7200 # Node ID a14fe26c014405abf214ac8b8c4ffb98eca14dae # Parent 90017a182892f9587b566c56aa690315afdd161a clarified heap options; diff -r 90017a182892 -r a14fe26c0144 src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Tue Oct 04 14:39:31 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Tue Oct 04 14:53:06 2016 +0200 @@ -30,6 +30,7 @@ threads: Int = default_threads, arch_64: Boolean = false, heap: Int = default_heap, + max_heap: Option[Int] = None, more_settings: List[String] = Nil, verbose: Boolean = false, build_args: List[String] = Nil): Process_Result = @@ -37,8 +38,12 @@ /* sanity checks */ if (threads < 1) error("Bad threads value < 1: " + threads) + if (heap < 100) error("Bad heap value < 100: " + heap) + if (max_heap.isDefined && max_heap.get < heap) + error("Bad max_heap value < heap: " + max_heap.get) + System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => case _ => error("Cannot run build_history within existing Isabelle settings environment") @@ -129,7 +134,8 @@ } val ml_options = - "-H " + heap + " --gcthreads " + threads + + "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + + " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") List( @@ -167,6 +173,7 @@ var allow = false var components_base = "" var heap: Option[Int] = None + var max_heap: Option[Int] = None var threads = default_threads var isabelle_identifier = default_isabelle_identifier var more_settings: List[String] = Nil @@ -182,9 +189,10 @@ Options are: -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) + -H SIZE 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 + """) + -U SIZE maximal ML heap in MB (default: unbounded) -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) @@ -200,6 +208,7 @@ "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => threads = Value.Int.parse(arg)), "N:" -> (arg => isabelle_identifier = arg), + "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "m:" -> @@ -230,7 +239,8 @@ components_base = components_base, fresh = fresh, nonfree = nonfree, 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) + max_heap = max_heap, more_settings = more_settings, verbose = verbose, + build_args = build_args) res.print if (!res.ok) sys.exit(res.rc) })