Backend-specific options should be available for all backend-specific CLI commands

[robin-aws]

We have options like --go-module-name and --python-module-name that can be passed to the corresponding dafny translate go and dafny translate python commands. They are not hooked up for similar commands like dafny build -t:go or dafny test -t:go though.

[ShubhamChaturvedi7]

AFAIK, this was done deliberately because translate is the only command that was supposed to spit out code for libraries. What has changed?

[robin-aws]

No I think was more of an oversight, it was enough effort to make any per-backend options that I think we didn't think as much about this. :)

The other commands like dafny build and dafny run certainly do run against a specific backend, and even if you aren't looking at the code, there will be options that affect that code. Given something like dafny build <lang> is essentially "dafny translate <lang> and then build the result in ", you should be able to specify the same options.

As a concrete example, https://github.com/dafny-lang/dafny/pull/5613 wants to add a --raw-pointers flag just for Rust, which affects the structure of the Rust code pretty substantially. It's reasonable to want to test a program with dafny test -t:rs --raw-pointers.

[MikaelMayer]

@keyboardDrummer how would you go about solving this issue ?

[robin-aws]

I recall now the issue is that for dafny translate go ..., we make go a subcommand with it's own set of options to parse, whereas for dafny build -t:go ... we have to provide the set of valid options for dafny build before parsing, so it's too late by the time the parsing gets to the -t:go option.

An alternative is to keep the option at the top level but document it clearly as only being for one backend, or perhaps more in the future, and then raise an error if it's used with an incompatible backend. Something like:

> dafny build --help-internal
...
--raw-pointers (backend specific: rust)
...
> dafny build -t:go --raw-pointers ...
Error: --raw-pointers can only be used with the following backends: rust

[keyboardDrummer]

No I think was more of an oversight, it was enough effort to make any per-backend options that I think we didn't think as much about this. :)

It was my intention for these options to only be available for dafny translate

Looking at the future, I think it's important to have commands for Dafny that are optimized for applications defined with Dafny as the only or primary language, and my intention is for dafny run and dafny build to be two of these. dafny run is for development, to run a piece of code as quickly as possible, possibly with a debugger attached. dafny build is for producing a runnable artifact that runs quickly and with little startup time.

I think neither dafny run or build should focus on the use-case of vending Dafny code as a non-Dafny library. My belief is that dafny translate covers most of that use-case, because you will almost surely want to customize the downstream build more than Dafny allows you to, so Dafny only needs to produce sources in the target language.

What's your use-case for using dafny build with target specific options?

[MikaelMayer]

We had already this disagreement in the past, I remember :-)

I remember that you were hesitant at having/keeping the "--target" option for run, because you thought of "run" as a black box, such that the user should not even think what backend it's going to execute on, since it's Dafny they are executing. Similarly, I remember you considering that "build" should build a runnable artifact such that the user would not have to think in which language the artifact was produced with, and similarly not really liking the the "--target" option for specifying the backend of the build. Finally, I remember you pushed for making the target a subcommand of the "translate" command instead of an option, as it was the only way you thought we should ideally produce artifacts, is that correct?

In practice, we use dafny run to test the capabilities of each individual back-end and to verify that they all emit the same value. All our multi-compiler tests are run using dafny run with different language targets. dafny run however does not have the guarantee to create the repository locally, it creates a temporary folder and put everything there. On the other side, we also use in our test suite dafny build when we want to run the artifact multiple times on different outputs, and again for each backend, because it has the guarantee that the artifact build is in the provided or current folder.

I also now use dafny build to verify that the source code that is compiled conforms to some expectations, like programs compiled with --unicode-char false should use a specific kind of string that is not visible only by testing input/output. Now I also use dafny build to ensure I don't just have some source code that I can plug-in somewhere, but that Dafny is able to create an all-included package in the given target, that is, it knows both the language and the minimum build script that makes the program compilable in the target language. That way, I can for example run cargo test after a successful dafny build on the resulting repository which is nearby.

As we do support the --target option for test, build and run, I don't see a reason that would justify to prevent backend-specific options from being available there as well.

Please let me know how we could make it happen without having to move all the options back to DafnyNewCli ?

[keyboardDrummer]

Please let me know how we could make it happen without having to move all the options back to DafnyNewCli ?

You can add a --compile/build option to dafny translate that would make it behave like dafny build but with a target and target specific options

[robin-aws]

I think it's absolutely true that users of dafny run will generally care a lot less about most translation options than those using dafny translate. Many of them will only be relevant if you're building libraries that have to interoperate with other code.

I don't think it's fair to say dafny run users will NEVER care though. Something like --raw-pointers could potentially have a big performance benefit for some programs, and at the same time it's likely it shouldn't be the default because it's much less safe.

I do expect that in the long term projects will set such an option in a project file and never actually explicitly pass it to dafny run. But for consistency we should definitely accept it on dafny run when appropriate.

[keyboardDrummer]

I don't think it's fair to say dafny run users will NEVER care though. Something like --raw-pointers could potentially have a big performance benefit for some programs, and at the same time it's likely it shouldn't be the default because it's much less safe.

What does/would that option do?

[MikaelMayer]

What does/would that option do?

That option would change reference-counted mutable cells into nonnull mutable cells, saving the cost of increasing/decreasing counter references, at the expense of not deallocating memory. This is fine for short-lived programs or if programs recycle memory using pools.