author | wenzelm |
Wed, 27 Mar 2024 12:50:37 +0100 | |
changeset 80021 | ba06861e91f9 |
parent 79681 | df1059ea8846 |
child 80023 | c43a51fde4f5 |
permissions | -rw-r--r-- |
78415
a4dee214dfcf
clarified file location: to be used by regular Isabelle/Scala tools;
wenzelm
parents:
78158
diff
changeset
|
1 |
/* Title: Pure/System/other_isabelle.scala |
64188 | 2 |
Author: Makarius |
3 |
||
77082 | 4 |
Manage other Isabelle distributions: support historic versions starting from |
5 |
tag "build_history_base". |
|
64188 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
75393 | 11 |
object Other_Isabelle { |
77050 | 12 |
def apply( |
77093 | 13 |
root: Path, |
77050 | 14 |
isabelle_identifier: String = "", |
77093 | 15 |
ssh: SSH.System = SSH.Local, |
77050 | 16 |
progress: Progress = new Progress |
17 |
): Other_Isabelle = { |
|
77093 | 18 |
val (isabelle_home, url_prefix) = |
19 |
ssh match { |
|
20 |
case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) |
|
21 |
case _ => |
|
22 |
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { |
|
23 |
error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") |
|
24 |
} |
|
25 |
(root.canonical, "") |
|
26 |
} |
|
27 |
val isabelle_home_url = url_prefix + isabelle_home.implode |
|
28 |
new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) |
|
77050 | 29 |
} |
67045 | 30 |
} |
31 |
||
77041 | 32 |
final class Other_Isabelle private( |
67045 | 33 |
val isabelle_home: Path, |
34 |
val isabelle_identifier: String, |
|
77093 | 35 |
isabelle_home_url: String, |
36 |
ssh: SSH.System, |
|
75393 | 37 |
progress: Progress |
38 |
) { |
|
80021
ba06861e91f9
proper services for Setup_Tool --- avoid hardwired stuff;
wenzelm
parents:
79681
diff
changeset
|
39 |
other_isabelle => |
ba06861e91f9
proper services for Setup_Tool --- avoid hardwired stuff;
wenzelm
parents:
79681
diff
changeset
|
40 |
|
77093 | 41 |
override def toString: String = isabelle_home_url |
67046 | 42 |
|
64188 | 43 |
|
44 |
/* static system */ |
|
45 |
||
65930 | 46 |
def bash( |
77042 | 47 |
script: String, |
48 |
redirect: Boolean = false, |
|
49 |
echo: Boolean = false, |
|
50 |
strict: Boolean = true |
|
51 |
): Process_Result = { |
|
79633 | 52 |
val env = |
53 |
Isabelle_System.export_env( |
|
54 |
user_home = ssh.user_home, |
|
55 |
isabelle_identifier = isabelle_identifier) |
|
56 |
ssh.execute(env + "cd " + ssh.bash_path(isabelle_home) + "\n" + script, |
|
77093 | 57 |
progress_stdout = progress.echo_if(echo, _), |
58 |
progress_stderr = progress.echo_if(echo, _), |
|
59 |
redirect = redirect, |
|
60 |
settings = false, |
|
61 |
strict = strict) |
|
77042 | 62 |
} |
64188 | 63 |
|
69166 | 64 |
def getenv(name: String): String = |
77071 | 65 |
bash("bin/isabelle getenv -b " + Bash.string(name)).check.out |
69166 | 66 |
|
77080
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
67 |
val settings: Isabelle_System.Settings = (name: String) => getenv(name) |
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
68 |
|
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
69 |
def expand_path(path: Path): Path = path.expand_env(settings) |
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
70 |
def bash_path(path: Path): String = Bash.string(expand_path(path).implode) |
64188 | 71 |
|
77085
351eee493580
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
wenzelm
parents:
77082
diff
changeset
|
72 |
val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER")) |
77080
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
73 |
|
77085
351eee493580
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
wenzelm
parents:
77082
diff
changeset
|
74 |
def etc: Path = isabelle_home_user + Path.explode("etc") |
77080
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
75 |
def etc_settings: Path = etc + Path.explode("settings") |
7e11e96a922d
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
wenzelm
parents:
77078
diff
changeset
|
76 |
def etc_preferences: Path = etc + Path.explode("preferences") |
64188 | 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( |
|
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77124
diff
changeset
|
82 |
components_base: String = Components.dynamic_components_base, |
77055 | 83 |
catalogs: List[String] = Components.default_catalogs, |
75393 | 84 |
components: List[String] = Nil |
85 |
): List[String] = { |
|
77088
6e2c6ccc5dc0
clarified defaults: imitate "isabelle components -I" without further parameters;
wenzelm
parents:
77087
diff
changeset
|
86 |
val admin = Components.admin(Path.ISABELLE_HOME).implode |
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
|
87 |
|
77090 | 88 |
catalogs.map(name => |
89 |
"init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: |
|
90 |
components.map(name => |
|
91 |
"init_component " + quote(components_base) + "/" + name) |
|
69388 | 92 |
} |
93 |
||
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
94 |
def resolve_components( |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
95 |
echo: Boolean = false, |
78610 | 96 |
clean_platforms: Option[List[Platform.Family]] = None, |
77124
be90af1e3254
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
wenzelm
parents:
77123
diff
changeset
|
97 |
clean_archives: Boolean = false, |
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77124
diff
changeset
|
98 |
component_repository: String = Components.static_component_repository |
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
99 |
): Unit = { |
77093 | 100 |
val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) |
101 |
for (path <- missing) { |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
102 |
Components.resolve(path.dir, path.file_name, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
103 |
clean_platforms = clean_platforms, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
104 |
clean_archives = clean_archives, |
77124
be90af1e3254
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
wenzelm
parents:
77123
diff
changeset
|
105 |
component_repository = component_repository, |
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
106 |
ssh = ssh, |
77093 | 107 |
progress = if (echo) progress else new Progress) |
108 |
} |
|
109 |
} |
|
110 |
||
77094 | 111 |
def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { |
112 |
if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) |
|
113 |
||
114 |
val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") |
|
115 |
val dummy_stty_remote = expand_path(dummy_stty) |
|
116 |
if (!ssh.is_file(dummy_stty_remote)) { |
|
117 |
ssh.make_directory(dummy_stty_remote.dir) |
|
118 |
ssh.write_file(dummy_stty_remote, dummy_stty) |
|
78158 | 119 |
ssh.set_executable(dummy_stty_remote) |
77094 | 120 |
} |
121 |
try { |
|
122 |
bash( |
|
123 |
"export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" + |
|
124 |
"export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" + |
|
125 |
"bin/isabelle jedit -b", echo = echo).check |
|
126 |
} |
|
127 |
catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) } |
|
128 |
} |
|
129 |
||
69388 | 130 |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
131 |
/* settings */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
132 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
133 |
def clean_settings(): Boolean = |
77093 | 134 |
if (!ssh.is_file(etc_settings)) true |
135 |
else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { |
|
136 |
ssh.delete(etc_settings) |
|
77042 | 137 |
true |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
138 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
139 |
else false |
64188 | 140 |
|
75393 | 141 |
def init_settings(settings: List[String]): Unit = { |
77078 | 142 |
if (clean_settings()) { |
77093 | 143 |
ssh.make_directory(etc_settings.dir) |
144 |
ssh.write(etc_settings, |
|
77078 | 145 |
"# generated by Isabelle " + Date.now() + "\n" + |
146 |
"#-*- shell-script -*- :mode=shellscript:\n" + |
|
147 |
settings.mkString("\n", "\n", "\n")) |
|
77042 | 148 |
} |
77078 | 149 |
else error("Cannot proceed with existing user settings file: " + etc_settings) |
64188 | 150 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
151 |
|
79681
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
152 |
def debug_settings(): List[String] = { |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
153 |
val debug = System.getProperty("isabelle.debug", "") == "true" |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
154 |
if (debug) { |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
155 |
List("ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.debug=true\"") |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
156 |
} |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
157 |
else Nil |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
158 |
} |
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79633
diff
changeset
|
159 |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
160 |
|
77123 | 161 |
/* init */ |
162 |
||
77095 | 163 |
def init( |
164 |
other_settings: List[String] = init_components(), |
|
165 |
fresh: Boolean = false, |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
166 |
echo: Boolean = false, |
78610 | 167 |
clean_platforms: Option[List[Platform.Family]] = None, |
77124
be90af1e3254
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
wenzelm
parents:
77123
diff
changeset
|
168 |
clean_archives: Boolean = false, |
77128
f40c36ab154d
clarified names to emphasize suble differences in meaning;
wenzelm
parents:
77124
diff
changeset
|
169 |
component_repository: String = Components.static_component_repository |
77095 | 170 |
): Unit = { |
171 |
init_settings(other_settings) |
|
77097
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
172 |
resolve_components( |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
173 |
echo = echo, |
023273cf2651
clean components more accurately: purge other platforms or archives;
wenzelm
parents:
77095
diff
changeset
|
174 |
clean_platforms = clean_platforms, |
77124
be90af1e3254
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
wenzelm
parents:
77123
diff
changeset
|
175 |
clean_archives = clean_archives, |
be90af1e3254
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
wenzelm
parents:
77123
diff
changeset
|
176 |
component_repository = component_repository) |
77095 | 177 |
scala_build(fresh = fresh, echo = echo) |
80021
ba06861e91f9
proper services for Setup_Tool --- avoid hardwired stuff;
wenzelm
parents:
79681
diff
changeset
|
178 |
Setup_Tool.init(other_isabelle) |
77095 | 179 |
} |
180 |
||
181 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
182 |
/* cleanup */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
183 |
|
75393 | 184 |
def cleanup(): Unit = { |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
185 |
clean_settings() |
77093 | 186 |
ssh.delete(etc) |
187 |
ssh.delete(isabelle_home_user) |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
188 |
} |
64188 | 189 |
} |