author | wenzelm |
Sat, 17 Jul 2021 13:42:21 +0200 | |
changeset 74029 | 0701ff55780d |
parent 73963 | 59b6f0462086 |
permissions | -rw-r--r-- |
73963 | 1 |
/* Title: Tools/Setup/isabelle/setup/Environment.scala |
73906 | 2 |
Author: Makarius |
3 |
||
4 |
Fundamental Isabelle system environment: quasi-static module with |
|
5 |
optional init operation. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle.setup; |
|
9 |
||
10 |
import java.io.File; |
|
11 |
import java.io.IOException; |
|
12 |
import java.nio.file.Files; |
|
13 |
import java.nio.file.Path; |
|
14 |
import java.util.HashMap; |
|
15 |
import java.util.LinkedList; |
|
16 |
import java.util.List; |
|
17 |
import java.util.Locale; |
|
18 |
import java.util.Map; |
|
19 |
import java.util.function.BiFunction; |
|
20 |
import java.util.regex.Matcher; |
|
21 |
import java.util.regex.Pattern; |
|
22 |
||
23 |
||
24 |
public class Environment |
|
25 |
{ |
|
26 |
/** Support for Cygwin as POSIX emulation on Windows **/ |
|
27 |
||
28 |
public static Boolean is_windows() |
|
29 |
{ |
|
30 |
return System.getProperty("os.name", "").startsWith("Windows"); |
|
31 |
} |
|
32 |
||
33 |
||
34 |
||
35 |
/* system path representations */ |
|
36 |
||
73922 | 37 |
public static String slashes(String s) { return s.replace('\\', '/'); } |
73906 | 38 |
|
39 |
public static String standard_path(String cygwin_root, String platform_path) |
|
40 |
{ |
|
41 |
if (is_windows()) { |
|
42 |
String backslashes = platform_path.replace('/', '\\'); |
|
43 |
||
44 |
Pattern root_pattern = |
|
45 |
Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)"); |
|
46 |
Matcher root_matcher = root_pattern.matcher(backslashes); |
|
47 |
||
48 |
Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)"); |
|
49 |
Matcher drive_matcher = drive_pattern.matcher(backslashes); |
|
50 |
||
51 |
if (root_matcher.matches()) { |
|
52 |
String rest = root_matcher.group(1); |
|
53 |
return "/" + slashes(rest); |
|
54 |
} |
|
55 |
else if (drive_matcher.matches()) { |
|
56 |
String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT); |
|
57 |
String rest = drive_matcher.group(2); |
|
58 |
return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest)); |
|
59 |
} |
|
60 |
else { return slashes(backslashes); } |
|
61 |
} |
|
62 |
else { return platform_path; } |
|
63 |
} |
|
64 |
||
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
65 |
private static class Expand_Platform_Path |
73906 | 66 |
{ |
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
67 |
private String _cygwin_root; |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
68 |
private StringBuilder _result = new StringBuilder(); |
73906 | 69 |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
70 |
public Expand_Platform_Path(String cygwin_root) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
71 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
72 |
_cygwin_root = cygwin_root; |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
73 |
} |
73906 | 74 |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
75 |
public String result() { return _result.toString(); } |
73906 | 76 |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
77 |
void clear() { _result.setLength(0); } |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
78 |
void add(char c) { _result.append(c); } |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
79 |
void add(String s) { _result.append(s); } |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
80 |
void separator() |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
81 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
82 |
int n = _result.length(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
83 |
if (n > 0 && _result.charAt(n - 1) != File.separatorChar) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
84 |
add(File.separatorChar); |
73906 | 85 |
} |
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
86 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
87 |
|
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
88 |
public String check_root(String standard_path) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
89 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
90 |
String rest = standard_path; |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
91 |
boolean is_root = standard_path.startsWith("/"); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
92 |
|
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
93 |
if (is_windows()) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
94 |
Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)"); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
95 |
Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
96 |
|
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
97 |
Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)"); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
98 |
Matcher named_root_matcher = named_root_pattern.matcher(standard_path); |
73906 | 99 |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
100 |
if (cygdrive_matcher.matches()) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
101 |
String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
102 |
rest = cygdrive_matcher.group(2); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
103 |
clear(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
104 |
add(drive); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
105 |
add(':'); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
106 |
add(File.separatorChar); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
107 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
108 |
else if (named_root_matcher.matches()) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
109 |
String root = named_root_matcher.group(1); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
110 |
rest = named_root_matcher.group(2); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
111 |
clear(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
112 |
add(File.separatorChar); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
113 |
add(File.separatorChar); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
114 |
add(root); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
115 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
116 |
else if (is_root) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
117 |
clear(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
118 |
add(_cygwin_root); |
73906 | 119 |
} |
120 |
} |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
121 |
else if (is_root) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
122 |
clear(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
123 |
add(File.separatorChar); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
124 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
125 |
return rest; |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
126 |
} |
73906 | 127 |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
128 |
public void check_rest(Map<String,String> env, String main) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
129 |
throws IOException, InterruptedException |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
130 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
131 |
for (String p : main.split("/", -1)) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
132 |
if (env != null && p.startsWith("$")) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
133 |
String var = p.substring(1); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
134 |
String res = env.getOrDefault(var, ""); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
135 |
if (res.isEmpty()) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
136 |
throw new RuntimeException( |
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
73963
diff
changeset
|
137 |
"Bad Isabelle environment variable: " + Library.quote(var)); |
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
138 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
139 |
else check(null, res); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
140 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
141 |
else if (!p.isEmpty()) { |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
142 |
separator(); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
143 |
add(p); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
144 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
145 |
} |
73906 | 146 |
} |
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
147 |
|
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
148 |
public void check(Map<String,String> env, String path) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
149 |
throws IOException, InterruptedException |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
150 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
151 |
check_rest(env, check_root(path)); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
152 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
153 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
154 |
|
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
155 |
public static String expand_platform_path( |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
156 |
Map<String,String> env, String cygwin_root, String standard_path) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
157 |
throws IOException, InterruptedException |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
158 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
159 |
Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
160 |
expand.check(env, standard_path); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
161 |
return expand.result(); |
73906 | 162 |
} |
163 |
||
73960 | 164 |
public static String join_platform_paths(List<Path> paths) |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
165 |
{ |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
166 |
List<String> strs = new LinkedList<String>(); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
167 |
for (Path p : paths) { strs.add(p.toString()); } |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
168 |
return String.join(File.pathSeparator, strs); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
169 |
} |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
170 |
|
73960 | 171 |
public static String join_standard_paths(List<Path> paths) |
172 |
throws IOException, InterruptedException |
|
173 |
{ |
|
174 |
List<String> strs = new LinkedList<String>(); |
|
175 |
for (Path p : paths) { strs.add(standard_path(p.toString())); } |
|
176 |
return String.join(":", strs); |
|
177 |
} |
|
178 |
||
73906 | 179 |
|
180 |
/* raw process */ |
|
181 |
||
182 |
public static ProcessBuilder process_builder( |
|
183 |
List<String> cmd, File cwd, Map<String,String> env, boolean redirect) |
|
184 |
{ |
|
185 |
ProcessBuilder builder = new ProcessBuilder(); |
|
186 |
||
187 |
// fragile on Windows: |
|
188 |
// see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 |
|
189 |
builder.command(cmd); |
|
190 |
||
191 |
if (cwd != null) builder.directory(cwd); |
|
192 |
if (env != null) { |
|
193 |
builder.environment().clear(); |
|
194 |
builder.environment().putAll(env); |
|
195 |
} |
|
196 |
builder.redirectErrorStream(redirect); |
|
197 |
||
198 |
return builder; |
|
199 |
} |
|
200 |
||
201 |
public static class Exec_Result |
|
202 |
{ |
|
203 |
private final int _rc; |
|
204 |
private final String _out; |
|
205 |
private final String _err; |
|
206 |
||
207 |
Exec_Result(int rc, String out, String err) |
|
208 |
{ |
|
209 |
_rc = rc; |
|
73963 | 210 |
_out = Library.trim_line(out); |
211 |
_err = Library.trim_line(err); |
|
73906 | 212 |
} |
213 |
||
214 |
public int rc() { return _rc; } |
|
215 |
public boolean ok() { return _rc == 0; } |
|
216 |
public String out() { return _out; } |
|
217 |
public String err() { return _err; } |
|
218 |
} |
|
219 |
||
220 |
public static Exec_Result exec_process( |
|
221 |
List<String> command_line, |
|
222 |
File cwd, |
|
223 |
Map<String,String> env, |
|
224 |
boolean redirect) throws IOException, InterruptedException |
|
225 |
{ |
|
226 |
Path out_file = Files.createTempFile(null, null); |
|
227 |
Path err_file = Files.createTempFile(null, null); |
|
228 |
Exec_Result res; |
|
229 |
try { |
|
230 |
ProcessBuilder builder = process_builder(command_line, cwd, env, redirect); |
|
231 |
builder.redirectOutput(out_file.toFile()); |
|
232 |
builder.redirectError(err_file.toFile()); |
|
233 |
||
234 |
Process proc = builder.start(); |
|
235 |
proc.getOutputStream().close(); |
|
236 |
try { proc.waitFor(); } |
|
237 |
finally { |
|
238 |
proc.getInputStream().close(); |
|
239 |
proc.getErrorStream().close(); |
|
240 |
proc.destroy(); |
|
241 |
Thread.interrupted(); |
|
242 |
} |
|
243 |
||
244 |
int rc = proc.exitValue(); |
|
245 |
String out = Files.readString(out_file); |
|
246 |
String err = Files.readString(err_file); |
|
247 |
res = new Exec_Result(rc, out, err); |
|
248 |
} |
|
249 |
finally { |
|
250 |
Files.deleteIfExists(out_file); |
|
251 |
Files.deleteIfExists(err_file); |
|
252 |
} |
|
253 |
return res; |
|
254 |
} |
|
255 |
||
256 |
||
257 |
/* init (e.g. after extraction via 7zip) */ |
|
258 |
||
259 |
private static String bootstrap_directory( |
|
260 |
String preference, String variable, String property, String description) |
|
261 |
{ |
|
262 |
String a = preference; // explicit argument |
|
263 |
String b = System.getenv(variable); // e.g. inherited from running isabelle tool |
|
264 |
String c = System.getProperty(property); // e.g. via JVM application boot process |
|
265 |
String dir; |
|
266 |
||
267 |
if (a != null && !a.isEmpty()) { dir = a; } |
|
268 |
else if (b != null && !b.isEmpty()) { dir = b; } |
|
269 |
else if (c != null && !c.isEmpty()) { dir = c; } |
|
270 |
else { throw new RuntimeException("Unknown " + description + " directory"); } |
|
271 |
||
272 |
if ((new File(dir)).isDirectory()) { return dir; } |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
73963
diff
changeset
|
273 |
else { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
73963
diff
changeset
|
274 |
throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
73963
diff
changeset
|
275 |
} |
73906 | 276 |
} |
277 |
||
278 |
private static void cygwin_exec(String isabelle_root, List<String> cmd) |
|
279 |
throws IOException, InterruptedException |
|
280 |
{ |
|
281 |
File cwd = new File(isabelle_root); |
|
282 |
Map<String,String> env = new HashMap<String,String>(System.getenv()); |
|
283 |
env.put("CYGWIN", "nodosfilewarning"); |
|
284 |
Exec_Result res = exec_process(cmd, cwd, env, true); |
|
285 |
if (!res.ok()) throw new RuntimeException(res.out()); |
|
286 |
} |
|
287 |
||
288 |
public static void cygwin_link(String content, File target) throws IOException |
|
289 |
{ |
|
290 |
Path target_path = target.toPath(); |
|
291 |
Files.writeString(target_path, "!<symlink>" + content + "\u0000"); |
|
292 |
Files.setAttribute(target_path, "dos:system", true); |
|
293 |
} |
|
294 |
||
295 |
public static void cygwin_init(String isabelle_root, String cygwin_root) |
|
296 |
throws IOException, InterruptedException |
|
297 |
{ |
|
298 |
if (is_windows()) { |
|
299 |
File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized"); |
|
300 |
boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete(); |
|
301 |
||
302 |
if (uninitialized) { |
|
303 |
Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath(); |
|
304 |
String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]); |
|
305 |
||
306 |
// recover symlinks |
|
307 |
int i = 0; |
|
308 |
int m = symlinks.length; |
|
309 |
int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m; |
|
310 |
while (i < n) { |
|
311 |
if (i + 1 < n) { |
|
312 |
String target = symlinks[i]; |
|
313 |
String content = symlinks[i + 1]; |
|
314 |
cygwin_link(content, new File(isabelle_root, target)); |
|
315 |
i += 2; |
|
316 |
} else { throw new RuntimeException("Unbalanced symlinks list"); } |
|
317 |
} |
|
318 |
||
319 |
cygwin_exec(isabelle_root, |
|
320 |
List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")); |
|
321 |
cygwin_exec(isabelle_root, |
|
322 |
List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")); |
|
323 |
} |
|
324 |
} |
|
325 |
} |
|
326 |
||
327 |
||
328 |
/* implicit settings environment */ |
|
329 |
||
330 |
private static volatile Map<String,String> _settings = null; |
|
331 |
||
332 |
public static Map<String,String> settings() |
|
333 |
throws IOException, InterruptedException |
|
334 |
{ |
|
335 |
if (_settings == null) { init("", ""); } // unsynchronized check |
|
336 |
return _settings; |
|
337 |
} |
|
338 |
||
73913 | 339 |
public static String getenv(String name) |
340 |
throws IOException, InterruptedException |
|
341 |
{ |
|
342 |
return settings().getOrDefault(name, ""); |
|
343 |
} |
|
344 |
||
73906 | 345 |
public static synchronized void init(String _isabelle_root, String _cygwin_root) |
346 |
throws IOException, InterruptedException |
|
347 |
{ |
|
348 |
if (_settings == null) { |
|
349 |
String isabelle_root = |
|
350 |
bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root"); |
|
351 |
||
352 |
String cygwin_root = ""; |
|
353 |
if (is_windows()) { |
|
354 |
cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root"); |
|
355 |
cygwin_init(isabelle_root, cygwin_root); |
|
356 |
} |
|
357 |
||
358 |
Map<String,String> env = new HashMap<String,String>(System.getenv()); |
|
359 |
||
360 |
BiFunction<String,String,Void> env_default = |
|
361 |
(String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; }; |
|
362 |
||
363 |
String temp_windows = is_windows() ? System.getenv("TEMP") : null; |
|
364 |
||
365 |
env_default.apply("CYGWIN_ROOT", cygwin_root); |
|
366 |
env_default.apply("TEMP_WINDOWS", |
|
367 |
(temp_windows != null && temp_windows.contains("\\")) ? temp_windows : ""); |
|
368 |
env_default.apply("ISABELLE_JDK_HOME", |
|
369 |
standard_path(cygwin_root, System.getProperty("java.home", ""))); |
|
370 |
env_default.apply("HOME", System.getProperty("user.home", "")); |
|
371 |
env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", "")); |
|
372 |
||
373 |
Map<String,String> settings = new HashMap<String,String>(); |
|
374 |
Path settings_file = Files.createTempFile(null, null); |
|
375 |
try { |
|
376 |
List<String> cmd = new LinkedList<String>(); |
|
377 |
if (is_windows()) { |
|
378 |
cmd.add(cygwin_root + "\\bin\\bash"); |
|
379 |
cmd.add("-l"); |
|
380 |
cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle")); |
|
381 |
} else { |
|
382 |
cmd.add(isabelle_root + "/bin/isabelle"); |
|
383 |
} |
|
384 |
cmd.add("getenv"); |
|
385 |
cmd.add("-d"); |
|
386 |
cmd.add(settings_file.toString()); |
|
387 |
||
388 |
Exec_Result res = exec_process(cmd, null, env, true); |
|
389 |
if (!res.ok()) throw new RuntimeException(res.out()); |
|
390 |
||
391 |
for (String s : Files.readString(settings_file).split("\u0000", -1)) { |
|
392 |
int i = s.indexOf('='); |
|
393 |
if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); } |
|
394 |
else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); } |
|
395 |
} |
|
396 |
} |
|
397 |
finally { Files.delete(settings_file); } |
|
398 |
||
399 |
if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); } |
|
400 |
||
401 |
settings.put("PATH", settings.get("PATH_JVM")); |
|
402 |
settings.remove("PATH_JVM"); |
|
403 |
||
404 |
_settings = Map.copyOf(settings); |
|
405 |
} |
|
406 |
} |
|
73911 | 407 |
|
408 |
||
409 |
/* Cygwin root (after init) */ |
|
410 |
||
411 |
public static String cygwin_root() |
|
412 |
throws IOException, InterruptedException |
|
413 |
{ |
|
73913 | 414 |
return getenv("CYGWIN_ROOT"); |
73911 | 415 |
} |
416 |
||
417 |
public static String standard_path(String platform_path) |
|
418 |
throws IOException, InterruptedException |
|
419 |
{ |
|
420 |
return standard_path(cygwin_root(), platform_path); |
|
421 |
} |
|
422 |
||
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
423 |
public static String expand_platform_path(String standard_path) |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
424 |
throws IOException, InterruptedException |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
425 |
{ |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
426 |
return expand_platform_path(settings(), cygwin_root(), standard_path); |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
427 |
} |
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
428 |
|
73911 | 429 |
public static String platform_path(String standard_path) |
430 |
throws IOException, InterruptedException |
|
431 |
{ |
|
73956
ac1884965dc8
support expand_platform_path, which is reminiscent of isabelle.Path.expand;
wenzelm
parents:
73930
diff
changeset
|
432 |
return expand_platform_path(null, cygwin_root(), standard_path); |
73911 | 433 |
} |
434 |
||
435 |
||
436 |
/* kill process (via bash) */ |
|
437 |
||
438 |
static public boolean kill_process(String group_pid, String signal) |
|
439 |
throws IOException, InterruptedException |
|
440 |
{ |
|
441 |
List<String> cmd = new LinkedList<String>(); |
|
442 |
if (is_windows()) { |
|
443 |
cmd.add(cygwin_root() + "\\bin\\bash.exe"); |
|
444 |
} |
|
445 |
else { |
|
446 |
cmd.add("/usr/bin/env"); |
|
447 |
cmd.add("bash"); |
|
448 |
} |
|
449 |
cmd.add("-c"); |
|
450 |
cmd.add("kill -" + signal + " -" + group_pid); |
|
451 |
return exec_process(cmd, null, null, false).ok(); |
|
452 |
} |
|
73906 | 453 |
} |