author | wenzelm |
Fri, 09 Jul 2021 14:43:41 +0200 | |
changeset 73954 | a3a64aab815a |
parent 73952 | 74ab1fb470a3 |
child 73955 | 2b9ae1aa9257 |
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; |
73914 | 11 |
import java.io.File; |
12 |
import java.io.IOException; |
|
13 |
import java.math.BigInteger; |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
14 |
import java.nio.charset.StandardCharsets; |
73914 | 15 |
import java.nio.file.Files; |
16 |
import java.nio.file.Path; |
|
73918 | 17 |
import java.nio.file.StandardCopyOption; |
73914 | 18 |
import java.security.MessageDigest; |
19 |
import java.security.NoSuchAlgorithmException; |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
20 |
import java.util.ArrayList; |
73914 | 21 |
import java.util.Comparator; |
22 |
import java.util.LinkedList; |
|
23 |
import java.util.List; |
|
73919 | 24 |
import java.util.Locale; |
73914 | 25 |
import java.util.Properties; |
73922 | 26 |
import java.util.jar.Attributes; |
27 |
import java.util.jar.JarEntry; |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
28 |
import java.util.jar.JarFile; |
73922 | 29 |
import java.util.jar.JarOutputStream; |
30 |
import java.util.jar.Manifest; |
|
73914 | 31 |
import java.util.stream.Stream; |
32 |
||
73954 | 33 |
import javax.tools.JavaCompiler; |
34 |
import javax.tools.JavaFileObject; |
|
35 |
import javax.tools.StandardJavaFileManager; |
|
36 |
import javax.tools.ToolProvider; |
|
37 |
||
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
38 |
import scala.tools.nsc.MainClass; |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
39 |
|
73914 | 40 |
|
73944 | 41 |
public class Build |
73914 | 42 |
{ |
73951 | 43 |
/** context **/ |
44 |
||
45 |
public static String BUILD_PROPS = "build.props"; |
|
46 |
||
47 |
public static Context directory_context(Path dir) |
|
48 |
throws IOException |
|
49 |
{ |
|
50 |
Properties props = new Properties(); |
|
51 |
props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS))); |
|
52 |
return new Context(dir, props); |
|
53 |
} |
|
54 |
||
55 |
public static Context component_context(Path dir) |
|
56 |
throws IOException |
|
57 |
{ |
|
58 |
Properties props = new Properties(); |
|
59 |
Path build_props = dir.resolve("etc").resolve(BUILD_PROPS); |
|
60 |
if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); } |
|
61 |
return new Context(dir, props); |
|
62 |
} |
|
73922 | 63 |
|
73914 | 64 |
public static class Context |
65 |
{ |
|
73951 | 66 |
private final Path _dir; |
67 |
private final Properties _props; |
|
73914 | 68 |
|
73951 | 69 |
public Context(Path dir, Properties props) |
73914 | 70 |
{ |
73951 | 71 |
_dir = dir; |
72 |
_props = props; |
|
73914 | 73 |
} |
74 |
||
73951 | 75 |
@Override public String toString() { return _dir.toString(); } |
73914 | 76 |
|
73951 | 77 |
public String name() { return _props.getProperty("name", _dir.toFile().getName()); } |
78 |
public String description() { return _props.getProperty("description", name()); } |
|
73915 | 79 |
|
73951 | 80 |
public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); } |
73917 | 81 |
public String jar_name() { return lib_name() + ".jar"; } |
73915 | 82 |
|
73954 | 83 |
public String scalac_options() { return _props.getProperty("scalac_options", ""); } |
84 |
public String javac_options() { return _props.getProperty("javac_options", ""); } |
|
85 |
||
73951 | 86 |
public String main() { return _props.getProperty("main", ""); } |
73914 | 87 |
|
73931 | 88 |
private List<String> get_list(String name) |
89 |
{ |
|
90 |
List<String> list = new LinkedList<String>(); |
|
73951 | 91 |
for (String s : _props.getProperty(name, "").split("\\s+")) { |
73931 | 92 |
if (!s.isEmpty()) { list.add(s); } |
93 |
} |
|
94 |
return List.copyOf(list); |
|
95 |
} |
|
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
96 |
public List<String> requirements() { return get_list("requirements"); } |
73931 | 97 |
public List<String> sources() { return get_list("sources"); } |
98 |
public List<String> resources() { return get_list("resources"); } |
|
99 |
public List<String> services() { return get_list("services"); } |
|
73914 | 100 |
|
73951 | 101 |
public Path path(String file) { return _dir.resolve(file); } |
73917 | 102 |
public boolean exists(String file) { return Files.exists(path(file)); } |
73914 | 103 |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
104 |
// historic |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
105 |
public Path shasum_path() { return path(lib_name() + ".shasum"); } |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
106 |
|
73921 | 107 |
public String item_name(String s) |
73918 | 108 |
{ |
109 |
int i = s.indexOf(':'); |
|
110 |
return i > 0 ? s.substring(0, i) : s; |
|
111 |
} |
|
112 |
||
73921 | 113 |
public String item_target(String s) |
73918 | 114 |
{ |
115 |
int i = s.indexOf(':'); |
|
116 |
return i > 0 ? s.substring(i + 1) : s; |
|
117 |
} |
|
118 |
||
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
119 |
public String shasum(String name, List<Path> paths) |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
120 |
throws IOException, NoSuchAlgorithmException |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
121 |
{ |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
122 |
boolean exists = false; |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
123 |
MessageDigest sha = MessageDigest.getInstance("SHA"); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
124 |
for (Path file : paths) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
125 |
if (Files.exists(file)) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
126 |
exists = true; |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
127 |
sha.update(Files.readAllBytes(file)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
128 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
129 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
130 |
if (exists) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
131 |
String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
132 |
return digest + " " + name + "\n"; |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
133 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
134 |
else { return ""; } |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
135 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
136 |
|
73914 | 137 |
public String shasum(String file) |
138 |
throws IOException, NoSuchAlgorithmException |
|
139 |
{ |
|
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
140 |
return shasum(file, List.of(path(file))); |
73914 | 141 |
} |
142 |
} |
|
143 |
||
73922 | 144 |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
145 |
/** compile sources **/ |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
146 |
|
73954 | 147 |
private static void add_options(List<String> options_list, String options) |
148 |
{ |
|
149 |
if (options != null) { |
|
150 |
for (String s : options.split("\\s+")) { |
|
151 |
if (!s.isEmpty()) { options_list.add(s); } |
|
152 |
} |
|
153 |
} |
|
154 |
} |
|
155 |
||
156 |
public static void compile_scala_sources( |
|
157 |
Path target_dir, String more_options, List<Path> deps, List<Path> sources) |
|
158 |
throws IOException, InterruptedException |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
159 |
{ |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
160 |
ArrayList<String> args = new ArrayList<String>(); |
73954 | 161 |
add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS")); |
162 |
add_options(args, more_options); |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
163 |
args.add("-d"); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
164 |
args.add(target_dir.toString()); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
165 |
args.add("-bootclasspath"); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
166 |
args.add(Environment.join_paths(deps)); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
167 |
args.add("--"); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
168 |
for (Path p : sources) { args.add(p.toString()); } |
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 |
MainClass main = new MainClass(); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
171 |
boolean ok = main.process(args.toArray(String[]::new)); |
73954 | 172 |
if (!ok) throw new RuntimeException("Failed to compile Scala sources"); |
173 |
} |
|
174 |
||
175 |
public static void compile_java_sources( |
|
176 |
Path target_dir, String more_options, List<Path> deps, List<Path> sources) |
|
177 |
throws IOException, InterruptedException |
|
178 |
{ |
|
179 |
JavaCompiler compiler = ToolProvider.getSystemJavaCompiler(); |
|
180 |
StandardJavaFileManager file_manager = |
|
181 |
compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8); |
|
182 |
||
183 |
List<String> options = new LinkedList<String>(); |
|
184 |
add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS")); |
|
185 |
add_options(options, more_options); |
|
186 |
options.add("-d"); |
|
187 |
options.add(target_dir.toString()); |
|
188 |
options.add("-classpath"); |
|
189 |
options.add(Environment.join_paths(deps)); |
|
190 |
||
191 |
List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>(); |
|
192 |
for (Path p : sources) { |
|
193 |
if (p.toString().endsWith(".java")) { |
|
194 |
for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) { |
|
195 |
java_sources.add(o); |
|
196 |
} |
|
197 |
} |
|
198 |
} |
|
199 |
if (!java_sources.isEmpty()) { |
|
200 |
boolean ok = compiler.getTask(null, file_manager, null, options, null, java_sources).call(); |
|
201 |
if (!ok) throw new RuntimeException("Failed to compile Java sources"); |
|
202 |
} |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
203 |
} |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
204 |
|
73922 | 205 |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
206 |
/** shasum for jar content **/ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
207 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
208 |
private static String SHASUM = "META-INF/shasum"; |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
209 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
210 |
public static String get_shasum(Path jar_path) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
211 |
throws IOException |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
212 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
213 |
if (Files.exists(jar_path)) { |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
214 |
try (JarFile jar_file = new JarFile(jar_path.toFile())) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
215 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
216 |
JarEntry entry = jar_file.getJarEntry(SHASUM); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
217 |
if (entry != null) { |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
218 |
byte[] bytes = jar_file.getInputStream(entry).readAllBytes(); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
219 |
return new String(bytes, StandardCharsets.UTF_8); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
220 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
221 |
else { return ""; } |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
222 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
223 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
224 |
else { return ""; } |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
225 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
226 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
227 |
public static void create_shasum(Path dir, String shasum) |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
228 |
throws IOException |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
229 |
{ |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
230 |
Path path = dir.resolve(SHASUM); |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
231 |
Files.createDirectories(path.getParent()); |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
232 |
Files.writeString(path, shasum); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
233 |
} |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
234 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
235 |
|
73922 | 236 |
/** create jar **/ |
237 |
||
238 |
public static void create_jar(Path dir, String main, Path jar) |
|
239 |
throws IOException |
|
240 |
{ |
|
73949 | 241 |
Files.createDirectories(dir.resolve(jar).getParent()); |
73922 | 242 |
Files.deleteIfExists(jar); |
243 |
||
244 |
Manifest manifest = new Manifest(); |
|
245 |
Attributes attributes = manifest.getMainAttributes(); |
|
246 |
attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0"); |
|
247 |
attributes.put(new Attributes.Name("Created-By"), |
|
248 |
System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")"); |
|
249 |
if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); } |
|
250 |
||
251 |
try (JarOutputStream out = |
|
252 |
new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest)) |
|
253 |
{ |
|
254 |
for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) { |
|
255 |
boolean is_dir = Files.isDirectory(path); |
|
256 |
boolean is_file = Files.isRegularFile(path); |
|
257 |
if (is_dir || is_file) { |
|
258 |
String name = Environment.slashes(dir.relativize(path).toString()); |
|
73950 | 259 |
if (!name.isEmpty()) { |
260 |
JarEntry entry = new JarEntry(is_dir ? name + "/" : name); |
|
261 |
entry.setTime(path.toFile().lastModified()); |
|
262 |
out.putNextEntry(entry); |
|
263 |
if (is_file) { out.write(Files.readAllBytes(path)); } |
|
264 |
out.closeEntry(); |
|
265 |
} |
|
73922 | 266 |
} |
267 |
} |
|
268 |
} |
|
269 |
} |
|
270 |
||
271 |
||
73954 | 272 |
/** build **/ |
73922 | 273 |
|
73954 | 274 |
public static void build(Context context, boolean fresh) |
73914 | 275 |
throws IOException, InterruptedException, NoSuchAlgorithmException |
276 |
{ |
|
73915 | 277 |
String jar_name = context.jar_name(); |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
278 |
Path jar_path = context.path(jar_name); |
73914 | 279 |
|
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
280 |
List<String> requirements = context.requirements(); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
281 |
List<String> resources = context.resources(); |
73931 | 282 |
List<String> sources = context.sources(); |
73914 | 283 |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
284 |
Files.deleteIfExists(context.shasum_path()); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
285 |
|
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
286 |
if (sources.isEmpty() && resources.isEmpty()) { |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
287 |
Files.deleteIfExists(jar_path); |
73914 | 288 |
} |
289 |
else { |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
290 |
String shasum_old = get_shasum(jar_path); |
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
291 |
String shasum; |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
292 |
List<Path> compiler_deps = new LinkedList<Path>(); |
73914 | 293 |
{ |
294 |
StringBuilder _shasum = new StringBuilder(); |
|
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
295 |
for (String s : requirements) { |
73952 | 296 |
if (s.startsWith("env:")) { |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
297 |
List<Path> paths = new LinkedList<Path>(); |
73952 | 298 |
for (String p : Environment.getenv(s.substring(4)).split(":", -1)) { |
73948
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
299 |
if (!p.isEmpty()) { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
300 |
Path path = Path.of(Environment.platform_path(p)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
301 |
compiler_deps.add(path); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
302 |
paths.add(path); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
303 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
304 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
305 |
_shasum.append(context.shasum(s, paths)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
306 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
307 |
else { |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
308 |
compiler_deps.add(context.path(s)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
309 |
_shasum.append(context.shasum(s)); |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
310 |
} |
731ab64bae97
more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents:
73946
diff
changeset
|
311 |
} |
73918 | 312 |
for (String s : resources) { |
73921 | 313 |
_shasum.append(context.shasum(context.item_name(s))); |
73918 | 314 |
} |
73920 | 315 |
for (String s : sources) { _shasum.append(context.shasum(s)); } |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
316 |
shasum = _shasum.toString(); |
73914 | 317 |
} |
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
318 |
if (fresh || !shasum_old.equals(shasum)) { |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
319 |
System.out.println( |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
320 |
"### Building " + context.description() + " (" + jar_path + ") ..."); |
73914 | 321 |
|
322 |
String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH"); |
|
323 |
||
324 |
Path build_dir = Files.createTempDirectory("isabelle"); |
|
325 |
try { |
|
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
326 |
/* compile sources */ |
73914 | 327 |
|
328 |
for (String s : isabelle_class_path.split(":", -1)) { |
|
73931 | 329 |
if (!s.isEmpty()) { |
330 |
compiler_deps.add(Path.of(Environment.platform_path(s))); |
|
331 |
} |
|
73914 | 332 |
} |
333 |
||
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
334 |
List<Path> compiler_sources = new LinkedList<Path>(); |
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
335 |
for (String s : sources) { compiler_sources.add(context.path(s)); } |
73914 | 336 |
|
73954 | 337 |
compile_scala_sources( |
338 |
build_dir, context.scalac_options(), compiler_deps, compiler_sources); |
|
339 |
||
340 |
compiler_deps.add(build_dir); |
|
341 |
compile_java_sources( |
|
342 |
build_dir, context.javac_options(), compiler_deps, compiler_sources); |
|
73914 | 343 |
|
344 |
||
73918 | 345 |
/* copy resources */ |
346 |
||
347 |
for (String s : context.resources()) { |
|
73921 | 348 |
String name = context.item_name(s); |
349 |
String target = context.item_target(s); |
|
73918 | 350 |
Path file_name = Path.of(name).normalize().getFileName(); |
351 |
Path target_path = Path.of(target).normalize(); |
|
352 |
||
353 |
Path target_dir; |
|
354 |
Path target_file; |
|
355 |
{ |
|
356 |
if (target.endsWith("/") || target.endsWith("/.")) { |
|
357 |
target_dir = build_dir.resolve(target_path); |
|
358 |
target_file = target_dir.resolve(file_name); |
|
359 |
} |
|
360 |
else { |
|
361 |
target_file = build_dir.resolve(target_path); |
|
362 |
target_dir = target_file.getParent(); |
|
363 |
} |
|
364 |
} |
|
365 |
Files.createDirectories(target_dir); |
|
366 |
Files.copy(context.path(name), target_file, |
|
367 |
StandardCopyOption.COPY_ATTRIBUTES); |
|
368 |
} |
|
369 |
||
370 |
||
73922 | 371 |
/* packaging */ |
73914 | 372 |
|
73946
4d4c806cb7c8
clarified shasum: sources / resources within jar;
wenzelm
parents:
73944
diff
changeset
|
373 |
create_shasum(build_dir, shasum); |
73930
17c09d1b3588
invoke Scala compiler from Java, without external process;
wenzelm
parents:
73922
diff
changeset
|
374 |
create_jar(build_dir, context.main(), jar_path); |
73914 | 375 |
} |
376 |
finally { |
|
377 |
try (Stream<Path> walk = Files.walk(build_dir)) { |
|
378 |
walk.sorted(Comparator.reverseOrder()) |
|
379 |
.map(Path::toFile) |
|
380 |
.forEach(File::delete); |
|
381 |
} |
|
382 |
} |
|
383 |
} |
|
384 |
} |
|
385 |
} |
|
386 |
} |