1.1 --- a/src/Pure/Admin/build_history.scala Sat Nov 11 16:28:15 2017 +0100
1.2 +++ b/src/Pure/Admin/build_history.scala Sat Nov 11 17:04:14 2017 +0100
1.3 @@ -96,6 +96,7 @@
1.4
1.5 /** build_history **/
1.6
1.7 + private val default_user_home = Path.explode("$USER_HOME")
1.8 private val default_rev = "tip"
1.9 private val default_multicore = (1, 1)
1.10 private val default_heap = 1500
1.11 @@ -104,6 +105,7 @@
1.12 def build_history(
1.13 options: Options,
1.14 root: Path,
1.15 + user_home: Path = default_user_home,
1.16 progress: Progress = No_Progress,
1.17 rev: String = default_rev,
1.18 afp_rev: Option[String] = None,
1.19 @@ -171,7 +173,8 @@
1.20 /* main */
1.21
1.22 val other_isabelle =
1.23 - Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress)
1.24 + Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
1.25 + user_home = user_home, progress = progress)
1.26
1.27 val build_host = Isabelle_System.hostname()
1.28 val build_history_date = Date.now()
1.29 @@ -228,7 +231,7 @@
1.30 val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
1.31 val build_result =
1.32 Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
1.33 - progress = build_out_progress)(
1.34 + user_home = user_home, progress = build_out_progress)(
1.35 "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
1.36 strict = false)
1.37 val build_end = Date.now()
1.38 @@ -398,11 +401,12 @@
1.39 var rev = default_rev
1.40 var ml_statistics_step = 1
1.41 var build_tags = List.empty[String]
1.42 + var user_home = default_user_home
1.43 var verbose = false
1.44 var exit_code = false
1.45
1.46 val getopts = Getopts("""
1.47 -Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
1.48 +Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
1.49
1.50 Options are:
1.51 -A REV include $ISABELLE_HOME/AFP repository at given revision
1.52 @@ -423,6 +427,7 @@
1.53 -r REV update to revision (default: """ + default_rev + """)
1.54 -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
1.55 -t TAG free-form build tag (multiple occurrences possible)
1.56 + -u DIR alternative USER_HOME directory
1.57 -v verbose
1.58 -x return overall exit code from build processes
1.59
1.60 @@ -454,6 +459,7 @@
1.61 "r:" -> (arg => rev = arg),
1.62 "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
1.63 "t:" -> (arg => build_tags = build_tags ::: List(arg)),
1.64 + "u:" -> (arg => user_home = Path.explode(arg)),
1.65 "v" -> (_ => verbose = true),
1.66 "x" -> (_ => exit_code = true))
1.67
1.68 @@ -467,11 +473,12 @@
1.69 val progress = new Console_Progress(stderr = true)
1.70
1.71 val results =
1.72 - build_history(Options.init(), root, progress = progress, rev = rev, afp_rev = afp_rev,
1.73 - afp_partition = afp_partition, isabelle_identifier = isabelle_identifier,
1.74 - ml_statistics_step = ml_statistics_step, components_base = components_base, fresh = fresh,
1.75 - nonfree = nonfree, multicore_base = multicore_base, multicore_list = multicore_list,
1.76 - arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
1.77 + build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
1.78 + afp_rev = afp_rev, afp_partition = afp_partition,
1.79 + isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
1.80 + components_base = components_base, fresh = fresh, nonfree = nonfree,
1.81 + multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
1.82 + heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
1.83 max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
1.84 verbose = verbose, build_tags = build_tags, build_args = build_args)
1.85