Let target be an argument instead of an option for translate

[keyboardDrummer]

Changes

dafny translate is intended to let Dafny interoperate with other languages, so it makes sense to let the specific target language be a mandatory argument, instead of an optional option. This PR lets target be an argument instead of an option for dafny translate.

dafny build was intended to mimic the behavior of dotnet build, producing either a platform specific executable, like a .exe for Windows, or a platform independent executable that can be fed to dafny [run], which executes the program faster than when passing Dafny source files to dafny run, which is similar to producing a .dll using dotnet build and then feeding that .dll back to dotnet to run it.

Right now, dafny build instead produces artifacts that can be run using execution platforms other than dafny, such as using dotnet or java. This is against the intention of dafny build. To remedy this situation, we will also remove the dafny build for now, until we can implement its behavior so it mimics dotnet build.

To enable easily producing .jar etc., we're adding the --compile-target convenience option to dafny translate, that tries to further compile the produced target sources, and will produce .dll and .jar files when C# or Java are chosen as targets respectively.

Testing

Updated tests

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[davidcok]

Wait. Wait. Wait. I thought dafny build was supposed to do what you propose for dafny translate --compile-target . I'd much rather keep each command focussed on its task and not confuse that task with options like this.

[MikaelMayer]

dafny translate is intended to let Dafny interoperate with other languages, so it makes sense to let the specific target language be a mandatory argument, instead of an optional option. This PR lets target be an argument instead of an option for dafny translate.

I haven't looked at the code, but I don't think making the target mandatory is a good idea. Since Dafny is written in C#, it's natural that, if omitted, dafny translate file.dfy actually emits C# code. But I understand that providing the target could be made more explicit.
I would suggest the following:

• Do not remove the target option
• Recognize a target if the first argument, process it and remove it from the list of dafny files.

This approach has the benefits that

• It's no longer a breaking change as you are suggesting, users can still use the option --target if they have it in their workflows (and if a developer like me switches from running on a target to translating on that target to debug something, it makes the transition easier)
• We can keep the command simple for generating C# projects. with only dafny translate
• We have the benefit of not having to remember --target:, we can just put the name of the target

dafny build was intended to mimic the behavior of dotnet build, producing either a platform specific executable, like a .exe for Windows, or a platform independent executable that can be fed to dafny [run], which executes the program faster than when passing Dafny source files to dafny run, which is similar to producing a .dll using dotnet build and then feeding that .dll back to dotnet to run it.
Right now, dafny build instead produces artifacts that can be run using execution platforms other than dafny, such as using dotnet or java. This is against the intention of dafny build. To remedy this situation, we will also remove the dafny build for now, until we can implement its behavior so it mimics dotnet build.

I don't think removing a command will "remedy this situation" in any sense. I had always considered that "dafny build" produces a hands-off executable or library that I can now independently run. How is that against the intention of Dafny build?

To enable easily producing .jar etc., we're adding the --compile-target convenience option to dafny translate, that tries to further compile the produced target sources, and will produce .dll and .jar files when C# or Java are chosen as targets respectively.

You can definitely add this --compile-target option, although I would advise you to remove the -target part of it, just keep --compile which is easier to remember and to type.
But I think in this case you should just change dafny build file.dfy to be a synonym of dafny translate --compile file.dfy, with a possible warning to the user like "/!\ dafny build is currently outputting all the files before compilation, but we want to remove this in the future. If you want to continue emitting the intermediate code before compilation, use dafny translate --compile. To remove this warning, add the option --nowarn-build" or something like that.

[davidcok]

As someone who has done lots of Java in the past and is still concerned that Java integrate well with Dafny, I'll comment the following:

• I use dafny translate specifically for (a) understanding what the dafny translation is doing (i.e. what names and types it is using) so that I can integrate it better with other Java code and (b) creating source artifacts that can be made part of a larger Java project.
• I use dafny build for (a) to compile the java source -- the layout of Java from Dafny is not easy to remember and consequently having to recreate the build line is a nuisance.
• I would like to use dafny build to produce an executable jar file. Perhaps because I had a java mindset, I always did think this was part of the intention of dafny build.
• To me it just does not make sense to replace dafny build by dafny translate --compile and to impoverish dafny build as well.

Any large-scale development project today (that uses Dafny at a all) is highly likely to be a mix of Dafny and other code.
From my perspective, having the translate and build options as they currently are supports those better than the proposal.