# HG changeset patch # User wenzelm # Date 1689847894 -7200 # Node ID a4dee214dfcf9ac0b4c21958bc5e1c527d66a747 # Parent 406d34a8a67ae21fe83c58e42c21ac8c21779c2b clarified file location: to be used by regular Isabelle/Scala tools; diff -r 406d34a8a67a -r a4dee214dfcf etc/build.props --- a/etc/build.props Thu Jul 20 12:10:54 2023 +0200 +++ b/etc/build.props Thu Jul 20 12:11:34 2023 +0200 @@ -47,7 +47,6 @@ src/Pure/Admin/component_zstd.scala \ src/Pure/Admin/isabelle_cronjob.scala \ src/Pure/Admin/isabelle_devel.scala \ - src/Pure/Admin/other_isabelle.scala \ src/Pure/Concurrent/consumer_thread.scala \ src/Pure/Concurrent/counter.scala \ src/Pure/Concurrent/delay.scala \ @@ -168,6 +167,7 @@ src/Pure/System/mingw.scala \ src/Pure/System/nodejs.scala \ src/Pure/System/options.scala \ + src/Pure/System/other_isabelle.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ src/Pure/System/process_result.scala \ diff -r 406d34a8a67a -r a4dee214dfcf src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Thu Jul 20 12:10:54 2023 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -/* Title: Pure/Admin/other_isabelle.scala - Author: Makarius - -Manage other Isabelle distributions: support historic versions starting from -tag "build_history_base". -*/ - -package isabelle - - -object Other_Isabelle { - def apply( - root: Path, - isabelle_identifier: String = "", - ssh: SSH.System = SSH.Local, - progress: Progress = new Progress - ): Other_Isabelle = { - val (isabelle_home, url_prefix) = - ssh match { - case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) - case _ => - if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { - error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") - } - (root.canonical, "") - } - val isabelle_home_url = url_prefix + isabelle_home.implode - new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) - } -} - -final class Other_Isabelle private( - val isabelle_home: Path, - val isabelle_identifier: String, - isabelle_home_url: String, - ssh: SSH.System, - progress: Progress -) { - override def toString: String = isabelle_home_url - - - /* static system */ - - def bash( - script: String, - redirect: Boolean = false, - echo: Boolean = false, - strict: Boolean = true - ): Process_Result = { - ssh.execute( - Isabelle_System.export_isabelle_identifier(isabelle_identifier) + - "cd " + ssh.bash_path(isabelle_home) + "\n" + script, - progress_stdout = progress.echo_if(echo, _), - progress_stderr = progress.echo_if(echo, _), - redirect = redirect, - settings = false, - strict = strict) - } - - 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") - - - /* components */ - - def init_components( - components_base: String = Components.dynamic_components_base, - catalogs: List[String] = Components.default_catalogs, - components: List[String] = Nil - ): List[String] = { - val admin = Components.admin(Path.ISABELLE_HOME).implode - - catalogs.map(name => - "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: - components.map(name => - "init_component " + quote(components_base) + "/" + name) - } - - def resolve_components( - echo: Boolean = false, - clean_platforms: Option[List[Platform.Family.Value]] = None, - clean_archives: Boolean = false, - component_repository: String = Components.static_component_repository - ): Unit = { - val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) - for (path <- missing) { - Components.resolve(path.dir, path.file_name, - clean_platforms = clean_platforms, - clean_archives = clean_archives, - component_repository = component_repository, - ssh = ssh, - progress = if (echo) progress else new Progress) - } - } - - def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { - if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) - - val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") - val dummy_stty_remote = expand_path(dummy_stty) - if (!ssh.is_file(dummy_stty_remote)) { - ssh.make_directory(dummy_stty_remote.dir) - ssh.write_file(dummy_stty_remote, dummy_stty) - ssh.set_executable(dummy_stty_remote) - } - try { - bash( - "export PATH=\"" + bash_path(dummy_stty_remote.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) } - } - - - /* settings */ - - def clean_settings(): Boolean = - if (!ssh.is_file(etc_settings)) true - else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { - ssh.delete(etc_settings) - true - } - else false - - def init_settings(settings: List[String]): Unit = { - if (clean_settings()) { - ssh.make_directory(etc_settings.dir) - ssh.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) - } - - - /* init */ - - def init( - other_settings: List[String] = init_components(), - fresh: Boolean = false, - echo: Boolean = false, - clean_platforms: Option[List[Platform.Family.Value]] = None, - clean_archives: Boolean = false, - component_repository: String = Components.static_component_repository - ): Unit = { - init_settings(other_settings) - resolve_components( - echo = echo, - clean_platforms = clean_platforms, - clean_archives = clean_archives, - component_repository = component_repository) - scala_build(fresh = fresh, echo = echo) - } - - - /* cleanup */ - - def cleanup(): Unit = { - clean_settings() - ssh.delete(etc) - ssh.delete(isabelle_home_user) - } -} diff -r 406d34a8a67a -r a4dee214dfcf src/Pure/System/other_isabelle.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/other_isabelle.scala Thu Jul 20 12:11:34 2023 +0200 @@ -0,0 +1,176 @@ +/* Title: Pure/System/other_isabelle.scala + Author: Makarius + +Manage other Isabelle distributions: support historic versions starting from +tag "build_history_base". +*/ + +package isabelle + + +object Other_Isabelle { + def apply( + root: Path, + isabelle_identifier: String = "", + ssh: SSH.System = SSH.Local, + progress: Progress = new Progress + ): Other_Isabelle = { + val (isabelle_home, url_prefix) = + ssh match { + case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) + case _ => + if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { + error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") + } + (root.canonical, "") + } + val isabelle_home_url = url_prefix + isabelle_home.implode + new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) + } +} + +final class Other_Isabelle private( + val isabelle_home: Path, + val isabelle_identifier: String, + isabelle_home_url: String, + ssh: SSH.System, + progress: Progress +) { + override def toString: String = isabelle_home_url + + + /* static system */ + + def bash( + script: String, + redirect: Boolean = false, + echo: Boolean = false, + strict: Boolean = true + ): Process_Result = { + ssh.execute( + Isabelle_System.export_isabelle_identifier(isabelle_identifier) + + "cd " + ssh.bash_path(isabelle_home) + "\n" + script, + progress_stdout = progress.echo_if(echo, _), + progress_stderr = progress.echo_if(echo, _), + redirect = redirect, + settings = false, + strict = strict) + } + + 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") + + + /* components */ + + def init_components( + components_base: String = Components.dynamic_components_base, + catalogs: List[String] = Components.default_catalogs, + components: List[String] = Nil + ): List[String] = { + val admin = Components.admin(Path.ISABELLE_HOME).implode + + catalogs.map(name => + "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: + components.map(name => + "init_component " + quote(components_base) + "/" + name) + } + + def resolve_components( + echo: Boolean = false, + clean_platforms: Option[List[Platform.Family.Value]] = None, + clean_archives: Boolean = false, + component_repository: String = Components.static_component_repository + ): Unit = { + val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) + for (path <- missing) { + Components.resolve(path.dir, path.file_name, + clean_platforms = clean_platforms, + clean_archives = clean_archives, + component_repository = component_repository, + ssh = ssh, + progress = if (echo) progress else new Progress) + } + } + + def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { + if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) + + val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") + val dummy_stty_remote = expand_path(dummy_stty) + if (!ssh.is_file(dummy_stty_remote)) { + ssh.make_directory(dummy_stty_remote.dir) + ssh.write_file(dummy_stty_remote, dummy_stty) + ssh.set_executable(dummy_stty_remote) + } + try { + bash( + "export PATH=\"" + bash_path(dummy_stty_remote.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) } + } + + + /* settings */ + + def clean_settings(): Boolean = + if (!ssh.is_file(etc_settings)) true + else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { + ssh.delete(etc_settings) + true + } + else false + + def init_settings(settings: List[String]): Unit = { + if (clean_settings()) { + ssh.make_directory(etc_settings.dir) + ssh.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) + } + + + /* init */ + + def init( + other_settings: List[String] = init_components(), + fresh: Boolean = false, + echo: Boolean = false, + clean_platforms: Option[List[Platform.Family.Value]] = None, + clean_archives: Boolean = false, + component_repository: String = Components.static_component_repository + ): Unit = { + init_settings(other_settings) + resolve_components( + echo = echo, + clean_platforms = clean_platforms, + clean_archives = clean_archives, + component_repository = component_repository) + scala_build(fresh = fresh, echo = echo) + } + + + /* cleanup */ + + def cleanup(): Unit = { + clean_settings() + ssh.delete(etc) + ssh.delete(isabelle_home_user) + } +}