-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The product of dafny build for java should be an executable jar file, not a class file #2827
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Comments
MikaelMayer
added
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
labels
Sep 30, 2022
davidcok
added a commit
that referenced
this issue
Jan 16, 2023
…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 <davidcok@github.com>
davidcok
added a commit
to davidcok/dafny
that referenced
this issue
Jan 18, 2023
…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>
davidcok
added a commit
to davidcok/dafny
that referenced
this issue
Jan 20, 2023
…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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
The
dafny build
command is supposed to produce an executable artifact in the target language.The closest thing to that in Java is an executable jar file; that would be preferable to the array of class files now generated.
A more recent alternative might even be to use jlink.
The text was updated successfully, but these errors were encountered: