Use subcommands instead of an argument for the various back-ends that can be used with translate #4601

keyboardDrummer · 2023-10-03T13:24:23Z

Changes

Use subcommands instead of an argument for the various back-ends that can be used with translate, this allows each sub-command to get custom option. The syntax for using translate remains the same.
Remove ICommandSpec, which was a wrapper around System.Commandline.Command that made it difficult to introduce commands that did something different than run the Dafny compilation pipeline. Commands that benefit from this are dafny server, dafny format, dafny doc, dafny generate-tests, dafny find-dead-code, dafny merge-coverage-reports
Previously DafnyDriver did some CLI argument processing, and some orchestrating of the various steps of the Dafny pipeline. It has been renamed to CompilerDriver and now only does the latter. CommandRegistry was previously doing part of argument processing, but is now doing all argument processing and has been renamed to DafnyCli. There was some testing code related to CLI arguments in DafnyDriver that has been moved to a new class DafnyCliTests.
No longer build the standalone Dafny server executable

Help output

Default:

rwillems@bcd0745419f2 dafny % ./Scripts/dafny translate --help
Description:
  Translate Dafny sources to source and build files in a specified language.

Usage:
  Dafny translate [command] [options]

Options:
  -?, -h, --help   Show help and usage information
  --help-internal  Show help and usage information, including options designed for developing the Dafny language and toolchain.

Commands:
  cs <file>    Translate Dafny sources to C# source and build files.
  js <file>    Translate Dafny sources to JavaScript source and build files.
  go <file>    Translate Dafny sources to Go source and build files.
  java <file>  Translate Dafny sources to Java source and build files.
  py <file>    Translate Dafny sources to Python source and build files.
  cpp <file>   Translate Dafny sources to C++ source and build files. This back-end has various limitations (see Docs/Compilation/Cpp.md). This includes lack of support for BigIntegers (aka int), most higher order functions, and advanced features like traits or co-inductive types.

With hidden commands (Rust):

rwillems@bcd0745419f2 dafny % ./Scripts/dafny translate --help-internal
Description:
  Translate Dafny sources to source and build files in a specified language.

Usage:
  Dafny translate [command] [options]

Options:
  -?, -h, --help   Show help and usage information
  --help-internal  Show help and usage information, including options designed for developing the Dafny language and toolchain.

Commands:
  cs <file>    Translate Dafny sources to C# source and build files.
  js <file>    Translate Dafny sources to JavaScript source and build files.
  go <file>    Translate Dafny sources to Go source and build files.
  java <file>  Translate Dafny sources to Java source and build files.
  py <file>    Translate Dafny sources to Python source and build files.
  cpp <file>   Translate Dafny sources to C++ source and build files. This back-end has various limitations (see Docs/Compilation/Cpp.md). This includes lack of support for BigIntegers (aka int), most higher order functions, and advanced features like traits or co-inductive types.
  lib <file>   Translate Dafny sources to Dafny Library (.doo) source and build files.
  rs <file>    Translate Dafny sources to Rust source and build files.

Testing

Tests that were testing properties of the standalone language server process are now testing the Dafny CLI with the server command instead
The rest of this PR is a refactoring that's covered by existing tests

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

…o backendCommand

Source/DafnyLanguageServer.Test/StandaloneServerTest.cs

Source/DafnyDriver/CompilerDriver.cs

Source/DafnyDriver/Commands/DafnyCliTests.cs

Source/DafnyDriver/Commands/TranslateCommand.cs

robin-aws · 2023-10-04T23:13:07Z

Source/DafnyDriver/Commands/TranslateCommand.cs

-    var noVerify = dafnyOptions.Get(BoogieOptionBag.NoVerify);
-    dafnyOptions.CompilerName = context.ParseResult.GetValueForArgument(Target);
-    dafnyOptions.SpillTargetCode = noVerify ? 3U : 2U;
+    result.AddCommand(new Command("cs", "C#"));


Shouldn't the subcommands be dynamically populated based on the set of available backends? Or are you going to leave that for #4591? (That would be just fine if so)

There's a catch-22 there because plugins can add new back-ends. I think it would be better if plugins that expose new back-ends are new binaries that reference Dafny as a library. They could potentially then be called using dafny translate <new-backend-name> by being available on path with the name dafny-translate-<new-backend-name>, similar to how dotnet does it.

@MikaelMayer

I'll populate it based on the hardcoded back-ends though.

Ah that is an unfortunate circular dependency. That sounds like this PR breaks the workflow for compiler plugins though, because something like dafny translate blort ... --plugin:BlortCompiler.dll will no longer work?

The whole reason why plugins are provided to Dafny rather than the other way round is that it makes it possible to add these plugins to Dafny in VSCode too, including plugins that expose backends, because these backends could also serve as a basis for verifying things specifics to some backends in the future;

I suggest that, for custom back-ends, we simply break the circular dependency by having a special command that emulates the previous behavior, like "custom-backend" that will support an option like "--name:rs" and load a back-end from the set of plugins.

That sounds like this PR breaks the workflow for compiler plugins though, because something like dafny translate blort ... --plugin:BlortCompiler.dll will no longer work?

That's correct, but I can't imagine anyone was doing this.

The whole reason why plugins are provided to Dafny rather than the other way round is that it makes it possible to add these plugins to Dafny in VSCode too

That you can still do. dafny server --plugin:AddWhateverYouLikeToTheIDE.dll

I suggest that, for custom back-ends, we simply break the circular dependency by having a special command that emulates the previous behavior, like "custom-backend" that will support an option like "--name:rs" and load a back-end from the set of plugins.

I suggest we consider adding that when there's a need.

That's correct, but I can't imagine anyone was doing this.

To clarify: you don't believe anyone was doing this or you just don't know about this use case?

That you can still do. dafny server --plugin:AddWhateverYouLikeToTheIDE.dll

But then they can't choose the back end. I know of at least one team that has two custom back-ends and use VSCode with their custom plugin. I'm pretty sure they will appreciate being able to right-click, and select dafny run, and with their custom arguments can choose which backend it would run on.

I suggest we consider adding that when there's a need.

This PR is removing what was plugins enabled in the first place, for which @cpitclaudel spent quite some time refactoring the codebase. In general, I would say that any PR that removes a feature without offering workarounds, when the author does not have evidence will not affect customers, should be approved by at least two team members, one of which participated in the creation of the said feature if possible.

+1 to what @MikaelMayer is saying, unfortunately. Is there any way we can special-case the --plugin option so it can be at least partially processed before resolving the subcommands? I doubt it without moderate hackery but I have to ask anyway. :P

Alternatively, how hard would it be to implement this idea instead? "They could potentially then be called using dafny translate by being available on path with the name dafny-translate-, similar to how dotnet does it." Then we would at least have a quick workaround to the breaking change.

Made a related PR: #4627

Is there any way we can special-case the --plugin option so it can be at least partially processed before resolving the subcommands?

We can but I don't think we should. Actually I think some of our current back-ends should become separate binaries at some point.

Alternatively, how hard would it be to implement this idea instead? "They could potentially then be called using dafny translate by being available on path with the name dafny-translate-, similar to how dotnet does it." Then we would at least have a quick workaround to the breaking change.

The 'workaround' is to build a binary instead of a library when building your custom back-end. The users that I know whom are using custom back-ends already do this. They also use a Dafny plugin but they don't use it for translation to a target language, only to customize resolution of the language server, which this PR still allows.

But then they can't choose the back end. I know of at least one team that has two custom back-ends and use VSCode with their custom plugin. I'm pretty sure they will appreciate being able to right-click, and select dafny run, and with their custom arguments can choose which backend it would run on.

You can configure tasks in VS code to easily run a custom binary on the current active file.

Source/DafnyDriver/Commands/DafnyCli.cs

Test/c++/arrays.dfy

robin-aws

LGTM! I pushed a commit to add newlines to the cpp description as IMO it really improved the readability, and I say we should do that in general to all long command and argument descriptions.

You have a couple of legit test failures to deal with, but I'll happily re-approve once those are fixed.

robin-aws · 2023-10-11T20:22:10Z

Source/IntegrationTests/LitTests.cs

@@ -535,7 +543,7 @@ class MultiBackendLitCommand : ILitCommand {
    public (int, string, string) Execute(TextReader inputReader,
      TextWriter outputWriter,
      TextWriter errorWriter) {
-      var exitCode = new MultiBackendTest(inputReader, outputWriter, errorWriter).Start(arguments.Prepend("for-each-compiler"));
+      var exitCode = new MultiBackendTest(inputReader, outputWriter, errorWriter).Start(arguments);


I assume you found this because of actually running tests with DAFNY_INTEGRATION_TESTS_IN_PROCESS=true? Thanks for the fix, and we should add some singleton tests for that mode to protect against regressions (not as part of this PR)

robin-aws · 2023-10-11T20:23:37Z

Source/TestDafny/MultiBackendTest.cs

-      new string[] { "verify", options.TestFile! }.Concat(options.OtherArgs).ToArray());
-    var dafnyOptions = ((ParseArgumentSuccess)parseResult).DafnyOptions;
+  private async Task<int> ForEachCompiler(ForEachCompilerOptions options) {
+    var pluginParseResult = CommonOptionBag.PluginOption.Parse(options.OtherArgs.ToArray());


i'm pleased that at least this context supports plugins :)

… can be used with translate (dafny-lang#4601) ### Changes - Use subcommands instead of an argument for the various back-ends that can be used with `translate`, this allows each sub-command to get custom option. The syntax for using translate remains the same. - Remove `ICommandSpec`, which was a wrapper around `System.Commandline.Command` that made it difficult to introduce commands that did something different than run the entire Dafny pipeline, such as `dafny server`, `dafny format`, `dafny doc`, `dafny generate-tests`, `dafny find-dead-code`, `dafny merge-coverage-reports` - Previously `DafnyDriver` did some CLI argument processing, and some orchestrating of the various steps of the Dafny pipeline. It has been renamed to `DafnyPipelineDriver` and now only does the latter. `CommandRegistry` was previously doing part of argument processing, but is now doing all argument processing and has been renamed to `DafnyCli` - No longer build the standalone Dafny server executable ### Testing - This is a refactoring that's covered by existing tests - Tests that were testing properties the standalone language server process are now testing the Dafny CLI with the server command instead <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>

Fixes #4322 Depends on #4601 ### Changes - For C#, add the option `--outer-namespace`: `All generated code will be nested inside the outer namespace. Option can be specified multiple times for deeper nesting`. - For Java, add the option `--outer-package`: `All generated code will be nested inside the outer package. Option can be specified multiple times for deeper nesting`. - In some back-ends, the presence of a default module could be translated away, but this is troublesome when using an `--outer-namespace` in which the default module should also be placed. This PR lets the default module behave more like other modules when translating, so more `_module` ends up in the generated code. If we want to get rid of this, I suggest we don't add special casing for the default module, but instead try to avoid qualifying references more than needed during translation. ### Testing - Add test that verifies that all back-ends can run code when using `--outer-namespace` - Add tests for C#, Java and Javascript that checks that the code generated by these back-ends uses `--outer-namespac` when it is specified. <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>

keyboardDrummer added 12 commits October 2, 2023 12:48

Add back-end specific translate sub-commands

1c89b58

Stop using ICommandSpec and instead use native Command

05f71ac

Rename

231a2e7

Build passes

30489b5

Ran formatter

f3bfa67

Fixing bugs

0cb866e

Extract method TryLegacyArgumentParser

fdfec45

More fixes

7f87e47

Fixes

bc719c8

Fix static initializer cycle problem

bd752ee

Ran formatter

be44a56

Merge branch 'master' into backendCommand

d79cc5a

keyboardDrummer enabled auto-merge (squash) October 3, 2023 13:28

keyboardDrummer added 8 commits October 3, 2023 16:55

Fix two process tests

c59fe2f

Fix doc command

0b222c4

Merge branch 'backendCommand' of github.com:keyboardDrummer/dafny int…

b1f734c

…o backendCommand

Move testing code into dedicated testing class

7544817

Renames

e4a78a4

Refactoring

ff043bc

Two fixes

825a5bc

Fix tests

7216fe6

keyboardDrummer requested a review from robin-aws October 4, 2023 10:31

keyboardDrummer mentioned this pull request Sep 29, 2023

Allow specifying an outer namespace when translating #4591

Merged

keyboardDrummer added 2 commits October 4, 2023 15:21

Merge remote-tracking branch 'origin/master' into backendCommand

a48ed84

Update error docs

a1b6122

robin-aws reviewed Oct 4, 2023

View reviewed changes

keyboardDrummer added 4 commits October 5, 2023 11:11

Code review

d336729

Hide Rust command by default

f141a75

Merge branch 'master' into backendCommand

7c88809

Improve UX

a2b8fa5

Merge branch 'master' into backendCommand

e6379b0

keyboardDrummer requested a review from robin-aws October 6, 2023 12:15

keyboardDrummer and others added 2 commits October 11, 2023 15:46

Merge remote-tracking branch 'origin/master' into backendCommand

b8dcf76

Add newlines to cpp command description

9e3c2da

robin-aws previously approved these changes Oct 11, 2023

View reviewed changes

keyboardDrummer added 3 commits October 12, 2023 12:36

Merge remote-tracking branch 'origin/master' into backendCommand

bac2ca4

Readd fix

2f920c6

Fix trait legacy UI

edcd715

keyboardDrummer dismissed robin-aws’s stale review via edcd715 October 12, 2023 10:39

stefan-aws approved these changes Oct 12, 2023

View reviewed changes

keyboardDrummer merged commit b68e693 into dafny-lang:master Oct 12, 2023
18 checks passed

keyboardDrummer deleted the backendCommand branch October 12, 2023 11:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use subcommands instead of an argument for the various back-ends that can be used with translate #4601

Use subcommands instead of an argument for the various back-ends that can be used with translate #4601

keyboardDrummer commented Oct 3, 2023 •

edited

Loading

robin-aws Oct 4, 2023

keyboardDrummer Oct 5, 2023 •

edited

Loading

robin-aws Oct 5, 2023

MikaelMayer Oct 5, 2023

keyboardDrummer Oct 6, 2023 •

edited

Loading

MikaelMayer Oct 6, 2023

robin-aws Oct 6, 2023

keyboardDrummer Oct 7, 2023

keyboardDrummer Oct 7, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Oct 11, 2023

robin-aws Oct 11, 2023

Use subcommands instead of an argument for the various back-ends that can be used with translate #4601

Use subcommands instead of an argument for the various back-ends that can be used with translate #4601

Conversation

keyboardDrummer commented Oct 3, 2023 • edited Loading

Changes

Help output

Testing

Choose a reason for hiding this comment

keyboardDrummer Oct 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 7, 2023 • edited Loading

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Oct 3, 2023 •

edited

Loading

keyboardDrummer Oct 5, 2023 •

edited

Loading

keyboardDrummer Oct 6, 2023 •

edited

Loading

keyboardDrummer Oct 7, 2023 •

edited

Loading