Skip to content
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

Switch Over to New Dafny CLI Style #558

Closed
DavePearce opened this issue Apr 3, 2023 · 3 comments · Fixed by #563
Closed

Switch Over to New Dafny CLI Style #558

DavePearce opened this issue Apr 3, 2023 · 3 comments · Fixed by #563

Comments

@DavePearce
Copy link
Collaborator

Currently, Dafny has two CLI "styles". For example, the new style looks like this:

dafny build --output-files

The goal here is to complete the switch over to the new style.

@DavePearce
Copy link
Collaborator Author

DavePearce commented Apr 4, 2023

There are some challenges here:

  1. When using translate, the --include-runtime option doesn't seem to do anything.
  2. When using build, Dafny wants to compile the whole thing into a Jar file. This is not interacting very well with Gradle.

So, dafny translate currently appears the most promising but the Java build (under Gradle) fails because it doesn't have access to the DafnyRuntime.jar. Perhaps future versions of Dafny will fix --include-runtime ?

@DavePearce DavePearce linked a pull request Apr 4, 2023 that will close this issue
@DavePearce
Copy link
Collaborator Author

Seems like we can make this work using dafny build instead of dafny translate and them compiling the java files against the generated jar file.

@DavePearce
Copy link
Collaborator Author

So, I have hit a road-block on this issue:

  • When using the new CLI style, verification consistently fails for reasons unknown.

See this issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant