author | wenzelm |
Tue, 24 Jan 2023 15:16:24 +0100 | |
changeset 77072 | e8010cb36820 |
parent 77071 | 7a89ef6b0276 |
child 77073 | 7b65209fdfe8 |
permissions | -rw-r--r-- |
64188 | 1 |
/* Title: Pure/Admin/other_isabelle.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Manage other Isabelle distributions. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object Other_Isabelle { |
77050 | 11 |
def apply( |
12 |
isabelle_home: Path, |
|
13 |
isabelle_identifier: String = "", |
|
14 |
user_home: Path = Path.USER_HOME, |
|
15 |
progress: Progress = new Progress |
|
16 |
): Other_Isabelle = { |
|
69408
fb26935838c7
more robust, notably for macos /var vs. /private/var;
wenzelm
parents:
69404
diff
changeset
|
17 |
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) |
77050 | 18 |
} |
67045 | 19 |
} |
20 |
||
77041 | 21 |
final class Other_Isabelle private( |
67045 | 22 |
val isabelle_home: Path, |
23 |
val isabelle_identifier: String, |
|
67046 | 24 |
user_home: Path, |
75393 | 25 |
progress: Progress |
26 |
) { |
|
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
27 |
override def toString: String = isabelle_home.toString |
67046 | 28 |
|
77042 | 29 |
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { |
67046 | 30 |
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") |
77042 | 31 |
} |
67046 | 32 |
|
64188 | 33 |
|
34 |
/* static system */ |
|
35 |
||
65930 | 36 |
def bash( |
77042 | 37 |
script: String, |
38 |
redirect: Boolean = false, |
|
39 |
echo: Boolean = false, |
|
40 |
strict: Boolean = true |
|
41 |
): Process_Result = { |
|
67046 | 42 |
progress.bash( |
43 |
"export USER_HOME=" + File.bash_path(user_home) + "\n" + |
|
44 |
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, |
|
65930 | 45 |
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) |
77042 | 46 |
} |
64188 | 47 |
|
69166 | 48 |
def getenv(name: String): String = |
77071 | 49 |
bash("bin/isabelle getenv -b " + Bash.string(name)).check.out |
69166 | 50 |
|
51 |
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER")) |
|
64188 | 52 |
|
68754 | 53 |
val etc: Path = isabelle_home_user + Path.explode("etc") |
54 |
val etc_settings: Path = etc + Path.explode("settings") |
|
55 |
val etc_preferences: Path = etc + Path.explode("preferences") |
|
64188 | 56 |
|
77071 | 57 |
def resolve_components(echo: Boolean = false): Unit = { |
77069
348f4d95d110
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
wenzelm
parents:
77055
diff
changeset
|
58 |
val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) |
348f4d95d110
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
wenzelm
parents:
77055
diff
changeset
|
59 |
for (path <- missing) { |
77071 | 60 |
Components.resolve(path.dir, path.file_name, |
61 |
progress = if (echo) progress else new Progress) |
|
77069
348f4d95d110
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
wenzelm
parents:
77055
diff
changeset
|
62 |
} |
348f4d95d110
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
wenzelm
parents:
77055
diff
changeset
|
63 |
} |
348f4d95d110
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
wenzelm
parents:
77055
diff
changeset
|
64 |
|
77072
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
65 |
def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
66 |
if (fresh) { |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
67 |
Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes")) |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
68 |
} |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
69 |
try { |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
70 |
bash( |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
71 |
"export PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty")) + ":$PATH\"\n" + |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
72 |
"export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" + |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
73 |
"bin/isabelle jedit -b", echo = echo).check |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
74 |
} |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
75 |
catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) } |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
76 |
} |
e8010cb36820
more robust and uniform Other_Isabelle.scala_build;
wenzelm
parents:
77071
diff
changeset
|
77 |
|
73625
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
78 |
|
69388 | 79 |
/* components */ |
80 |
||
81 |
def init_components( |
|
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
82 |
component_repository: String = Components.default_component_repository, |
69434 | 83 |
components_base: Path = Components.default_components_base, |
77055 | 84 |
catalogs: List[String] = Components.default_catalogs, |
75393 | 85 |
components: List[String] = Nil |
86 |
): List[String] = { |
|
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
87 |
val dir = Components.admin(isabelle_home) |
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
88 |
|
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
89 |
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) :: |
69396 | 90 |
catalogs.map(name => |
69434 | 91 |
"init_components " + File.bash_path(components_base) + " " + |
92 |
File.bash_path(dir + Path.basic(name))) ::: |
|
69396 | 93 |
components.map(name => |
69434 | 94 |
"init_component " + File.bash_path(components_base + Path.basic(name))) |
69388 | 95 |
} |
96 |
||
97 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
98 |
/* settings */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
99 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
100 |
def clean_settings(): Boolean = |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
101 |
if (!etc_settings.is_file) true |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
102 |
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { |
77042 | 103 |
etc_settings.file.delete |
104 |
true |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
105 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
106 |
else false |
64188 | 107 |
|
75393 | 108 |
def init_settings(settings: List[String]): Unit = { |
77042 | 109 |
if (!clean_settings()) { |
64188 | 110 |
error("Cannot proceed with existing user settings file: " + etc_settings) |
77042 | 111 |
} |
64188 | 112 |
|
72375 | 113 |
Isabelle_System.make_directory(etc_settings.dir) |
64188 | 114 |
File.write(etc_settings, |
115 |
"# generated by Isabelle " + Date.now() + "\n" + |
|
69388 | 116 |
"#-*- shell-script -*- :mode=shellscript:\n" + |
117 |
settings.mkString("\n", "\n", "\n")) |
|
64188 | 118 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
119 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
120 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
121 |
/* cleanup */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
122 |
|
75393 | 123 |
def cleanup(): Unit = { |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
124 |
clean_settings() |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
125 |
etc.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
126 |
isabelle_home_user.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
127 |
} |
64188 | 128 |
} |