Allow specifying an outer namespace when translating #4591

keyboardDrummer · 2023-09-29T15:32:14Z

Fixes #4322

Changes

Add the option --outer-namespace: Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.

Testing

Add test that verifies the behavior of --outer-namespace for C#, Java, Go, Python and JavaScript
For Python, modules are currently (already before this PR) emitted using a flat directory structure, even though more idiomatic might be to have every module define a folder, and put the module contents in __init__.py

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

Test/comp/globalNamespace/globalNamespaceRunConfig.toml

Source/DafnyCore/Plugins/IExecutableBackend.cs

Source/TestDafny/MultiBackendTest.cs

robin-aws

Mostly looks great, and nice that the actual implementation is pretty simple (especially compared to #4601 :)

Looks like this is just for Java and C#, which is fine for now, but will will need the other backends at some point. Make sure we either keep #4322 open or cut fresh issues for the remaining backends. The PR description is also a bit out of date.

Test/comp/ExternJavaString.dfy

Source/DafnyCore/Options/CommonOptionBag.cs

Source/DafnyCore/Options/DafnyProject.cs

robin-aws · 2023-10-12T15:50:05Z

Source/IntegrationTests/LitTests.cs

@@ -239,7 +239,7 @@ public class LitTests {
              return false;
            }

-            if (arguments.Any(arg => arg is "/compile:3" or "/compile:4" or "run" or "translate")) {
+            if (arguments.Any(arg => arg is "/compile:3" or "/compile:4" or "run")) {


This doesn't seem right to me, I added "translate" because there were important backend-specific tests that weren't being run for all backends before that.

there were important backend-specific tests that weren't being run for all backends before that.

Are you saying there were tests using dafny translate that you converted to use %testDafnyForEachCompiler?

I doubt that because I don't think you can test dafny translate without back-end specific code.

No I couldn't convert them to %testDafnyForEachCompiler as you say, but I did manually add missing backend cases. https://github.com/dafny-lang/dafny/blob/master/Test/comp/separate-compilation/usesTimesTwo.dfy for example.

The name NeedsConverting() is a bit out of date, since the idea is just to identify tests that use backends but don't test all backends.

What's the use of adding // NONUNIFORM: using dafny translate to all tests that exercise dafny translate ?

I thought NONUNIFORM meant you are consciously only testing some back-ends, but now you're suggesting it will mean that you're not using %testDafnyForEach...

For run you commonly should be able to use %testDafnyForEachCompiler, so I think it makes sense there.

You can do that by looking for dafny translate !

The idea was to have // NONUNIFORM on all tests that don't automatically pick up new compilers, regardless of why. We could modify https://github.com/dafny-lang/dafny/blob/master/.github/workflows/msbuild.yml#L59-L60 to look for dafny translate as well if you want.

The idea was to have // NONUNIFORM on all tests that don't automatically pick up new compilers, regardless of why

What's the use? The reason you gave was that so you can "periodically audit the non-uniform tests and at least manually add new backends", but you don't need this semantic comment for that. Any test that specifies a target, either using --target, or using dafny translate, is non-uniform.

What I think is useful, is to complain about usages of dafny run, dafny build or dafny test that don't use --target, because they are uniform and could be tested against all back-ends, so it's wasted tested opportunity not to do so.

btw, do you know why a file like this one https://github.com/dafny-lang/dafny/blob/master/Test/c%2B%2B/extern.dfy#L1 isn't flagged by the check?

// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t"

I don't offhand, I'll look into it separately from this PR. And that means for now I won't object to this change. :)

After offline conversation I realize this is a good change - // NONUNIFORM should only be used for tests of backend-specific behaviour, like ExternJavaString.dfy. as part of my action item I'll remove the tag from tests like that.

Test/comp/globalNamespace/globalNamespaceRunConfig.toml

…to translatePrefix

keyboardDrummer · 2023-10-16T11:43:15Z

Switched back to a unified option for all back-ends, since the new implementation guarantees a unified interface for all back-ends.

…to translatePrefix

robin-aws · 2023-10-16T15:49:47Z

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -171,6 +183,17 @@ public abstract class IExecutableBackend {
  /// </summary>
  public abstract void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram);

+  public static readonly Option<string> OuterModule =
+    new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.");


Suggested change

new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.");

new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting.");

That last sentence is a leftover from the previous design AFAICT.

It was not. Doesn't it help to indicate which module will be the outermost one?

…ors, to work with C++ (::, ::, ->) and JS (_, ., .) well

keyboardDrummer requested a review from robin-aws September 29, 2023 15:32

robin-aws mentioned this pull request Oct 4, 2023

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

Merged

robin-aws reviewed Oct 4, 2023

View reviewed changes

Test/comp/globalNamespace/globalNamespaceRunConfig.toml Outdated Show resolved Hide resolved

Source/DafnyCore/Plugins/IExecutableBackend.cs Outdated Show resolved Hide resolved

Source/TestDafny/MultiBackendTest.cs Outdated Show resolved Hide resolved

keyboardDrummer enabled auto-merge (squash) October 5, 2023 11:24

keyboardDrummer requested review from robin-aws October 5, 2023 13:20

robin-aws requested changes Oct 12, 2023

View reviewed changes

Enable outer modules for C# and Java

6801e50

keyboardDrummer force-pushed the translatePrefix branch from 70581d2 to 6801e50 Compare October 13, 2023 13:05

keyboardDrummer added 10 commits October 13, 2023 15:13

Fix parser

7530350

Add deleted tests

c0ec305

Delete tests that don't exercise the feature

869f434

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

4b713dc

Fix NRE issue

e462de7

Merge branch 'master' into translatePrefix

f1c2f4e

Fix NSE

1af41f8

Switch to --outer-module option

30cf7d1

Merge branch 'translatePrefix' of github.com:keyboardDrummer/dafny in…

dba4c44

…to translatePrefix

Merge branch 'master' into translatePrefix

b70aace

keyboardDrummer added 3 commits October 16, 2023 14:30

Run formatter and add missing tests

2dd7299

Fix NRE

b724f66

Merge branch 'translatePrefix' of github.com:keyboardDrummer/dafny in…

660198a

…to translatePrefix

robin-aws reviewed Oct 16, 2023

View reviewed changes

keyboardDrummer added 5 commits October 17, 2023 10:44

Differentiate between module, static class and instance class separat…

55306f6

…ors, to work with C++ (::, ::, ->) and JS (_, ., .) well

Merge branch 'master' into translatePrefix

9796715

Customize module separators for Python and Go

a6150e2

Fix

deba271

Generate package files for Python

6f97cfc

keyboardDrummer requested a review from robin-aws October 17, 2023 12:48

keyboardDrummer added 3 commits October 17, 2023 15:39

Python, every module is a package

58a9275

Python fixes

84a4e74

Fix test so they do not abuse regex

2607ebf

robin-aws approved these changes Oct 17, 2023

View reviewed changes

Merge branch 'master' into translatePrefix

ec6f01b

keyboardDrummer merged commit ba3bac3 into dafny-lang:master Oct 17, 2023
18 checks passed

keyboardDrummer deleted the translatePrefix branch October 17, 2023 22:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow specifying an outer namespace when translating #4591

Allow specifying an outer namespace when translating #4591

keyboardDrummer commented Sep 29, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Oct 12, 2023

keyboardDrummer Oct 13, 2023 •

edited

Loading

robin-aws Oct 13, 2023

keyboardDrummer Oct 13, 2023

keyboardDrummer Oct 13, 2023 •

edited

Loading

robin-aws Oct 16, 2023

keyboardDrummer Oct 17, 2023 •

edited

Loading

keyboardDrummer Oct 17, 2023 •

edited

Loading

robin-aws Oct 17, 2023

robin-aws Oct 17, 2023

keyboardDrummer commented Oct 16, 2023

robin-aws Oct 16, 2023

keyboardDrummer Oct 17, 2023

	new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.");
	new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting.");

Allow specifying an outer namespace when translating #4591

Allow specifying an outer namespace when translating #4591

Conversation

keyboardDrummer commented Sep 29, 2023 • edited Loading

Changes

Testing

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 13, 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 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 17, 2023 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer Oct 17, 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 commented Oct 16, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Sep 29, 2023 •

edited

Loading

keyboardDrummer Oct 13, 2023 •

edited

Loading

keyboardDrummer Oct 13, 2023 •

edited

Loading

keyboardDrummer Oct 17, 2023 •

edited

Loading

keyboardDrummer Oct 17, 2023 •

edited

Loading