feat: python-module-name #5461
feat: python-module-name #5461
Conversation
Yup and that was intentional for the same reasons. Hence it would be better to know explicitly when a user was translating code with the intent to use it as a library, and warn/error if there's any code in the default module. But that can be an orthogonal improvement outside of the scope of this PR. |
There was a problem hiding this comment.
FYI we don't normally check in Dafny-generated files in the integration tests, but opted to do this anyway for now when we made the same changes for Go. There's an issue tracking the fact that we want to fix this though, and it should include these files as well once merged: #5399
| // will have their `.`s replaced with `_` before this code is executed, | ||
| // ex. module M.N --> "M_N", and will not hit this branch.) | ||
| // | ||
| // Nested externs currently CANNOT be used with python-module-name: |
There was a problem hiding this comment.
Thanks for the very detailed comment on this issue!
I think one of the factors making this worse is that {:extern} can be used either to say "this thing is implemented externally", or "this thing will be referenced by external code". In the latter case you're specifying the external name you want for the code you're generating, but in the former you're sometimes trying to declare the existing name for existing code. So whether python-module-name should apply to the extern name depends on the implicit use!
But to me that just means you're doing the right thing by not supporting either case for now - if your use cases can avoid it for now, that's the right call.
| // This is primarily here to exclude prefix modules | ||
| // (e.g. something like A.B that only appears in a module A.B.C { ... } declaration) | ||
| // since those can appear in multiple separately-compiled projects. | ||
| if (ModuleEmptyForCompilation(module)) { | ||
| continue; | ||
| } | ||
|
|
There was a problem hiding this comment.
Why remove this? Didn't it break the use case you were trying to use translation records with?
There's a DuplicateModules.dfy test case that should be broken by this change, perhaps the CI only worked because you hadn't merged the latest from master yet?
There was a problem hiding this comment.
Mistake, I'll add this back.
I reverted this commit: 4ce2f7e
That commit prevented writing files if they were empty.
However, Python code generation still generates imports for those files.
These imports aren't valid since the files don't exist.
I would bet that other languages have the same issue, but haven't tested this.
We'd need a fix for this, since the current state doesn't work.
Description
1
Add a
--python-module-nameoption to the (new) Dafny CLI.This option takes in a string that will be prefixed to translated module imports.
ex. If a module has a generated Python import statement
import MyModule,then translating with
--python-module-name=my_python_modulewill result in an import statement
import my_python_module.MyModule as MyModule.I intend that Smithy-Dafny will use this with
--python-module-name=[module_name].internaldafny.generated.2
Do not generate
import module_forSystem_.pyin the DafnyRuntime Python.Before this change
System_.pyin the DafnyRuntimePython generates this import. This removes that import.Two problems with this import:
module_.py. Havingimport module_prevents the DafnyRuntimeModule from being used on its own.import module_is an invalid import statement with module mode.module_will be located at[python_module_name].module_, and isn't able to be imported without qualifiers.An alternative to removing the import is to generate a
module_.pyin the DafnyRuntimePython. I don't know why DafnyRuntimePython doesn't have this file, so this was easier for me. I don't have an opinion on which approach happens; I'll defer to the Dafny team on the approach.3
Python: Do not generate import statements for empty modules.
"Empty modules" might come from prefixes of nested modules.
This is a follow-up to 4ce2f7e, which stopped generating empty modules.
How has this been tested?
Some tests in the directory above:
I've tested this with Smithy-Dafny-Python and the (WIP) Python MPL, and this behavior works as I'd expect.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.