VS code 可以验证但不能运行 Dafny 代码 [英] VS code can verify but not run Dafny code

问题描述

我使用的是最新的 Dafny 和 VScode.但是在 macOS 11.5 上 Dafny 代码

I am using the latest Dafny and VScode. But on a macOS 11.5 The Dafny code

function method Size(t: Tree): nat
decreases t
{
    match t
       case Leaf => 1
       case Node(l,r) => Size(l)+ Size(r)
}
        
method Main() {
  var tl:Tree := Leaf;
  var tc:Tree := Node(Node(Leaf, Leaf),Leaf);
  assert Size(tl) == 1;
  assert Size(tc) == 3;
  print "  ",Size(tl),"  ",Size(tc), "\n";
} 

验证但当我尝试运行它时，弹出窗口告诉我您没有用于调试 Dafny 的扩展程序.我们应该在 Marketplace 中找到 Dafny 扩展吗?但后来在市场上找不到.

verifies but when I try to run it a popup tells me You don't have an extension for debugging Dafny. Should we find a Dafny extension in the Marketplace? but then can not find one in the marketplace.

对我做错了什么有任何想法吗?

Any ideas as to what I am doing wrong?

推荐答案

这个问题也有很多同学用 MacOS 发现的，所以跟我安装的没关系.但是，其中一名学生找到了解决方案.

This problem was also found by many students using MacOS, so is not to do with my installation. But, one of the students had the solution.

在 MacOS 上，Run 下拉菜单中的 Run without debugging 选项不起作用.您需要右键单击该文件(控制单击)，然后选择 Dafny: Compile and Run 选项.然后运行该文件.

On MacOS the option to Run without debugging on the dropdown menu from Run does not work. You need to right click on the file (control click) then take the Dafny: Compile and Run option. This then runs the file.

这篇关于VS code 可以验证但不能运行 Dafny 代码的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！