Skip to content
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

Python Syntax Error: For Loop with Set Modulus Bound #4007

Closed
alex-usher opened this issue May 15, 2023 · 0 comments · Fixed by #4015
Closed

Python Syntax Error: For Loop with Set Modulus Bound #4007

alex-usher opened this issue May 15, 2023 · 0 comments · Fixed by #4015
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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

Comments

@alex-usher
Copy link

Dafny version

4.1.0

Code to produce this issue

method Main() {
    for i := 0 to |(set x : int | 0 <= x < 3 :: x)| {
        var a := 1;
    }
}

Command to run and resulting output

$ dafny /compile:4 /compileTarget:py main.dfy
Dafny program verifier finished with 1 verified, 0 errors
Wrote textual form of target program to main-py/main.py
Additional target code written to main-py/_dafny.py
Additional target code written to main-py/System_.py
Additional target code written to main-py/module_.py
Running...

Traceback (most recent call last):
  File "main-py/main.py", line 7, in <module>
    import module_
  File "main-py/module_.py", line 21
    hi0_: intdef iife0_():
                 ^^^^^^
SyntaxError: invalid syntax

What happened?

Compiling and running the above program for the Python backend verified and produced an output file, but when running Python over the output file, the syntax error is thrown and the program aborts. This occurs when the loop is non-empty and the bound is a modulus over a set comprehension. I would expect the behaviour to follow the other backends, which run successfully.

What type of operating system are you experiencing the problem on?

Linux, Mac

@alex-usher alex-usher added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 15, 2023
@fabiomadge fabiomadge added part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: python Dafny's Python transpiler and its runtime labels May 15, 2023
keyboardDrummer pushed a commit that referenced this issue May 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label 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
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants