Jar files, both library and executable, are now created as part of bu…

…ild on Java (#3355)

Fixes #2827

Adds the creation of a java jar file to the build step on a Java
platform.
- If there is a Main method, the jar is an executable jar. So a simple
A.dfy can be built as `dafny build -t:java A.dfy`
and then run as `java -jar A.jar`
- If there is no Main entry point, all the generated class files are
assembled into a library Jar file that can be used on the
classpath as a java library.
- In both cases, the DafnyRuntime library is included in the generated
jar
- The .java and .class artifacts are retained if --spill-translation is
true (not the default) or if the legacy CLI is being used (so as not to
break old workflows)
- The jar file is placed in the directory specified by --output (which
is the working directory by default)

Note that the --output option can specifies the _name_ of the output jar
file, as in Q.jar or zzz/Q.jar,
but it is not the name of the directory in which to put the jar file. In
java builds, the build artifacts are placed in
a directory whose location is the path and name of the jar file, without
'-jar' and with '-java'. (This behavior is unchanged)

Having a library or executable jar simplifies the user's task in
figuring out how to use the built artifacts.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <[email protected]>

Source/DafnyCore/Compilers/Compiler-java.cs

@@ -2344,27 +2344,87 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
         files.Add(Path.GetFullPath(file));
       }
 
-      var psi = PrepareProcessStartInfo("javac", new List<string> { "-encoding", "UTF8" }.Concat(files));
-      psi.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
-      psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename);
-      return 0 == RunProcess(psi, outputWriter, "Error while compiling Java files.");
+      // Compile the generated source to .class files, adding the output directory to the classpath
+      var compileProcess = PrepareProcessStartInfo("javac", new List<string> { "-encoding", "UTF8" }.Concat(files));
+      compileProcess.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
+      compileProcess.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename);
+      if (0 != RunProcess(compileProcess, outputWriter, "Error while compiling Java files.")) {
+        return false;
+      }
+
+      if (!DafnyOptions.O.UseRuntimeLib) {
+        // If the built-in runtime library is used, unpack it so it can be repacked into the final jar
+        var libUnpackProcess = PrepareProcessStartInfo("jar", new List<String> { "xf", "DafnyRuntime.jar" });
+        libUnpackProcess.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
+        if (0 != RunProcess(libUnpackProcess, outputWriter, "Error while creating jar file (unzipping runtime library).")) {
+          return false;
+        }
+      }
+
+      var classFiles = Directory.EnumerateFiles(targetDirectory, "*.class", SearchOption.AllDirectories)
+          .Select(file => Path.GetRelativePath(targetDirectory, file)).ToList();
+
+
+      var simpleProgramName = Path.GetFileNameWithoutExtension(targetFilename);
+      var jarPath = Path.GetFullPath(Path.ChangeExtension(dafnyProgramName, ".jar"));
+      if (!CreateJar(callToMain == null ? null : simpleProgramName,
+                     jarPath,
+                     Path.GetFullPath(Path.GetDirectoryName(targetFilename)),
+                     classFiles,
+                     outputWriter)) {
+        return false;
+      }
+
+      // Keep the build artifacts if --spill-translation is true
+      // But keep them for legacy CLI so as not to break old behavior
+      if (DafnyOptions.O.UsingNewCli) {
+        if (DafnyOptions.O.SpillTargetCode == 0) {
+          Directory.Delete(targetDirectory, true);
+        } else {
+          classFiles.ForEach(f => File.Delete(f));
+        }
+      }
+
+      if (DafnyOptions.O.CompileVerbose) {
+        // For the sake of tests, just write out the filename and not the directory path
+        var fileKind = callToMain != null ? "executable" : "library";
+        outputWriter.WriteLine($"Wrote {fileKind} jar {Path.GetFileName(jarPath)}");
+      }
+
+      return true;
+    }
+
+
+    public bool CreateJar(string/*?*/ entryPointName, string jarPath, string rootDirectory, List<string> files, TextWriter outputWriter) {
+      System.IO.Directory.CreateDirectory(Path.GetDirectoryName(jarPath));
+      var args = entryPointName == null ? // If null, then no entry point is added
+          new List<string> { "cf", jarPath }
+          : new List<string> { "cfe", jarPath, entryPointName };
+      var jarCreationProcess = PrepareProcessStartInfo("jar", args.Concat(files));
+      jarCreationProcess.WorkingDirectory = rootDirectory;
+      return 0 == RunProcess(jarCreationProcess, outputWriter, "Error while creating jar file: " + jarPath);
     }
 
     public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string /*?*/ targetFilename,
      ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
+      string jarPath = Path.ChangeExtension(dafnyProgramName, ".jar"); // Must match that in CompileTargetProgram
       var psi = PrepareProcessStartInfo("java",
-        new List<string> { "-Dfile.encoding=UTF-8", Path.GetFileNameWithoutExtension(targetFilename) }
+        new List<string> { "-Dfile.encoding=UTF-8", "-jar", jarPath }
           .Concat(DafnyOptions.O.MainArgs));
-      psi.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
-      psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename);
+      // Run the target program in the user's working directory and with the user's classpath
+      psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(null);
       return 0 == RunProcess(psi, outputWriter);
     }
 
     protected string GetClassPath(string targetFilename) {
-      var targetDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
       var classpath = Environment.GetEnvironmentVariable("CLASSPATH"); // String.join converts null to ""
       // Note that the items in the CLASSPATH must have absolute paths because the compilation is performed in a subfolder of where the command-line is executed
-      return string.Join(Path.PathSeparator, ".", targetDirectory, Path.Combine(targetDirectory, "DafnyRuntime.jar"), classpath);
+      if (targetFilename != null) {
+        var targetDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
+        return string.Join(Path.PathSeparator, ".", targetDirectory, Path.Combine(targetDirectory, "DafnyRuntime.jar"), classpath);
+      } else {
+        return classpath;
+      }
     }
 
     static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {

Source/DafnyCore/DafnyOptions.cs

@@ -239,6 +239,7 @@ public enum DiagnosticsFormats {
       JSON,
     }
 
+    public bool UsingNewCli = false;
     public bool UnicodeOutput = false;
     public DiagnosticsFormats DiagnosticsFormat = DiagnosticsFormats.PlainText;
     public bool DisallowSoundnessCheating = false;

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -90,6 +90,7 @@ public static ParseArgumentResult Create(string[] arguments) {
         return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR);
       }
     }
+    dafnyOptions.UsingNewCli = true;
 
     var rootCommand = new RootCommand("The Dafny CLI enables working with Dafny, a verification-aware programming language. Use 'dafny /help' to see help for a previous CLI format.");
     foreach (var command in commandToSpec.Keys) {

Test/.gitignore

@@ -17,6 +17,7 @@
 
 # Java output
 **/*-java
+**/*.jar
 
 # C++ output
 **/*.h

Test/comp/CompileWithArguments.dfy

@@ -17,11 +17,10 @@
 // RUN: %s.exe "cpp" 2 >> "%t"
 // RUN: %s.exe "cpp" 1 >> "%t"
 // RUN: %s.exe "cpp" "aloha" >> "%t"
-// RUN: %baredafny build %args --no-verify --target:java "%s" >> "%t"
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java %S/CompileWithArguments-java/CompileWithArguments.java %S/CompileWithArguments-java/*/*.java
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java 2 >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java 1 >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java aloha >> "%t"
+// RUN: %baredafny build %args --unicode-char --no-verify --target:java "%s" --output:"%s.jar" >> "%t"
+// RUN: java -jar "%s.jar" Java 2 >> "%t"
+// RUN: java -jar "%s.jar" Java 1 >> "%t"
+// RUN: java -jar "%s.jar" Java aloha >> "%t"
 // RUN: %baredafny build %args --no-verify --target:py "%s" >> "%t"
 // RUN: python3 %S/CompileWithArguments-py/CompileWithArguments.py Python 2 >> "%t"
 // RUN: python3 %S/CompileWithArguments-py/CompileWithArguments.py Python 1 >> "%t"

Test/comp/compile1verbose/CompileAndThenRun.dfy.expect

@@ -17,6 +17,7 @@ Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun-java/CompileAndThenRun.java
 Additional target code written to CompileAndThenRun-java/_System/nat.java
 Additional target code written to CompileAndThenRun-java/_System/__default.java
+Wrote executable jar CompileAndThenRun.jar
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors

Test/comp/compile3/JustRun.dfy.expect

@@ -21,6 +21,7 @@ Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun-java/JustRun.java
 Additional target code written to JustRun-java/_System/nat.java
 Additional target code written to JustRun-java/_System/__default.java
+Wrote executable jar JustRun.jar
 Running...
 
 hello, Dafny

Test/git-issues/git-issue-2827a/.gitignore

@@ -0,0 +1 @@
+A.jar

Test/git-issues/git-issue-2827a/A.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny build -t:java "%s" > "%t"
+// RUN: java -jar "%S/A.jar" >>  "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Hello, World!\n";
+}

Test/git-issues/git-issue-2827a/A.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Hello, World!

Test/git-issues/git-issue-2827b/.gitignore

@@ -0,0 +1 @@
+B.jar

Test/git-issues/git-issue-2827b/B.dfy

@@ -0,0 +1,8 @@
+// RUN: %baredafny build -t:java "%s" "%S"/org/D.java > "%t"
+// RUN: java -cp "%S"/B.jar org.D >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Fails on integration tests because the file org/D.java is not put in the right place.
+method m() {
+  print "Hello, World!\n";
+}

Test/git-issues/git-issue-2827b/B.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Hello, World!

Test/git-issues/git-issue-2827b/org/D.java

@@ -0,0 +1,7 @@
+package org;
+
+public class D {
+public static void main(String[] args) {
+  _System.__default.m();
+}
+}

Test/git-issues/git-issue-2827c/.gitignore

@@ -0,0 +1 @@
+A.jar

Test/git-issues/git-issue-2827c/A.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny build -t:java --output "%S/Q.jar" "%s" > "%t"
+// RUN: java -jar "%S/Q.jar" >>  "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Hello, World!\n";
+}

Test/git-issues/git-issue-2827c/A.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Hello, World!

Test/git-issues/git-issue-2827d/.gitignore

@@ -0,0 +1 @@
+A.jar

Test/git-issues/git-issue-2827d/A.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny build -t:java --output "%S/zzz/Q.jar" "%s" > "%t"
+// RUN: java -jar "%S/zzz/Q.jar" >>  "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Hello, World!\n";
+}

Test/git-issues/git-issue-2827d/A.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Hello, World!

Test/lit.site.cfg

@@ -99,7 +99,7 @@ binaryDir = os.path.join(repositoryRoot, 'Binaries')
 config.dafnyBinaryDir = binaryDir
 sourceDirectory = os.path.join(repositoryRoot, 'Source')
 
-defaultDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'Dafny', 'Dafny.csproj'))
+defaultDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'Dafny', 'Dafny.csproj')) + ' -- '
 dafnyExecutable = lit_config.params.get('executable', defaultDafnyExecutable )
 
 testDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'TestDafny', 'TestDafny.csproj')) + " -- for-each-compiler"

Test/unicodechars/comp/CompileWithArguments.dfy

@@ -14,11 +14,10 @@
 // RUN: node %s.js "javascript" 2 >> "%t"
 // RUN: node %s.js "javascript" 1 >> "%t"
 // RUN: node %s.js "javascript" "aloha" >> "%t"
-// RUN: %baredafny build %args --unicode-char --no-verify --target:java "%s" >> "%t"
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java %S/CompileWithArguments-java/CompileWithArguments.java %S/CompileWithArguments-java/*/*.java
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java 2 >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java 1 >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileWithArguments-java CompileWithArguments Java aloha >> "%t"
+// RUN: %baredafny build %args --unicode-char --no-verify --target:java "%s" --output:"%s.jar" >> "%t"
+// RUN: java -jar "%s.jar" Java 2 >> "%t"
+// RUN: java -jar "%s.jar" Java 1 >> "%t"
+// RUN: java -jar "%s.jar" Java aloha >> "%t"
 // RUN: %baredafny build %args --unicode-char --no-verify --target:py "%s" >> "%t"
 // RUN: python3 %S/CompileWithArguments-py/CompileWithArguments.py Python 2 >> "%t"
 // RUN: python3 %S/CompileWithArguments-py/CompileWithArguments.py Python 1 >> "%t"

docs/DafnyRef/UserGuide.md

@@ -256,7 +256,7 @@ Various options control the translation process, in addition to all those descri
    - `--verbose` --- print information about generated files
 
 - The translation results
-   - `--output` (or `-o`) --- location (file or folder depending on the target) of the generated file(s)
+   - `--output` (or `-o`) --- location of the generated file(s) (this specifies a file path and name; a folder location for artifacts is derived from this name)
    - `--include-runtime` --- include the Dafny runtime for the target language in the generated artifacts
    - `--optimize-erasable-datatype-wrapper`
    - `--enforce-determinism`
@@ -265,12 +265,17 @@ Various options control the translation process, in addition to all those descri
 
 The `dafny build` command runs `dafny translate` and then compiles the result into an executable artifact for the target platform,
 such as a `.exe` or `.dll`. or executable `.jar`, or just the source code for an interpreted language.
+If the Dafny program does not have a Main entry point, then the build command creates a library, such as a `.dll` or `.jar`.
 As with `dafny translate`, all the previous phases are also executed, including verification (unless `--no-verify` is a command-line argument).
+By default, the generated file is in the same directory and has the same name with a different extension as the first
+.dfy file on the command line. This locaiton and name can be set by the `--output` option.
 
 There are no additional options for `dafny build` beyond those for `dafny translate` and the previous compiler phases.
 
 Note that `dafny build` may do optimizations that `dafny run` does not.
 
+Details for specific target platforms are described [in Section 25.7](#sec-compilation).
+
 <!-- TODO: OLD TEXT: The command has options that enable being specific about the build platform and architecture. -->
 
 #### 25.5.1.6. `dafny run` {#sec-dafny-run}
@@ -1279,19 +1284,21 @@ are contained in [this separate document](integration-cs/IntegrationCS).
 
 ### 25.7.4. Java
 
-The Dafny-to-Java compiler writes out the translated files of a file _A_`.dfy`
-to a directory _A_`-java`. The `-out` option can be used to choose a
-different output directory. 
+The Dafny-to-Java compiler translation phase writes out the translated files of a file _A_`.dfy`
+to a directory _A_`-java`. 
+The build phase writes out a library or executable jar file.
+The `--output` option (`-out` in the legacy CLI) can be used to choose a
+different jar file path and name and correspondingly different directory for .java and .class files. 
+
 The compiler produces a single wrapper method that then calls classes in 
 relevant other `.java` files. Because Java files must be named consistent
 with the class they contain, but Dafny files do not, there may be no relation
 between the Java file names and the Dafny file names.
 However, the wrapper class that contains the Java `main` method is named for
 the first `.dfy` file on the command-line.
-The output folder  will also contain
-translations to java for any library modules that are used.
 
-The step of compiling Java files (using `javac`) requires the Dafny runtime library. That library is automatically included if dafny is doing the compilation,
+The step of compiling Java files (using `javac`) requires the Dafny runtime library. 
+That library is automatically included if dafny is doing the compilation,
 but not if dafny is only doing translation.
 
 Examples of how to integrate Java source code and libraries with Dafny source

docs/dev/news/3355.fix

@@ -0,0 +1,16 @@
+`dafny build` for Java now creates a library or executable jar file.
+- If there is a Main method, the jar is an executable jar. So a simple A.dfy can be built as `dafny build -t:java A.dfy`
+and then run as `java -jar A.jar`
+- If there is no Main entry point, all the generated class files are assembled into a library jar file that can be used on a
+classpath as a java library.
+- In both cases, the DafnyRuntime library is included in the generated jar.
+- In old and new CLIs, the default location and name of the jar file is the name of the first dfy file, with the extension changed
+- In old and new CLIs, the path and name of the output jar file can be given by the --output option, with .jar added if necessary
+- As before, the compilation artifacts (.java and .class files) are placed in a directory whose name is the same as the jar file
+but without the .jar extension and with '-java' appended
+- With the new CLI, the generated .java artifacts are deleted unless --spill-translation=true and the .class files are deleted in any case;
+  both kinds of files are retained with the legacy CLI for backwards compatibility.
+- If any other jar files are needed to compile the dafny/java program, they must be on the CLASSPATH;
+  the same CLASSPATH used to compile the program is needed to run the program
+
+Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts.