--- a/src/Pure/Admin/build_history.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/Admin/build_history.scala Tue Jan 24 22:37:41 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,14 +98,12 @@
def local_build(
options: Options,
root: Path,
- user_home: Path = default_user_home,
progress: Progress = new Progress,
afp: Boolean = false,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
- components_base: Path = Components.default_components_base,
fresh: Boolean = false,
hostname: String = "",
multicore_base: Boolean = false,
@@ -176,8 +173,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()
@@ -190,7 +186,7 @@
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
- components_base = components_base,
+ components_base = Components.standard_components_base,
catalogs = Components.optional_catalogs)
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
@@ -200,20 +196,14 @@
File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
val isabelle_output =
- other_isabelle.isabelle_home_user + Path.explode("heaps") +
- Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
+ other_isabelle.expand_path(
+ Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER"))
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
if (first_build) {
other_isabelle.resolve_components(echo = verbose)
-
- if (fresh) {
- Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
- }
- other_isabelle.bash(
- "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty")) + ":$PATH\" " +
- "bin/isabelle jedit -b", redirect = true, echo = verbose).check
+ other_isabelle.scala_build(fresh = fresh, echo = verbose)
for {
tool <- List("ghc_setup", "ocaml_setup")
@@ -227,7 +217,7 @@
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
- (other_isabelle.isabelle_home_user + Path.explode("mash_state")).file.delete
+ other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/mash_state")).file.delete
val log_path =
other_isabelle.isabelle_home_user +
@@ -237,7 +227,7 @@
Isabelle_System.make_directory(log_path.dir)
- val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
+ val build_out = other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/log/build.out"))
val build_out_progress = new File_Progress(build_out)
build_out.file.delete
@@ -251,11 +241,10 @@
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
- val build_isabelle =
+ val build_result =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
- user_home = user_home, progress = build_out_progress)
- val build_result =
- build_isabelle.bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions),
+ progress = build_out_progress)
+ .bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
val build_end = Date.now()
@@ -404,7 +393,6 @@
Command_Line.tool {
var afp = false
var multicore_base = false
- var components_base: Path = Components.default_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
@@ -420,7 +408,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
@@ -430,8 +417,6 @@
Options are:
-A include $ISABELLE_HOME/AFP directory
-B first multicore build serves as base for scheduling information
- -C DIR base directory for Isabelle components (default: """ +
- Components.default_components_base + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
@@ -450,7 +435,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
@@ -462,7 +446,6 @@
""",
"A" -> (_ => afp = true),
"B" -> (_ => multicore_base = true),
- "C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
@@ -483,7 +466,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))
@@ -497,10 +479,10 @@
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,
+ component_repository = component_repository,
fresh = fresh, hostname = hostname, multicore_base = multicore_base,
multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
--- a/src/Pure/Admin/build_release.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/Admin/build_release.scala Tue Jan 24 22:37:41 2023 +0100
@@ -470,12 +470,7 @@
other_isabelle.init_components(components_base = context.components_base))
other_isabelle.resolve_components(echo = true)
- try {
- other_isabelle.bash(
- "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" +
- "bin/isabelle jedit -b", echo = true).check
- }
- catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
+ other_isabelle.scala_build(echo = true)
try {
other_isabelle.bash(
@@ -565,10 +560,12 @@
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
- Components.resolve(context.components_base, bundled_components,
- target_dir = Some(contrib_dir),
- copy_dir = Some(context.dist_dir + Path.explode("contrib")),
- progress = progress)
+ for (name <- bundled_components) {
+ Components.resolve(context.components_base, name,
+ target_dir = Some(contrib_dir),
+ copy_dir = Some(context.dist_dir + Path.explode("contrib")),
+ progress = progress)
+ }
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Jan 24 22:37:41 2023 +0100
@@ -410,8 +410,7 @@
options =
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -R " + Bash.string(Components.default_component_repository) +
- " -C '$USER_HOME/.isabelle/contrib' -f " +
- r.build_history_options,
+ " -f " + r.build_history_options,
args = "-o timeout=10800 " + r.args)
for ((log_name, bytes) <- results) {
--- a/src/Pure/Admin/other_isabelle.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Tue Jan 24 22:37:41 2023 +0100
@@ -1,7 +1,8 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
-Manage other Isabelle distributions.
+Manage other Isabelle distributions: support historic versions starting from
+tag "build_history_base".
*/
package isabelle
@@ -11,21 +12,17 @@
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
) {
- other_isabelle =>
-
override def toString: String = isabelle_home.toString
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
@@ -42,25 +39,50 @@
strict: Boolean = true
): Process_Result = {
progress.bash(
- "export USER_HOME=" + File.bash_path(user_home) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
}
- def resolve_components(echo: Boolean): Unit = {
- other_isabelle.bash(
- "bin/isabelle env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
- " isabelle components -a", redirect = true, echo = echo).check
+ def getenv(name: String): String =
+ bash("bin/isabelle getenv -b " + Bash.string(name)).check.out
+
+ val settings: Isabelle_System.Settings = (name: String) => getenv(name)
+
+ def expand_path(path: Path): Path = path.expand_env(settings)
+ def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
+
+ val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
+
+ def etc: Path = isabelle_home_user + Path.explode("etc")
+ def etc_settings: Path = etc + Path.explode("settings")
+ def etc_preferences: Path = etc + Path.explode("preferences")
+
+ def resolve_components(echo: Boolean = false): Unit = {
+ val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
+ for (path <- missing) {
+ Components.resolve(path.dir, path.file_name,
+ progress = if (echo) progress else new Progress)
+ }
}
- def getenv(name: String): String =
- other_isabelle.bash("bin/isabelle getenv -b " + Bash.string(name)).check.out
+ def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
+ if (fresh) {
+ Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
+ }
- val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
-
- val etc: Path = isabelle_home_user + Path.explode("etc")
- val etc_settings: Path = etc + Path.explode("settings")
- val etc_preferences: Path = etc + Path.explode("preferences")
+ val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
+ if (!expand_path(dummy_stty).is_file) {
+ Isabelle_System.copy_file(dummy_stty,
+ Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
+ }
+ try {
+ bash(
+ "export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
+ "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
+ "bin/isabelle jedit -b", echo = echo).check
+ }
+ catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) }
+ }
/* components */
@@ -93,15 +115,14 @@
else false
def init_settings(settings: List[String]): Unit = {
- if (!clean_settings()) {
- error("Cannot proceed with existing user settings file: " + etc_settings)
+ if (clean_settings()) {
+ Isabelle_System.make_directory(etc_settings.dir)
+ File.write(etc_settings,
+ "# generated by Isabelle " + Date.now() + "\n" +
+ "#-*- shell-script -*- :mode=shellscript:\n" +
+ settings.mkString("\n", "\n", "\n"))
}
-
- Isabelle_System.make_directory(etc_settings.dir)
- File.write(etc_settings,
- "# generated by Isabelle " + Date.now() + "\n" +
- "#-*- shell-script -*- :mode=shellscript:\n" +
- settings.mkString("\n", "\n", "\n"))
+ else error("Cannot proceed with existing user settings file: " + etc_settings)
}
--- a/src/Pure/General/path.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/General/path.scala Tue Jan 24 22:37:41 2023 +0100
@@ -283,7 +283,7 @@
/* expand */
- def expand_env(env: JMap[String, String]): Path = {
+ def expand_env(env: Isabelle_System.Settings): Path = {
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
case Path.Variable(s) =>
@@ -297,7 +297,7 @@
new Path(Path.norm_elems(elems.flatMap(eval)))
}
- def expand: Path = expand_env(Isabelle_System.settings())
+ def expand: Path = expand_env(Isabelle_System.settings_env())
def file_name: String = expand.base.implode
--- a/src/Pure/General/ssh.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/General/ssh.scala Tue Jan 24 22:37:41 2023 +0100
@@ -170,7 +170,8 @@
}
}
- val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
+ val settings: Isabelle_System.Settings =
+ (name: String) => if (name == "HOME" || name == "USER_HOME") user_home else ""
override def close(): Unit = {
if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
@@ -185,9 +186,11 @@
settings: Boolean = true,
strict: Boolean = true
): Process_Result = {
- val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line)
- run_command("ssh", args = args1, progress_stdout = progress_stdout,
- progress_stderr = progress_stderr, strict = strict)
+ run_command("ssh",
+ args = Bash.string(host) + " " + Bash.string(cmd_line),
+ progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr,
+ strict = strict)
}
override def download_file(
@@ -209,6 +212,11 @@
/* remote file-system */
override def expand_path(path: Path): Path = path.expand_env(settings)
+ override def absolute_path(path: Path): Path = {
+ val path1 = expand_path(path)
+ if (path1.is_absolute) path1 else Path.explode(user_home) + path1
+ }
+
def remote_path(path: Path): String = expand_path(path).implode
override def bash_path(path: Path): String = Bash.string(remote_path(path))
@@ -355,6 +363,7 @@
def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
def expand_path(path: Path): Path = path.expand
+ def absolute_path(path: Path): Path = path.absolute
def bash_path(path: Path): String = File.bash_path(path)
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
--- a/src/Pure/System/components.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/System/components.scala Tue Jan 24 22:37:41 2023 +0100
@@ -39,6 +39,7 @@
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ val standard_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib")
val default_catalogs: List[String] = List("main")
val optional_catalogs: List[String] = List("main", "optional")
@@ -57,7 +58,7 @@
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
ssh.execute(
- "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive),
+ "tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive),
progress_stdout = progress.echo,
progress_stderr = progress.echo).check
name
@@ -65,7 +66,7 @@
def resolve(
base_dir: Path,
- names: List[String],
+ name: String,
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
component_repository: String = Components.default_component_repository,
@@ -73,19 +74,17 @@
progress: Progress = new Progress
): Unit = {
ssh.make_directory(base_dir)
- for (name <- names) {
- val archive_name = Archive(name)
- val archive = base_dir + Path.explode(archive_name)
- if (!ssh.is_file(archive)) {
- val remote = Url.append_path(component_repository, archive_name)
- ssh.download_file(remote, archive, progress = progress)
- }
- for (dir <- copy_dir) {
- ssh.make_directory(dir)
- ssh.copy_file(archive, dir)
- }
- unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
+ val archive_name = Archive(name)
+ val archive = base_dir + Path.basic(archive_name)
+ if (!ssh.is_file(archive)) {
+ val remote = Url.append_path(component_repository, archive_name)
+ ssh.download_file(remote, archive, progress = progress)
}
+ for (dir <- copy_dir) {
+ ssh.make_directory(dir)
+ ssh.copy_file(archive, dir)
+ }
+ unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
--- a/src/Pure/System/isabelle_system.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Jan 24 22:37:41 2023 +0100
@@ -21,6 +21,13 @@
object Isabelle_System {
/* settings environment */
+ trait Settings { def get(name: String): String }
+ trait Settings_Env extends Settings { def env: JMap[String, String] }
+
+ class Env(val env: JMap[String, String]) extends Settings_Env {
+ override def get(name: String): String = Option(env.get(name)).getOrElse("")
+ }
+
def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
val env0 = isabelle.setup.Environment.settings()
if (putenv.isEmpty) env0
@@ -31,10 +38,12 @@
}
}
- def getenv(name: String, env: JMap[String, String] = settings()): String =
- Option(env.get(name)).getOrElse("")
+ def settings_env(putenv: List[(String, String)] = Nil): Settings_Env =
+ new Env(settings(putenv = putenv))
- def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
+ def getenv(name: String, env: Settings = settings_env()): String = env.get(name)
+
+ def getenv_strict(name: String, env: Settings = settings_env()): String =
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
--- a/src/Pure/Tools/dotnet_setup.scala Tue Jan 24 16:32:54 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Tue Jan 24 22:37:41 2023 +0100
@@ -50,7 +50,7 @@
self.ISABELLE_PLATFORM64))
}
- def default_target_dir: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ def default_target_dir: Path = Components.default_components_base
def default_install_url: String = "https://dot.net/v1/dotnet-install"
def default_version: String = "6.0.402"