Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automatic Counter Example Quits DafnyServer #61

Open
davidstreader opened this issue Jun 30, 2020 · 6 comments
Open

Automatic Counter Example Quits DafnyServer #61

davidstreader opened this issue Jun 30, 2020 · 6 comments

Comments

@davidstreader
Copy link

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
Copy link
Member

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
Copy link
Author

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
Copy link
Author

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
Copy link
Author

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
Copy link
Member

fabianhauser commented Jul 1, 2020

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
Copy link
Author

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.

@fabianhauser fabianhauser changed the title Just starting to use dafny but DafnyServer process quit unexpectedly Automatic Counter Example Quits DafnyServer Jul 8, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants