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