author | wenzelm |
Sat, 17 Jul 2021 13:42:21 +0200 | |
changeset 74029 | 0701ff55780d |
parent 74028 | 77cc23b550e9 |
child 74030 | 39e05601faeb |
permissions | -rw-r--r-- |
73944 | 1 |
/* Title: Tools/Setup/isabelle/setup/Build.java |
73914 | 2 |
Author: Makarius |
3 |
||
73954 | 4 |
Build Isabelle/Scala/Java modules. |
73914 | 5 |
*/ |
6 |
||
7 |
package isabelle.setup; |
|
8 |
||
9 |
||
73922 | 10 |
import java.io.BufferedOutputStream; |
74021 | 11 |
import java.io.ByteArrayInputStream; |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
12 |
import java.io.ByteArrayOutputStream; |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
13 |
import java.io.CharArrayWriter; |
73914 | 14 |
import java.io.File; |
15 |
import java.io.IOException; |
|
74021 | 16 |
import java.io.InputStream; |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
17 |
import java.io.PrintStream; |
73914 | 18 |
import java.math.BigInteger; |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
19 |
import java.nio.charset.StandardCharsets; |
73914 | 20 |
import java.nio.file.Files; |
21 |
import java.nio.file.Path; |
|
73918 | 22 |
import java.nio.file.StandardCopyOption; |
73914 | 23 |
import java.security.MessageDigest; |
24 |
import java.security.NoSuchAlgorithmException; |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
25 |
import java.util.ArrayList; |
73914 | 26 |
import java.util.Comparator; |
27 |
import java.util.LinkedList; |
|
28 |
import java.util.List; |
|
73919 | 29 |
import java.util.Locale; |
73914 | 30 |
import java.util.Properties; |
73967 | 31 |
import java.util.TreeMap; |
73922 | 32 |
import java.util.jar.Attributes; |
33 |
import java.util.jar.JarEntry; |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
34 |
import java.util.jar.JarFile; |
73922 | 35 |
import java.util.jar.JarOutputStream; |
36 |
import java.util.jar.Manifest; |
|
73914 | 37 |
import java.util.stream.Stream; |
38 |
||
73954 | 39 |
import javax.tools.JavaCompiler; |
40 |
import javax.tools.JavaFileObject; |
|
41 |
import javax.tools.StandardJavaFileManager; |
|
42 |
import javax.tools.ToolProvider; |
|
43 |
||
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
44 |
import scala.tools.nsc.MainClass; |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
45 |
|
73914 | 46 |
|
73944 | 47 |
public class Build |
73914 | 48 |
{ |
73951 | 49 |
/** context **/ |
50 |
||
51 |
public static String BUILD_PROPS = "build.props"; |
|
73961 | 52 |
public static String COMPONENT_BUILD_PROPS = "etc/build.props"; |
73951 | 53 |
|
54 |
public static Context directory_context(Path dir) |
|
55 |
throws IOException |
|
56 |
{ |
|
57 |
Properties props = new Properties(); |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
58 |
Path props_path = dir.resolve(BUILD_PROPS); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
59 |
props.load(Files.newBufferedReader(props_path)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
60 |
return new Context(dir, props, props_path.toString()); |
73951 | 61 |
} |
62 |
||
63 |
public static Context component_context(Path dir) |
|
64 |
throws IOException |
|
65 |
{ |
|
66 |
Properties props = new Properties(); |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
67 |
Path props_path = dir.resolve(COMPONENT_BUILD_PROPS); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
68 |
if (Files.exists(props_path)) { props.load(Files.newBufferedReader(props_path)); } |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
69 |
return new Context(dir, props, props_path.toString()); |
73951 | 70 |
} |
73922 | 71 |
|
73961 | 72 |
public static List<Context> component_contexts() |
73 |
throws IOException, InterruptedException |
|
74 |
{ |
|
75 |
List<Context> result = new LinkedList<Context>(); |
|
76 |
for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) { |
|
77 |
if (!p.isEmpty()) { |
|
78 |
Path dir = Path.of(Environment.platform_path(p)); |
|
79 |
if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) { |
|
80 |
result.add(component_context(dir)); |
|
81 |
} |
|
82 |
} |
|
83 |
} |
|
84 |
return List.copyOf(result); |
|
85 |
} |
|
86 |
||
73967 | 87 |
private static String sha_digest(MessageDigest sha, String name) |
88 |
{ |
|
89 |
String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); |
|
90 |
return digest + " " + name + "\n"; |
|
91 |
} |
|
92 |
||
73914 | 93 |
public static class Context |
94 |
{ |
|
73951 | 95 |
private final Path _dir; |
96 |
private final Properties _props; |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
97 |
private final String _location; |
73914 | 98 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
99 |
public Context(Path dir, Properties props, String location) |
73914 | 100 |
{ |
73951 | 101 |
_dir = dir; |
102 |
_props = props; |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
103 |
_location = location; |
73914 | 104 |
} |
105 |
||
73951 | 106 |
@Override public String toString() { return _dir.toString(); } |
73914 | 107 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
108 |
public String error_message(String msg) |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
109 |
{ |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
110 |
if (_location == null || _location.isEmpty()) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
111 |
return msg; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
112 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
113 |
else { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
114 |
return msg +" (in " + Library.quote(_location) + ")"; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
115 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
116 |
} |
73915 | 117 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
118 |
public String title() { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
119 |
String title = _props.getProperty("title", ""); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
120 |
if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); } |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
121 |
else return title; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
122 |
} |
73915 | 123 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
124 |
public String module() { return _props.getProperty("module", ""); } |
73954 | 125 |
public String scalac_options() { return _props.getProperty("scalac_options", ""); } |
126 |
public String javac_options() { return _props.getProperty("javac_options", ""); } |
|
73951 | 127 |
public String main() { return _props.getProperty("main", ""); } |
73914 | 128 |
|
73931 | 129 |
private List<String> get_list(String name) |
130 |
{ |
|
131 |
List<String> list = new LinkedList<String>(); |
|
73951 | 132 |
for (String s : _props.getProperty(name, "").split("\\s+")) { |
73931 | 133 |
if (!s.isEmpty()) { list.add(s); } |
134 |
} |
|
135 |
return List.copyOf(list); |
|
136 |
} |
|
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
137 |
public List<String> requirements() { return get_list("requirements"); } |
73931 | 138 |
public List<String> sources() { return get_list("sources"); } |
139 |
public List<String> resources() { return get_list("resources"); } |
|
140 |
public List<String> services() { return get_list("services"); } |
|
73914 | 141 |
|
73965 | 142 |
public boolean is_vacuous() |
143 |
{ |
|
144 |
return sources().isEmpty() && resources().isEmpty() && services().isEmpty(); |
|
145 |
} |
|
146 |
||
73957
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
147 |
public Path path(String file) |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
148 |
throws IOException, InterruptedException |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
149 |
{ |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
150 |
return _dir.resolve(Environment.expand_platform_path(file)); |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
151 |
} |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
152 |
public boolean exists(String file) |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
153 |
throws IOException, InterruptedException |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
154 |
{ |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
155 |
return Files.exists(path(file)); |
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
156 |
} |
73914 | 157 |
|
73921 | 158 |
public String item_name(String s) |
73918 | 159 |
{ |
160 |
int i = s.indexOf(':'); |
|
161 |
return i > 0 ? s.substring(0, i) : s; |
|
162 |
} |
|
163 |
||
73921 | 164 |
public String item_target(String s) |
73918 | 165 |
{ |
166 |
int i = s.indexOf(':'); |
|
167 |
return i > 0 ? s.substring(i + 1) : s; |
|
168 |
} |
|
169 |
||
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
170 |
public String shasum(String name, List<Path> paths) |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
171 |
throws IOException, NoSuchAlgorithmException |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
172 |
{ |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
173 |
MessageDigest sha = MessageDigest.getInstance("SHA"); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
174 |
for (Path file : paths) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
175 |
if (Files.exists(file)) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
176 |
sha.update(Files.readAllBytes(file)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
177 |
} |
73966 | 178 |
else { |
179 |
throw new RuntimeException( |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
180 |
error_message("Missing input file " + Library.quote(file.toString()))); |
73966 | 181 |
} |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
182 |
} |
73967 | 183 |
return sha_digest(sha, name); |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
184 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
185 |
|
73914 | 186 |
public String shasum(String file) |
73957
110a027a5473
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
wenzelm
parents:
73955
diff
changeset
|
187 |
throws IOException, NoSuchAlgorithmException, InterruptedException |
73914 | 188 |
{ |
73966 | 189 |
return shasum(file, List.of(path(file))); |
73914 | 190 |
} |
73967 | 191 |
|
192 |
public String shasum_props() |
|
193 |
throws NoSuchAlgorithmException |
|
194 |
{ |
|
195 |
TreeMap<String,Object> sorted = new TreeMap<String,Object>(); |
|
196 |
for (Object x : _props.entrySet()) { |
|
197 |
sorted.put(x.toString(), _props.get(x)); |
|
198 |
} |
|
199 |
MessageDigest sha = MessageDigest.getInstance("SHA"); |
|
200 |
sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)); |
|
201 |
return sha_digest(sha, "<props>"); |
|
202 |
} |
|
73914 | 203 |
} |
204 |
||
73922 | 205 |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
206 |
/** compile sources **/ |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
207 |
|
73954 | 208 |
private static void add_options(List<String> options_list, String options) |
209 |
{ |
|
210 |
if (options != null) { |
|
211 |
for (String s : options.split("\\s+")) { |
|
212 |
if (!s.isEmpty()) { options_list.add(s); } |
|
213 |
} |
|
214 |
} |
|
215 |
} |
|
216 |
||
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
217 |
private static void compiler_result(boolean ok, String out, String what) |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
218 |
{ |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
219 |
if (ok) { if (!out.isEmpty()) { System.err.println(out); } } |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
220 |
else { |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
221 |
String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
222 |
throw new RuntimeException(msg); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
223 |
} |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
224 |
} |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
225 |
|
73954 | 226 |
public static void compile_scala_sources( |
227 |
Path target_dir, String more_options, List<Path> deps, List<Path> sources) |
|
228 |
throws IOException, InterruptedException |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
229 |
{ |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
230 |
ArrayList<String> args = new ArrayList<String>(); |
73954 | 231 |
add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS")); |
232 |
add_options(args, more_options); |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
233 |
args.add("-d"); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
234 |
args.add(target_dir.toString()); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
235 |
args.add("-bootclasspath"); |
73960 | 236 |
args.add(Environment.join_platform_paths(deps)); |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
237 |
args.add("--"); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
238 |
|
73955 | 239 |
boolean scala_sources = false; |
240 |
for (Path p : sources) { |
|
241 |
args.add(p.toString()); |
|
242 |
if (p.toString().endsWith(".scala")) { scala_sources = true; } |
|
243 |
} |
|
244 |
if (scala_sources) { |
|
74021 | 245 |
InputStream in_orig = System.in; |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
246 |
PrintStream out_orig = System.out; |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
247 |
PrintStream err_orig = System.err; |
74021 | 248 |
ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]); |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
249 |
ByteArrayOutputStream out = new ByteArrayOutputStream(); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
250 |
|
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
251 |
// Single-threaded context! |
74028 | 252 |
boolean ok = false; |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
253 |
try { |
74022 | 254 |
PrintStream out_stream = new PrintStream(out); |
74021 | 255 |
System.setIn(in); |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
256 |
System.setOut(out_stream); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
257 |
System.setErr(out_stream); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
258 |
ok = new MainClass().process(args.toArray(String[]::new)); |
74022 | 259 |
out_stream.flush(); |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
260 |
} |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
261 |
finally { |
74021 | 262 |
System.setIn(in_orig); |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
263 |
System.setOut(out_orig); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
264 |
System.setErr(err_orig); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
265 |
} |
74020 | 266 |
compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources"); |
73955 | 267 |
} |
73954 | 268 |
} |
269 |
||
270 |
public static void compile_java_sources( |
|
271 |
Path target_dir, String more_options, List<Path> deps, List<Path> sources) |
|
272 |
throws IOException, InterruptedException |
|
273 |
{ |
|
274 |
JavaCompiler compiler = ToolProvider.getSystemJavaCompiler(); |
|
275 |
StandardJavaFileManager file_manager = |
|
276 |
compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8); |
|
277 |
||
278 |
List<String> options = new LinkedList<String>(); |
|
279 |
add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS")); |
|
280 |
add_options(options, more_options); |
|
281 |
options.add("-d"); |
|
282 |
options.add(target_dir.toString()); |
|
283 |
options.add("-classpath"); |
|
73960 | 284 |
options.add(Environment.join_platform_paths(deps)); |
73954 | 285 |
|
286 |
List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>(); |
|
287 |
for (Path p : sources) { |
|
288 |
if (p.toString().endsWith(".java")) { |
|
289 |
for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) { |
|
290 |
java_sources.add(o); |
|
291 |
} |
|
292 |
} |
|
293 |
} |
|
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
294 |
|
73954 | 295 |
if (!java_sources.isEmpty()) { |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
296 |
CharArrayWriter out = new CharArrayWriter(); |
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
297 |
boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call(); |
74025 | 298 |
out.flush(); |
74018
9d6c9a55f450
more informative errors: capture low-level compiler output;
wenzelm
parents:
73987
diff
changeset
|
299 |
compiler_result(ok, out.toString(), "Java sources"); |
73954 | 300 |
} |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
301 |
} |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
302 |
|
73922 | 303 |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
304 |
/** shasum for jar content **/ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
305 |
|
73965 | 306 |
private static String SHASUM = "META-INF/isabelle/shasum"; |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
307 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
308 |
public static String get_shasum(Path jar_path) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
309 |
throws IOException |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
310 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
311 |
if (Files.exists(jar_path)) { |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
312 |
try (JarFile jar_file = new JarFile(jar_path.toFile())) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
313 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
314 |
JarEntry entry = jar_file.getJarEntry(SHASUM); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
315 |
if (entry != null) { |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
316 |
byte[] bytes = jar_file.getInputStream(entry).readAllBytes(); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
317 |
return new String(bytes, StandardCharsets.UTF_8); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
318 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
319 |
else { return ""; } |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
320 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
321 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
322 |
else { return ""; } |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
323 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
324 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
325 |
public static void create_shasum(Path dir, String shasum) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
326 |
throws IOException |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
327 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
328 |
Path path = dir.resolve(SHASUM); |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
329 |
Files.createDirectories(path.getParent()); |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
330 |
Files.writeString(path, shasum); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
331 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
332 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
333 |
|
73965 | 334 |
/** services **/ |
335 |
||
336 |
private static String SERVICES = "META-INF/isabelle/services"; |
|
337 |
||
338 |
public static List<String> get_services(Path jar_path) |
|
339 |
throws IOException |
|
340 |
{ |
|
341 |
if (Files.exists(jar_path)) { |
|
342 |
try (JarFile jar_file = new JarFile(jar_path.toFile())) |
|
343 |
{ |
|
344 |
JarEntry entry = jar_file.getJarEntry(SERVICES); |
|
345 |
if (entry != null) { |
|
346 |
byte[] bytes = jar_file.getInputStream(entry).readAllBytes(); |
|
347 |
return Library.split_lines(new String(bytes, StandardCharsets.UTF_8)); |
|
348 |
} |
|
349 |
else { return List.of(); } |
|
350 |
} |
|
351 |
} |
|
352 |
else { return List.of(); } |
|
353 |
} |
|
354 |
||
355 |
public static void create_services(Path dir, List<String> services) |
|
356 |
throws IOException |
|
357 |
{ |
|
358 |
if (!services.isEmpty()) { |
|
359 |
Path path = dir.resolve(SERVICES); |
|
360 |
Files.createDirectories(path.getParent()); |
|
361 |
Files.writeString(path, Library.cat_lines(services)); |
|
362 |
} |
|
363 |
} |
|
364 |
||
365 |
||
73922 | 366 |
/** create jar **/ |
367 |
||
368 |
public static void create_jar(Path dir, String main, Path jar) |
|
369 |
throws IOException |
|
370 |
{ |
|
73949 | 371 |
Files.createDirectories(dir.resolve(jar).getParent()); |
73922 | 372 |
Files.deleteIfExists(jar); |
373 |
||
374 |
Manifest manifest = new Manifest(); |
|
375 |
Attributes attributes = manifest.getMainAttributes(); |
|
376 |
attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0"); |
|
377 |
attributes.put(new Attributes.Name("Created-By"), |
|
378 |
System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")"); |
|
379 |
if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); } |
|
380 |
||
381 |
try (JarOutputStream out = |
|
382 |
new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest)) |
|
383 |
{ |
|
384 |
for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) { |
|
385 |
boolean is_dir = Files.isDirectory(path); |
|
386 |
boolean is_file = Files.isRegularFile(path); |
|
387 |
if (is_dir || is_file) { |
|
388 |
String name = Environment.slashes(dir.relativize(path).toString()); |
|
73950 | 389 |
if (!name.isEmpty()) { |
390 |
JarEntry entry = new JarEntry(is_dir ? name + "/" : name); |
|
391 |
entry.setTime(path.toFile().lastModified()); |
|
392 |
out.putNextEntry(entry); |
|
393 |
if (is_file) { out.write(Files.readAllBytes(path)); } |
|
394 |
out.closeEntry(); |
|
395 |
} |
|
73922 | 396 |
} |
397 |
} |
|
398 |
} |
|
399 |
} |
|
400 |
||
401 |
||
73961 | 402 |
/** classpath **/ |
403 |
||
404 |
public static List<Path> classpath() |
|
405 |
throws IOException, InterruptedException |
|
406 |
{ |
|
407 |
List<Path> result = new LinkedList<Path>(); |
|
408 |
for (Context context : component_contexts()) { |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
409 |
String module = context.module(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
410 |
if (!module.isEmpty()) { result.add(context.path(module)); } |
73961 | 411 |
} |
412 |
return List.copyOf(result); |
|
413 |
} |
|
414 |
||
415 |
public static List<String> services() |
|
416 |
throws IOException, InterruptedException |
|
417 |
{ |
|
418 |
List<String> result = new LinkedList<String>(); |
|
419 |
for (Context context : component_contexts()) { |
|
420 |
for (String s : context.services()) { |
|
421 |
result.add(s); |
|
422 |
} |
|
423 |
} |
|
424 |
return List.copyOf(result); |
|
425 |
} |
|
426 |
||
427 |
||
73954 | 428 |
/** build **/ |
73922 | 429 |
|
73954 | 430 |
public static void build(Context context, boolean fresh) |
73914 | 431 |
throws IOException, InterruptedException, NoSuchAlgorithmException |
432 |
{ |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
433 |
String module = context.module(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
434 |
if (!module.isEmpty()) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
435 |
String title = context.title(); |
73914 | 436 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
437 |
Path jar_path = context.path(module); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
438 |
String jar_name = jar_path.toString(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
439 |
if (!jar_name.endsWith(".jar")) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
440 |
throw new RuntimeException( |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
441 |
context.error_message("Bad jar module " + Library.quote(jar_name))); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
442 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
443 |
|
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
444 |
if (context.is_vacuous()) { Files.deleteIfExists(jar_path); } |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
445 |
else { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
446 |
List<String> requirements = context.requirements(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
447 |
List<String> resources = context.resources(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
448 |
List<String> sources = context.sources(); |
73914 | 449 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
450 |
String shasum_old = get_shasum(jar_path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
451 |
String shasum; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
452 |
List<Path> compiler_deps = new LinkedList<Path>(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
453 |
{ |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
454 |
StringBuilder _shasum = new StringBuilder(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
455 |
_shasum.append(context.shasum_props()); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
456 |
for (String s : requirements) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
457 |
if (s.startsWith("env:")) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
458 |
List<Path> paths = new LinkedList<Path>(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
459 |
for (String p : Environment.getenv(s.substring(4)).split(":", -1)) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
460 |
if (!p.isEmpty()) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
461 |
Path path = Path.of(Environment.platform_path(p)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
462 |
compiler_deps.add(path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
463 |
paths.add(path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
464 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
465 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
466 |
_shasum.append(context.shasum(s, paths)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
467 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
468 |
else { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
469 |
compiler_deps.add(context.path(s)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
470 |
_shasum.append(context.shasum(s)); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
471 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
472 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
473 |
for (String s : resources) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
474 |
_shasum.append(context.shasum(context.item_name(s))); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
475 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
476 |
for (String s : sources) { _shasum.append(context.shasum(s)); } |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
477 |
shasum = _shasum.toString(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
478 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
479 |
if (fresh || !shasum_old.equals(shasum)) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
480 |
System.out.print("### Building " + title + " (" + jar_path + ") ...\n"); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
481 |
|
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
482 |
String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH"); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
483 |
|
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
484 |
Path build_dir = Files.createTempDirectory("isabelle"); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
485 |
try { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
486 |
/* compile sources */ |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
487 |
|
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
488 |
for (String s : isabelle_classpath.split(":", -1)) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
489 |
if (!s.isEmpty()) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
490 |
compiler_deps.add(Path.of(Environment.platform_path(s))); |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
491 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
492 |
} |
73914 | 493 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
494 |
List<Path> compiler_sources = new LinkedList<Path>(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
495 |
for (String s : sources) { compiler_sources.add(context.path(s)); } |
73914 | 496 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
497 |
compile_scala_sources( |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
498 |
build_dir, context.scalac_options(), compiler_deps, compiler_sources); |
73914 | 499 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
500 |
compiler_deps.add(build_dir); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
501 |
compile_java_sources( |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
502 |
build_dir, context.javac_options(), compiler_deps, compiler_sources); |
73914 | 503 |
|
504 |
||
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
505 |
/* copy resources */ |
73918 | 506 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
507 |
for (String s : context.resources()) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
508 |
String name = context.item_name(s); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
509 |
String target = context.item_target(s); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
510 |
Path file_name = Path.of(name).normalize().getFileName(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
511 |
Path target_path = Path.of(target).normalize(); |
73918 | 512 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
513 |
Path target_dir; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
514 |
Path target_file; |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
515 |
{ |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
516 |
if (target.endsWith("/") || target.endsWith("/.")) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
517 |
target_dir = build_dir.resolve(target_path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
518 |
target_file = target_dir.resolve(file_name); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
519 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
520 |
else { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
521 |
target_file = build_dir.resolve(target_path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
522 |
target_dir = target_file.getParent(); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
523 |
} |
73918 | 524 |
} |
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
525 |
Files.createDirectories(target_dir); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
526 |
Files.copy(context.path(name), target_file, |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
527 |
StandardCopyOption.COPY_ATTRIBUTES); |
73918 | 528 |
} |
529 |
||
530 |
||
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
531 |
/* packaging */ |
73914 | 532 |
|
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
533 |
create_shasum(build_dir, shasum); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
534 |
create_services(build_dir, context.services()); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
535 |
create_jar(build_dir, context.main(), jar_path); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
536 |
} |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
537 |
finally { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
538 |
try (Stream<Path> walk = Files.walk(build_dir)) { |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
539 |
walk.sorted(Comparator.reverseOrder()) |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
540 |
.map(Path::toFile) |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
541 |
.forEach(File::delete); |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74028
diff
changeset
|
542 |
} |
73914 | 543 |
} |
544 |
} |
|
545 |
} |
|
546 |
} |
|
547 |
} |
|
73961 | 548 |
|
549 |
public static void build_components(boolean fresh) |
|
550 |
throws IOException, InterruptedException, NoSuchAlgorithmException |
|
551 |
{ |
|
552 |
for (Context context : component_contexts()) { |
|
553 |
build(context, fresh); |
|
554 |
} |
|
555 |
} |
|
73914 | 556 |
} |