2020-05-12 VSCODE+Dafny

Dafny是一款能进行分析验证的编程语言。

VS Code本身就有Dafny extension（在搜索界面有2个dafny相关的拓展，安装的是dafny而不是dafny-vscode），但是我安装总是失败，还不能完全确定是不是网络的原因。安装成功后，理应在vscode下方栏新增如下选项：

屏幕快照 2020-05-12 下午2.20.40.png

但是我这边却只有报错，有时候是CONNREJECT，有时候是request 什么codeLen没有任何反应。
最后，我的解决策略如下：

1. 在https://github.com/dafny-lang/dafny/releases 上下载二进制代码，有windows/macOS/ubuntu等系统对应的版本。这一步可能要挂vpn，至少我在没有vpn的windows上下载不下来。
2. VS Code中，先去左边栏里的extensions搜索dafny，点击install
3. 然后右下角会弹出一个框，问你是否install dafny，这个时候不用install

4. 点击左下角设置按钮，选择settings，在新出现的设置选项界面展开extensions，就可以看到里面有Dafny extension configuration选项了。

   
   屏幕快照 2020-05-12 下午2.29.22.png
5. 看到上图最下面的选项Base Path了吗？填入你第一步下载下来并解压了的dafny的路径，注意这里面提示了，需要包含DafnyServer.exe的那个文件夹。Mac也是类似的。
6. 然后就可以重开VS Code，打开一个dfy文件，底下就能看到本文第一张图片里看到的选项了。
   7.如果你看到这样的错误：没在xx文件夹下找到Z3，那你可以看看是不是自己下错了dafny版本，我最后还是在mac上下载的，但是下载了windows版本orz，我承认这个错误很蠢。。。但是没办法嘛，人有的时候就是会犯低级错误的哈哈哈。