无法通过推荐命令将Dafny编译为Python的问题求助

问题背景 #

尝试使用Dafny参考文档中的Python编译功能时，遇到两个错误：

• 执行dafny build --target:py A.dfy，报错：Dafny: Error: unknown switch: --target
• 执行旧命令dafny Hello.dfy -compileTarget:py，报错：Dafny: Error: Invalid argument "py" to option compileTarget

核心原因 #

Dafny的Python编译属于实验性功能，仅在特定版本中支持，且命令行参数随版本迭代有变化，你当前的Dafny版本可能不兼容文档里的命令格式。

解决步骤 #

• 检查并升级Dafny版本
  终端执行dafny --version查看当前版本。Python编译支持需要较新的预览版/正式版，若版本过低：

  • VS插件：在VS扩展市场搜索Dafny，安装最新版本；
  • 终端版：执行dotnet tool update dafny --global --prerelease升级到最新预览版。

• 使用对应版本的正确命令
  新版Dafny（2.6+）的正确编译命令为：

  dafny compile --target python A.dfy
  

  若仍报错，需添加实验性标志：

  dafny compile --target python --experimental A.dfy
  

• 确认依赖环境

  • 本地需安装Python 3.8及以上版本，且Python已加入系统PATH（终端执行python --version能正常返回版本号）；
  • 编译完成后若提示缺少运行时依赖，执行pip install dafny-runtime安装。

• VS中直接操作（更简便）
  若习惯用VS，确保Dafny插件为最新版，右键点击.dfy文件，选择「Compile to Python」即可完成编译，无需手动输入终端命令。

内容的提问来源于stack exchange，提问作者Theo Deep