search

DafnyVSCode / Dafny-VSCode

Dafny 2 for Visual Studio Code (Legacy)
https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode-legacy
MIT License
18 stars 12 forks source link

Automatic Counter Example Quits DafnyServer #61

Open davidstreader opened 4 years ago

davidstreader commented 4 years ago

Hi Running Macos 10.14.6. Loaded VSCode and Dafny all worked well for some hours. Next day restarted VSCode and opened Dafny file. but server not found so I went to SETTINGs and added the _Absolute path to the DafnyServer.exe binary and then the file was automatically checked. But alas now two error messages keep flashing DafnyServer process quit unexpectedly; .. Restart succeeded any ideas?

Not sure if its relevant but have a warning Please use a workspace (File or Folder) ..

fabianhauser commented 4 years ago

Hi @davidstreader

This could be related to Please use a workspace (File or Folder) - the current plugin does not work well with single files. Could you try opening the whole folder (File->Open Folder)?

Could you also check which mono version you have?

davidstreader commented 4 years ago

Hi I am new to this. So starting from scratch I Add a workspace folder then add a new file and now am told

Error - 5:59:11 AM] Request textDocument/completion failed. Message: Request textDocument/completion failed with message: Cannot read property 'getText' of undefined Code: -32603

The only referance to mono I can find is: Dafny: Mono Executable Mono executable with absolute path. Only necessary if mono is not in system PATH (you'll get an error if that's the case). Ignored on Windows when useMono is false.

but I do not know which mono version (if any) I am using.

davidstreader commented 4 years ago

I removed the old version of visual studio code and re downloaded it. Then added a new workspace and a new file that when I saved it as two.dfy the same errors kept flashing.

davidstreader commented 4 years ago

deleated ~/.vscode restarted VSCode > new workspace add file and VSCode gets stuck displaying the first error despite having corrected it and having saved the file with the corrections. image

Originally this worked just fine so I assume that there is something left on my machine How do I do a clean restart other than by >rm -r ~/.vscode and then restarting VSCode? Am I doing something really silly because at the moment I am at a loss as to how to progress.

kind regards david

fabianhauser commented 4 years ago

No worries, the current stable version of the plugin is a bit buggy. We are currently working on a new version (Preview), but that doesn't yet work on macOS I'm afraid. (You did install the Stable Plugin "Dafny", right?)

Could you try installing the newest Mono version from https://www.mono-project.com/download/stable/ ?

How do I do a clean restart other than by >rm -r ~/.vscode and then restarting VSCode?

That should be sufficient, the extension does not touch anything outside of the extension folder in there...

davidstreader commented 4 years ago

Sorry for delay. Starting teaching Dafny next week so bit of a panic. Our problem was solved by turning off automatic counter example image

This is a shame as it looked like a useful feature.