# HG changeset patch # User wenzelm # Date 1510416254 -3600 # Node ID 19b6091c2137e5aee39fd99b3373ce5144a394d8 # Parent 897f1ac84aabb3ff3f8e6b91edb3fd9ec36bb2f4 support alternative USER_HOME directory; diff -r 897f1ac84aab -r 19b6091c2137 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sat Nov 11 16:28:15 2017 +0100 +++ b/src/Pure/Admin/build_history.scala Sat Nov 11 17:04:14 2017 +0100 @@ -96,6 +96,7 @@ /** build_history **/ + private val default_user_home = Path.explode("$USER_HOME") private val default_rev = "tip" private val default_multicore = (1, 1) private val default_heap = 1500 @@ -104,6 +105,7 @@ def build_history( options: Options, root: Path, + user_home: Path = default_user_home, progress: Progress = No_Progress, rev: String = default_rev, afp_rev: Option[String] = None, @@ -171,7 +173,8 @@ /* main */ val other_isabelle = - Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress) + Other_Isabelle(root, isabelle_identifier = isabelle_identifier, + user_home = user_home, progress = progress) val build_host = Isabelle_System.hostname() val build_history_date = Date.now() @@ -228,7 +231,7 @@ val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_result = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, - progress = build_out_progress)( + user_home = user_home, progress = build_out_progress)( "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) val build_end = Date.now() @@ -398,11 +401,12 @@ var rev = default_rev var ml_statistics_step = 1 var build_tags = List.empty[String] + var user_home = default_user_home var verbose = false var exit_code = false val getopts = Getopts(""" -Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...] +Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...] Options are: -A REV include $ISABELLE_HOME/AFP repository at given revision @@ -423,6 +427,7 @@ -r REV update to revision (default: """ + default_rev + """) -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) + -u DIR alternative USER_HOME directory -v verbose -x return overall exit code from build processes @@ -454,6 +459,7 @@ "r:" -> (arg => rev = arg), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), + "u:" -> (arg => user_home = Path.explode(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) @@ -467,11 +473,12 @@ val progress = new Console_Progress(stderr = true) val results = - build_history(Options.init(), root, progress = progress, rev = rev, afp_rev = afp_rev, - afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, - ml_statistics_step = ml_statistics_step, components_base = components_base, fresh = fresh, - nonfree = nonfree, multicore_base = multicore_base, multicore_list = multicore_list, - arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), + build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev, + afp_rev = afp_rev, afp_partition = afp_partition, + isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, + components_base = components_base, fresh = fresh, nonfree = nonfree, + multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, + heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, verbose = verbose, build_tags = build_tags, build_args = build_args)