# HG changeset patch # User wenzelm # Date 1674596261 -3600 # Node ID bd5045cd6ca919272a9f7ee4c35faba7f63b0508 # Parent 0e375276227b1809d9c5746cb9052765a8cb2f99# Parent 351eee493580dc0d076eba358ada505572e0f4c6 merged diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/Admin/build_history.scala --- 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), diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/Admin/build_release.scala --- 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)) diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/Admin/isabelle_cronjob.scala --- 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) { diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/Admin/other_isabelle.scala --- 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) } diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/General/path.scala --- 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 diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/General/ssh.scala --- 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 diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/System/components.scala --- 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]] = diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/System/isabelle_system.scala --- 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)) diff -r 0e375276227b -r bd5045cd6ca9 src/Pure/Tools/dotnet_setup.scala --- 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"