--- a/src/Pure/Admin/build_history.scala Tue Jan 24 16:08:28 2023 +0100
+++ b/src/Pure/Admin/build_history.scala Tue Jan 24 17:16:00 2023 +0100
@@ -91,7 +91,6 @@
/** local build **/
- private val default_user_home = Path.USER_HOME
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
@@ -99,7 +98,6 @@
def local_build(
options: Options,
root: Path,
- user_home: Path = default_user_home,
progress: Progress = new Progress,
afp: Boolean = false,
afp_partition: Int = 0,
@@ -176,8 +174,7 @@
/* main */
val other_isabelle =
- Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
- user_home = user_home, progress = progress)
+ Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress)
val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
@@ -247,7 +244,7 @@
val build_result =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
- user_home = user_home, progress = build_out_progress)
+ progress = build_out_progress)
.bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
@@ -413,7 +410,6 @@
var output_file = ""
var ml_statistics_step = 1
var build_tags = List.empty[String]
- var user_home = default_user_home
var verbose = false
var exit_code = false
@@ -443,7 +439,6 @@
-p TEXT additional text for generated etc/preferences
-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
@@ -476,7 +471,6 @@
"p:" -> (arg => more_preferences = more_preferences ::: List(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))
@@ -490,7 +484,7 @@
val progress = new Console_Progress(stderr = true)
val results =
- local_build(Options.init(), root, user_home = user_home, progress = progress,
+ local_build(Options.init(), root, progress = progress,
afp = afp, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository, components_base = components_base,
--- a/src/Pure/Admin/other_isabelle.scala Tue Jan 24 16:08:28 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Tue Jan 24 17:16:00 2023 +0100
@@ -11,17 +11,15 @@
def apply(
isabelle_home: Path,
isabelle_identifier: String = "",
- user_home: Path = Path.USER_HOME,
progress: Progress = new Progress
): Other_Isabelle = {
- new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
+ new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress)
}
}
final class Other_Isabelle private(
val isabelle_home: Path,
val isabelle_identifier: String,
- user_home: Path,
progress: Progress
) {
override def toString: String = isabelle_home.toString
@@ -40,7 +38,7 @@
strict: Boolean = true
): Process_Result = {
progress.bash(
- "export USER_HOME=" + File.bash_path(user_home) + "\n" +
+ "export USER_HOME=" + File.bash_path(Path.USER_HOME) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
}