Nested extern attribute creates stub with incorrect file name in Python #2963
Labels
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
lang: python
Dafny's Python transpiler and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Follow-up from #2952.
After #2952,
module {:extern "A.B.C"} A.B.C
works in Python, but creates an unnecessary and confusing stub namedA.B.C.py
(as opposed to where you actually implement the extern,A/B/C.py
). As clean up we should have the Python code generation not create this stub.The text was updated successfully, but these errors were encountered: