forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Jar files, both library and executable, are now created as part of bu…
…ild on Java (dafny-lang#3355) Fixes dafny-lang#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 <davidcok@github.com>
- Loading branch information
Showing
24 changed files
with
165 additions
and
27 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -17,6 +17,7 @@ | |
|
||
# Java output | ||
**/*-java | ||
**/*.jar | ||
|
||
# C++ output | ||
**/*.h | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
A.jar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
|
||
Dafny program verifier finished with 0 verified, 0 errors | ||
Hello, World! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
B.jar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
|
||
Dafny program verifier finished with 0 verified, 0 errors | ||
Hello, World! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
package org; | ||
|
||
public class D { | ||
public static void main(String[] args) { | ||
_System.__default.m(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
A.jar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
|
||
Dafny program verifier finished with 0 verified, 0 errors | ||
Hello, World! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
A.jar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
|
||
Dafny program verifier finished with 0 verified, 0 errors | ||
Hello, World! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. |