--- 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 \
--- 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)
- }
-}
--- /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)
+ }
+}