-
Notifications
You must be signed in to change notification settings - Fork 257
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🐍
Description
1
Add a
--python-module-name
option 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_module
will 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_.py
in the DafnyRuntime Python.Before this change
System_.py
in 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_.py
in 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.