Search code examples
dafnycode-translation

Cannot translate from Dafny to Python using recommended "dafny build --target:py A.dfy"


I am trying to use the Dafny-to-Python compiler that is suggested in Dafny's reference (25.7.7): http://dafny.org/dafny/DafnyRef/DafnyRef.html#2577-python

However, I cannot run the first step for it in the terminal: dafny build --target:py A.dfy, since I get the error: Dafny: Error: unknown switch: --target. I use Use /help for available options as they suggest, but have no idea on how to solve.

Just in case, I also attempted using the old version of the command (see 25.8.11. in the same reference): dafny Hello.dfy -compileTarget:py but then got message Dafny: Error: Invalid argument "py" to option compileTarget.

Any idea? Note that the authors themselves clearly state that The Dafny-to-Python compiler is still under development.

PS: I usually use Dafny in Visual Studio and not in the terminal, so maybe I lack some kind of library or something.


Solution

  • Neither the new CLI nor the Python compiler are supported by the very outdated version of Dafny you are using. You are presumably not using the correct VS Code extension, so I would start there. As of today, this should install 3.10.0 at /Users/$USER/.vscode/extensions/dafny-lang.ide-vscode-3.0.3/out/resources/3.10.0/github/dafny/Dafny.dll. To see how to use the dll, try hitting F5 with a Dafny file opened in VS Code. The Python compiler is complete and passes all tests these days.