Introduce top level commands commands for Dafny

[robin-aws]

Related discussion in: #1322 (comment)

Goal

Update the Dafny CLI so it can accept as its first argument a "command". When no command is passed, the CLI remains unchanged. Commands correspond to use-cases. When a command is used, other options may no longer be available since the command specifies them. The options /compile and /spillTargetCode are not available when using commands.

• dafny verify <inputs>, runs verification, but does not emit anything. Useful in CI and when developing without an IDE.

  • Similar to the current dafny /compile:0

• dafny run <inputs>, runs the Dafny program. Useful for running Dafny applications during development.

  • Similar to the current dafny /compile:3.
  • dafny run --no-verify runs the program without verifying it, similar to dafny /noVerify /compile:4
  • The option --debug=<port> will start a Debug server protocol server that listens at the specified port.
  • By default, no intermediate generated files are visible, although there may be an option to show them, like gcc's save temps
  • By default uses a Dafny back-end that provides a mix of fast compilation, fast execution, and few required dependencies. .NET is a sensible default since .NET is already a required dependency for calling the Dafny CLI.
  • When input files other than .dfy are specified, such as .cs, .dll, .java, .jar, these may be used to implement methods annotated with {:extern} in the Dafny sources. Only input files that use the same back-end type may be used. The option --target may be used to force using a particular back-end.

• dafny build [--os] [--arch] <inputs>, creates a binary that can either be executed directly on the specified platform and architecture, or using dafny run when a platform and architecture independent build is made. Useful when creating a Dafny-only application or library.

  • Example: dafny build --os=win --arch=x64 <sourceFile>, will create a .exe binary that can be executed on a 64 bit Windows machine.
  • Example: dafny build <sourceFile> will create a file that can be executed on any machine using dafny run <builtFile>. We leave the format of the built file unspecified for now.
  • Similar to the current dafny /compile:1.
  • dafny build --no-verify builds the program without verifying it, similar to dafny /noVerify /compile:2
  • By default uses a Dafny back-end that provides fast execution, and few required dependencies. .NET is a sensible default since .NET is already a required dependency for calling the Dafny CLI.
  • The back-end may be configured using --target

• dafny translate <target> <inputs>, compiles to target language source and build files. The end result can immediately be invoked by a target language build tool. Useful for creating libraries to be used by an application written in another language.

  • Similar to the current dafny /compile:0 /spillTargetCode:2 .
  • dafny translate --no-verify skips verification and produces target source code, similar to dafny /noVerify /compile:0 /spillTargetCode:3.
  • Targets are defined as subcommands of translate, and as such may define additional options and arguments. For example, java may take an additional argument [gradle|maven] to specify for which build system to generate files for, so a user could invoke dafny translate java gradle <inputFile>. Since targets are subcommands, help can be shown for them using dafny translate <target> --help.
  • For C#, should generate a .csproj file that references the Dafny Runtime NuGet package and the required .NET version.
  • For JavaScript, should generate a package.json that specifies a Dafny Runtime NPM package as a dependency, and possibly a jsconfig.json to specify which ECMAScript version is required.
  • For Python, should generate a pyproject.toml that specifies the required python version and the Python Dafny Runtime as a dependency.

Alternatives

A translate option that doesn't require a package manager

The current dafny translate produces files that rely on a package manager in the target language. For users who don't want to use a package system, Dafny could provide an option to produce sources that can be easily included as generated source in another project. This would mean the Dafny runtime is emitted as source, and possibly it would be good to package all the sources together in a single large source file for easy inclusion.

Combined commands

Users who want to get the output of different Dafny commands together, can do so by running several commands separately. For example, a customer who wants .cs sources, a .dll, and to run that .dll, can do:

dafny translate cs inputFile.dfy --out=translateFolder
dotnet build translateFolder/inputFile.csproj --out=buildFolder
dotnet buildFolder/inputFile.dll

Alternatively, Dafny could offer combined commands, like translate-build-run.

Out of scope

• dafny package/publish, commands related to publishing build artifacts.
• dafny [test|check] runs tests. Useful when developing and in CI.
  • Similar to the current dafny /compile:0
  • Passing --no-verify will skip verification
• Discussion of what hidden options are available for helping developers of Dafny

Implementation hints

We expect a straightforward implementation

[atomb]

One tiny cosmetic things we might consider doing along with this change, which is already hinted at in #2351 but not explicitly stated: using -- to begin options to the top-level commands. Traditionally, Windows tools have often used / and sometimes allow - instead, but even the .NET CLI has moved toward --, so it'd feel less out-of-place to do something similar.

[MikaelMayer]

I missed this discussion, thanks @atomb for reviving it ! And thanks @keyboardDrummer for starting a draft on this nice feature. I'm already defining the command "format" in this PR, but we can always make it compatible with whatever format we chose.

I would also like to quote my post 20 days earlier
#2351

My remarks on the diff between the two.

• I'm ok to say that "build" means "translate", meaning we produce files.
• I would love love love to see the flag -lang with the command build: dafny build -lang:cs. That would be much better than /compileTarget: especially, since we don't use the wording compile anymore.
• If one of our SinglePassCompiler has a way to "run" a program, then it makes no sense to not offer its default "compile" for the program itself. I'm not sure about your example @robin-aws but it looks like that, for Dafny, a choice had already been made, and we could always provide to compilers something like -compilerArgs with compiler-specific options, like we did for plugins. Other choices could be done by creating compiler plugins. Hence I suggest that:
  • dafny compile [/lang:<lang>] could simply be the equivalent of the previous dafny /compile:1 /compileTarget:<lang> and dafny compile build or something similar could simply be the chaining of the two (emit source files and compile them)

[davidcok]

Not having been involved in this discussion before, the proposed definitions seem reasonably intuitive to me
except I consider 'translate' to mean producing target source code and 'build' or 'compile' to be producing target executables or libraries.

[cpitclaudel]

Should we merge the discussion here with the discussion on #2534 ? I notice that we're starting to repeat things between these two.

[keyboardDrummer]

Should we merge the discussion here with the discussion on #2534 ? I notice that we're starting to repeat things between these two.

Shall we keep this issue focussed on just the commands, since that's what it was originally scoped to? I agree that in #2534 we need to tackle both this issue and the redesign of command line options, but maybe we can keep the issue separate?

[keyboardDrummer]

Not having been involved in this discussion before, the proposed definitions seem reasonably intuitive to me
except I consider 'translate' to mean producing target source code and 'build' or 'compile' to be producing target executables or libraries.

If one of our SinglePassCompiler has a way to "run" a program, then it makes no sense to not offer its default "compile" for the program itself.

Just because we can doesn't mean we should. What would be the use-case of offering compilation to a target language compilation artefact? To me it seems such an artefact it not well defined. It may or may not work on operating systems other than the current one; it may or may not need additional target language runtimes to be installed before it can be executed; and in the case of languages that are not compiled, the output would be the same as that of dafny build.

To take .NET as an example, I think it would be better to let Dafny users that want to generate a .exe or .dll, run the dotnet build tool themselves. That way they can decide which of the many option to use, such as whether the .NET framework is packaged together with the .dll.

[MikaelMayer]

What would be the use-case of offering compilation to a target language compilation artefact? To me it seems such an artefact it not well defined.

I think it's pretty well defined for C# and Java.

[cpitclaudel]

What would be the use-case of offering compilation to a target language compilation artefact?

I often try to build projects in languages that Dafny supports but that I don't know well. It's convenient that Dafny can build an executable that I can then run multiple times.

Even better would be if it told me what comment it runs to build.

[keyboardDrummer]

I often try to build projects in languages that Dafny supports but that I don't know well. It's convenient that Dafny can build an executable that I can then run multiple times.

So it's really a performance issue of running dafny run multiple times then, that you want to avoid by compiling to an executable once? Maybe there could be dafny run --cacheCompilation ?

[MikaelMayer]

So it's really a performance issue of running dafny run multiple times

It's not just about that. It's about the part of a decent programming language to offer to compile to binary its source files. That's everyone's expectation.
If someone makes an executable utility using Dafny and want to distribute it, they will want the compiled version.

[davidcok]

FWIW, I agree with Mikael. I like the ability to translate to source files and also to produce the compiled executable from those sources -- and it is a nuisance to go figure out how to construct the compile line for simple cases, especially for unfamiliar languages. Even for Java, which I know the best of these, the compile command is not immediately obvious.

[cpitclaudel]

So it's really a performance issue of running dafny run multiple times then, that you want to avoid by compiling to an executable once?

You could think of it that way? But I see the source code that Dafny generates as an internal detail (just like dotnet doesn't give me a textual representation of IL as its default output), so by default I'd expect to get a binary, not source code.

[keyboardDrummer]

You could think of it that way? But I see the source code that Dafny generates as an internal detail (just like dotnet doesn't give me a textual representation of IL as its default output), so by default I'd expect to get a binary, not source code.

The source code seems more useful since you can use it to invoke target language build tools. Suppose you want to publish a .NET package, wouldn't you then rather start with .cs and .csproj files than with a .dll?

If someone makes an executable utility using Dafny and want to distribute it, they will want the compiled version.

How are you distributing? Are you publishing to a package repository using the target language package manager? Do you then really prefer something that's already further compiled instead of source files?

---

Relevant discussion is in this issue: #1322

@jonhnet writes:

Should Dafny run all the back-end tools all the way to an executable? When it had a single C# backend, that felt pretty natural, just like I can invoke the assembler and linker by invoking gcc; they're abstracted away into the C interface. With a half-dozen backends, this feels a lot less natural: what an "executable" means for each backend is different, and many of the new backends have been introduced precisely to fit Dafny code into bigger systems. I'm with Bryan that one-step-to-executable is really only relevant for small programs, just as real systems very quickly outgrow "gcc foo.c into a.out".

[robin-aws]

Tentatively added this to Dafny 4.0, not because it is a breaking change but because it offers a fresh API where we can make breaking changes that aren't actually breaking, so I think it's relevant for planning purposes. :)

[MikaelMayer]

Suppose you want to publish a .NET package, wouldn't you then rather start with .cs and .csproj files than with a .dll?

Of course, target language files and csproj files are very important. We are not arguing that .cs and .csproj files are better than a .dll.
We only want to recognize the need to being able to produce and executable (at least for small-scale program). The Hello World of Dafny should still work with dafny run hello-world.dfy. So we don't want to remove it "because it's complex". We can always document its limit (i.e. has to be standalone, without extern, etc.)

[keyboardDrummer]

The Hello World of Dafny should still work with dafny run hello-world.dfy

Ok, that's part of the proposal right?

So we don't want to remove it

Which it?

[MikaelMayer]

Which it?

The ability to run (and thus compile and leave the executable of) a program.

[MikaelMayer]

dafny build hello-world.dfy

[robin-aws]

My suggestion here would be to have our "compile targets" be more precise, to name not just the target programming language used but also the actual artifact produced. We could have /compileTarget:cs to mean compile the Dafny source to equivalent *.cs files, but also /compileTarget:dll to mean compiling the target C# program as well. Similarly for Python (#2567) the currently supported target is /compileTarget:py which means Python source files, but we could also support /compileTarget:pyc.

The meaning of the top-level commands would become:

1. dafny build /compileTarget:X - Verify and then translate the Dafny source code to produce X.
2. dafny run /compileTarget:X - Verify, translate to produce X, and then execute X.

The idea of a compile target is then quite flexible, as long as there is some way to execute the artifact(s) produced whenever there is a main method defined. We could even support the Dafny interpreter under construction in the compiler-bootstrap project: https://github.com/dafny-lang/compiler-bootstrap/blob/main/src/REPL/Repl.dfy. In that case the "translation" step becomes a no-op. We may just want to produce some kind of token on disk in the verification phase so that the interpreter by default knows it is executing verified code.

[robin-aws]

I expect once we have a Dafny project file it will be extremely useful to specify multiple compileTarget options, so that building a project produces multiple flavours of artifacts while sharing the frontend phases of parsing, resolving, verifying, and so on.

[keyboardDrummer]

/compileTarget:dll to mean compiling the target C# program as well

I don't think "dll" wouldn't be specific enough to point to C#, but you could have "csdll". Which options would this pass to the C# compiler? Would you then also have an option "/targetLanguageCompilerOptions:"X=3,Y=3,.." that allows feeding in options to the C# compiler? I don't think that would be more attractive to users than calling dotnet separately and getting the dotnet CLI help for passing in options, and long as /compileTarget:cs generates c# build files (.csproj) that can be immediately consumed by dotnet.

dafny run /compileTarget:X - Verify, translate to produce X, and then execute X.

Would dafny run /compileTarget:X only allow an X that is directly executable, like "csdll", but not .cs source files? That seems inconsist with dafny build /compileTarget:X

I expect once we have a Dafny project file it will be extremely useful to specify multiple compileTarget options

I can see that being useful for projects that target multiple languages, but I don't see it being useful for generating different types of artefacts for the same language, like both .cs and c# based .dll files.

[MikaelMayer]

@robin-aws, I like a lot the idea of reusing /compileTarget to specify what kind of artefact we want Dafny to build.
In #2603, @keyboardDrummer renamed this command /target:, which is way more user-friendly.

I don't think "dll" wouldn't be specific enough to point to C#
Would dafny run /compileTarget:X only allow an X that is directly executable, like "csdll", but not .cs source files? That seems inconsist with dafny build /compileTarget:X

Fair enough. Let me suggest an approach that should be consistent and does not remove features that we had been offering to users until now.

Let's have every compiler declare what targets they can generate. Common targets would include "translate" (implicit in the build command if no other target is given) and "run" (implicit in the "run" command)

• CsharpCompiler declares that it can handle targets "translate", "dll", "csproj" and "run"
• CppCompiler declares that it can handle targets "translate", "exe" and "run"
• JavaCompiler declare that it can handle targets "translate", "jar" and "run"
• PythonCompiler declares that it can handle targets "translate", "pyc", and "run"
  ...

1. If /target:<target> is provided, we select the first compiler that can provide this kind of target
2. If /target:<lang>-<target> is provided, then we select the compiler defined by "lang" and we ask it to produce the target.
3. We can provide multiple targets for a single compiler by adding more -<target> to the /target: option.

Corollaries:

• dafny build /target:<lang> standalone automatically internally rewrites to dafny build /target:<lang>-translate, meaning we implicitly insert the "translate" target if no other target is given
• dafny build /target:dll will figure out that CSharpCompiler is the first that can handle dlls, and automatically internally rewrites to dafny build /target:cs-dll (with default options) and won't produce the intermediate source files
• dafny build /target:translate-dll will automatically rewrite to dafny build /target:cs-translate-dll and will produce the intermediate source files along with the dll (with default options)
• The command dafny run /target:<lang> is a syntactic sugar for dafny build /target:<lang>-run
• It becomes possible to produce the intermediate files, a project file, the intermediate executable and run it using either
  dafny run /target:<lang>-translate-csproj-dll

I designed the above targets so that they are easy to remember, correspond to what we would have expected before and now, and don't reduce the possibilities that compilers offer.
Moreover, for compilers provided by plugins, it makes it possible to define custom targets, which would not have been possible before.

Would you then also have an option "/targetLanguageCompilerOptions:"X=3,Y=3,.." that allows feeding in options to the C# compiler?

Of course that could be great, but first, we would probably name this option /targetOptions, and second, since we are not offering this right now, we don't need to take a decision on such a feature yet. I would even bet that for custom compilation that goes beyond defaults, users would use the translated source files anyway.

[davidcok]

A cpp compiler could also generate a .a or .so (so target:lib ?)

[cpitclaudel]

We may just want to produce some kind of token on disk in the verification phase so that the interpreter by default knows it is executing verified code.

For the interpreter this is not needed, since it does not assume that the code has been verified.

I like a lot the idea of reusing /compileTarget to specify what kind of artefact we want Dafny to build.

I don't like it too much. The target language and the kind of output to produce seem pretty orthogonal to me. I would much prefer have separate target-language and target-kind flags (especially since outputs can be non-executable, e.g. the C# compiler knows how to produce single files or project files, and maybe it also knows how to produce one file per module or one whole file.

[MikaelMayer]

The target language and the kind of output to produce seem pretty orthogonal to me

I agree we could have /target-language and /target-kind flags, but having also the common /target that accepts both (and can expand to the first two) would be very practical. It's similar to being able to define in CSS border: 1px red instead of border-color: red; border-width: 1px,. Although the two concepts are orthogonals, it's very convenient to define them in a single line where it's unambiguous.

So unless we have a language whose name is "run" or "translate", "csproj", "dll" or "exe", the fact that these concepts are orthogonal is perfect to gather them in one place unambiguously.
Moreover, it will prevent users from mistakenly write /target-kind:cs or /target-language:translate because they don't remember which option is for what.

[keyboardDrummer]

@MikaelMayer can we take a step back and first look at the use-cases? I'd prefer to let our UI reflect the use-cases instead of focussing on what the CLI can do.

Three use-cases I see are:

1. Run a standalone Dafny application once
2. Run a standalone Dafny application many times
3. Integrate a Dafny application with one written in another language

For use-case (1), we currently have dafny --compile:[3|4]. I'm proposing to replace that with dafny run. There doesn't seem to be discussion about that.

For use-case (3), we currently have dafny --spillTargetCode:[...]. I'm proposing to replace that with dafny integrate (previously I proposed calling it dafny build), which creates source and build files for the target language. I don't think the current dafny --compile:[1|2], which creates a target language binary artefact, like a .dll or .jar, is useful for use-case (3).

For use-case (2), we currently have dafny --compile:[1|2], which creates a target language binary artefact, like a .dll or .jar, which allows you to run the Dafny compiler once and then quickly execute the binary multiple times. However, this still requires the user to know how to execute the produced binary. I think we can do better: we should aim for a solution that doesn't require the user to think about a language other than Dafny.

I think ideally we'd have dafny build [--platform=<platform>] that can create both an artefact that can be executed directly on the platform it was built for, or a platform independent artefact that can be executed using dafny run. We can achieve the latter by letting dafny build do the same as dafny /compile:1. For the former we can use dotnet's --self-contained option to produce a native binary.

We will let dafny build have a --target:<language> option just like dafny run, but this seems mostly useful for Dafny developer debugging purposes, since by default dafny build and dafny run should use a generally well performing Dafny back-end.

[MikaelMayer]

For use-case (1), we currently have dafny --compile:[3|4]. I'm proposing to replace that with dafny run. There doesn't seem to be discussion about that.

Agreed, based on the discussions. The option /noVerify will replace the choice between 3 and 4

For use-case (3), we currently have dafny --spillTargetCode:[...]. I'm proposing to replace that with dafny integrate (previously I proposed calling it dafny build), which creates source and build files for the target language. I don't think the current dafny --compile:[1|2], which creates a target language binary artefact, like a .dll or .jar, is useful for use-case (3).

I disagree respectfully. For users, one way to integrate with another project is to simply create a stand-alone verified DLL or JAR (a library that does not need to be run, but that is 100% Dafny). That was one of the promises of Dafny: To create verified libraries in target platforms.

Also, I still largely prefer dafny translate (to remind Rosetta) or dafny build (that is more generic) rather than dafny integrate, because integration means Dafny has to take into account an existing project, which is not in the current abilities of our compiler. The user currently has the responsibility of setting up correct "extern". That could change, but within the scope of this change, I don't think we want to tackle this. We want to keep the existing behavior for now.

For use-case (2), we currently have dafny --compile:[1|2], which creates a target language binary artefact, like a .dll or .jar, which allows you to run the Dafny compiler once and then quickly execute the binary multiple times.

As said in my paragraph above, the binary artefact might just be a library and not be executable per se, but it could be useful for another executable application.

We will let dafny build have a --target: option just like dafny run, but this seems mostly useful for Dafny developer debugging purposes, since by default dafny build and dafny run should use a generally well performing Dafny back-end.

I see dafny run also as a practical way to test the different back-ends, especially if different back-ends have different assumptions that need to be tested (i.e. contracts around externs)

[keyboardDrummer]

That was one of the promises of Dafny: To create verified libraries in target platforms.

I agree.

I disagree respectfully. For users, one way to integrate with another project is to simply create a stand-alone verified DLL or JAR (a library that does not need to be run, but that is 100% Dafny).

Are you saying that a user running dafny /compile:1 /compileTarget:<lang> and using the results of that as part of a bigger application, is something we can expect?

I doubt this is a useful workflow for users since it doesn't give them control over the artefact that's produced by the target language build system. Even for one of the least configurable target platforms, .NET, the user still wouldn't know whether the created .dll has been optimised for running or debugging, and whether it's built for a particular platform or requires the .NET framework. Even if the .dll happens to be what they need, then wouldn't users in general prefer a workflow where they explicitly call dotnet to generate a .dll, so they know what .dll they're getting?

Integrating a Dafny library as part of a bigger application also means that the user is already familiar with the target language build system, so is there really a downside to asking them to invoke it? I think dafny [integrate|translate] would produce both source (.cs) and build (.csproj) files, so that users can immediately invoke the target language build tool without requiring them to provide extra configuration.

Also, I still largely prefer dafny translate (to remind Rosetta) or dafny build (that is more generic) rather than dafny integrate, because integration means Dafny has to take into account an existing project, which is not in the current abilities of our compiler.

I think translate better reflects what the CLI does than integrate. However, I thought we should choose the names so they map to what the user wants to do, rather than what it makes the CLI do, but I can see this being a point of contention. I think integrate better reflects the user's need than translate.

I see dafny run also as a practical way to test the different back-ends, especially if different back-ends have different assumptions that need to be tested (i.e. contracts around externs)

Agreed

[davidcok]

I vote in favor of both the use cases of

• Dafny putting out target source code
• Dafny putting out a compiled library (or executable).
  Even just in putting together examples combining Java and Dafny, it would be nice to get out a .jar file.
  I understand the point about control and that sometimes one wants to put in more information for the target language compile. But actually for that case I would also suggest a '-targetArgs' option which states additional CLI options for the compilation step.

As for names, I prefer 'translate' for the step of emitting source code.

[MikaelMayer]

Good job for the issue description rewriting @keyboardDrummer .

dafny integrate-cs

I think you meant dafny translate according to the above.

• dafny build /noVerify skips verification and produces target source code, similar to dafny /noVerify /compile:0 /spillTargetCode:3.

Let's choose between noVerify and no-verify officially (we can support with or without dash internally, and whatever capitalization). I think I could accomodate also -iassumeallresponsibilitysopleasedontverify :-).

dafny build [--arch]

What did you have in mind with --arch ? Can you please give an example.

For C#, should generate a .csproj

Could I please have an option --no-project file for the translate option? That will be useful for compiler development and debugging?
Also, would it be the plan to disable translate without --no-project until we implement a proper package generation after the PR that will introduce translate?

Missing in the discussion and alternatives

1. dafny check vs. dafny verify. Because we have the option "no-verify", I think we should choose dafny verify and put dafny check in the envisioned alternatives.
2. I think dafny integrate should be mentioned in the alternatives that we envisioned and that we did not choose. It's good to keep a trace of decisions
3. • dafny translate would produce the source files but no binary and not execute it. dafny build would produce the binary files but not the source files nor run it. dafny run would not produce the source files, no binary (other than in a /tmp folder), and run it.
     However, many times I'm like "I want to produce the files, compile them, and run them at the same occasion". Or any combination of these. It's unclear with the new verb system how we can achieve that. Could you please clarify? Would we be able to write "dafny translate build run" to exp
4. The option "-print" that prints the *.bpl file can be seen as a "translate", and dafny verify as a kind of dafny run on the Boogie platform. Could we enable dafny translate bpl or dafny translate boogie ?

[keyboardDrummer]

Could I please have an option --no-project file for the translate option? That will be useful for compiler development and debugging?

What should this option do besides leaving out the project file? Should it bundle all produces sources into a single source file with the Dafny runtime inlined? How will it be used?

dafny check vs. dafny verify. Because we have the option "no-verify", I think we should choose dafny verify and put dafny check in the envisioned alternatives.

That's a good point. I'm curious how much time it'll take to generally test a Dafny program versus verifying it. Generally languages have a way of running just resolution checking without running tests, since checking resolution is much cheaper. I made the assumption that testing a Dafny program was at a similar weight level as verifying, and thus users would generally want to do both at the same time, but thinking about that again I'm not so sure. Maybe testing is in a sense less bounded in runtime than verification, since you can generate large amounts of inputs for testing. In that case, I'd prefer having dafny verify and dafny [test|check] [--no-verify] be separate.

However, many times I'm like "I want to produce the files, compile them, and run them at the same occasion". Or any combination of these. It's unclear with the new verb system how we can achieve that. Could you please clarify? Would we be able to write "dafny translate build run" to exp

You wouldn't be able to do that in one step. I think it's fundamental about the verb system that you have to make choices about what you want to achieve, and once you choose one verb, results and options of other verbs may not be available. You could create combined verbs like translate-build-run, but then you have to weigh the usefulness of this verb against how much it heavier it makes the CLI help. How useful would this combined verb be for you? When would you use it?

The option "-print" that prints the *.bpl file can be seen as a "translate", and dafny verify as a kind of dafny run on the Boogie platform. Could we enable dafny translate bpl or dafny translate boogie

Interesting point, I thought about this too. However, I don't see how dafny translate boogie is useful for users. Dafny users don't need to integrate Dafny's Boogie output with other Boogie programs. Outputting Dafny's Boogie is meant for debugging Dafny. If a Dafny user has trouble getting a proof to verify, and they want to deep dive by inspecting the generated Boogie, then I would say they're 'debugging Dafny', and it's ok for them to have to look at Dafny's contributing documentation, which could lead them to a hidden option that prints Boogie. Offering an option to print Boogie as part of the default CLI help seems like bloating the help to users to me.

[MikaelMayer]

What should this option do besides leaving out the project file? Should it bundle all produces sources into a single source file with the Dafny runtime inlined? How will it be used?

After reflection, It looks like it's already the case that /spillTargetCde outputs jar dependencies, or necessary headers of cpp. Well, in that case, we can ignore this. I can always ignore the project file and have it overriden when I'm trying to call Dafny on multiple test files.

In that case, I'd prefer having dafny verify and dafny [test|check] [--no-verify] be separate.

Looks good to me.

You wouldn't be able to do that in one step. I think it's fundamental about the verb system that you have to make choices about what you want to achieve, and once you choose one verb, results and options of other verbs may not be available. You could create combined verbs like translate-build-run, but then you have to weigh the usefulness of this verb against how much it heavier it makes the CLI help. How useful would this combined verb be for you? When would you use it?

Making choice about what you want to achieve needs not to be exclusive. Being able to put multiple verbs next to each other makes sense in our case. We have to consider that the verbs "translate", "build" and "run" describe three phases of our pipeline, each depending on the previous one. The choice to make is whether we want to emit intermediate outputs or not. Why forcing the user to choose between the three? Moreover, this isn't added complexity in the implementation, we already do this in the current CLI. I'm talking only about a migration to a better command line, that is easier to remember.

However, I don't see how dafny translate boogie is useful for users.

It's useful for developers of the Dafny language. We do not need to consider it at this stage. But please put it in the "out of scope" section of the handling of this issue.

[keyboardDrummer]

Why forcing the user to choose between the three?

I think the way commands work is that you can't have two commands for one invocation, so while you could add a combined command, like translate-build, you can't have translate build.

Suppose you did dafny verify translate --help, what would be the output? Would it show the option --no-verify? What if one commands enforces options that conflict with another? For example, I'm on a Windows machine and I do dafny build run --os=linux, then I'm building an executable that only works on linux, which I can't run on my Windows machine.

I think to make it all work well, you've have to introduce combined commands, so you could introduce verify-translate that doesn't have the option --no-verify and you could introduce build-run that doesn't have the options arch and os.

On a technical note, the System.CommandLine library that we're intending to use also doesn't support multiple separate commands.

[MikaelMayer]

Suppose you did dafny verify translate --help, what would be the output?

The help of dafny verify, and the help of dafny translate, the first one on the top of the second

Would it show the option --no-verify?

Only for the help of dafny translate. And we could emit a warning that this option has no effect in dafny verify (unless we just want to print the Boogie source code)

What if one commands enforces options that conflict with another? For example, I'm on a Windows machine and I do dafny build run --os=linux, then I'm building an executable that only works on linux, which I can't run on my Windows machine.

First, I don't think we have these conflicts right now, so this is not relevant to this PR. Second, I think that when this happens, the "run" could ignore the --os= part, it can ensure a build of its own, run it in the linux subsystem, etc. I don't think we need to take these decisions now.

[keyboardDrummer]

Suppose you did dafny verify translate --help, what would be the output?

The help of dafny verify, and the help of dafny translate, the first one on the top of the second

Would it show the option --no-verify?

Only for the help of dafny translate. And we could emit a warning that this option has no effect in dafny verify (unless we just want to print the Boogie source code)

What if one commands enforces options that conflict with another? For example, I'm on a Windows machine and I do dafny build run --os=linux, then I'm building an executable that only works on linux, which I can't run on my Windows machine.

First, I don't think we have these conflicts right now, so this is not relevant to this PR. Second, I think that when this happens, the "run" could ignore the --os= part, it can ensure a build of its own, run it in the linux subsystem, etc. I don't think we need to take these decisions now.

It's not clear to me how you're suggesting it would work. Does dafny verify translate do two separate runs, one dafny verify and one dafny translate ? That seems wasteful.

I think what is closer to what you're looking for is an option --emit-sources for build and run, and an option --emit-binary for dafny run, but I was planning on hiding the --target option for both of these commands, since it's not relevant unless you're a Dafny language developer.

Could you tell me what's the exact scenario in which you're looking to do a translate-build-run? You're doing a run, so apparently it's a standalone Dafny application, not a library. I can imagine you also want to emit the binary, since you might decide the run performed well and immediately want to start using the binary. Now what do you need the translate sources for?

[cpitclaudel]

FTR, link to GCC's developer's options (including -save-temps): https://gcc.gnu.org/onlinedocs/gcc/Developer-Options.html