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

Dafny plugin does nothing #504

Open
damienstanton opened this issue Oct 22, 2024 · 4 comments
Open

Dafny plugin does nothing #504

damienstanton opened this issue Oct 22, 2024 · 4 comments

Comments

@damienstanton
Copy link

The plugin installs and provides syntax highlighting, however none of the operations do anything and there is no output in the Dafny VSCode output pane. There are also no errors in the devtools.

The "activating extensions" dialog shows in the lower left of the status bar (shown in this screenshot) for 1-2 seconds, and then disappears. There doesn't appear to be any other output.

Screenshot 2024-10-22 at 07 17 09

My environment:

Apple M2
macOS 15.1 beta
dotnet 8.0.303
openjdk 23
@keyboardDrummer
Copy link
Member

I haven't seen this before. If you open something other than a .dfy file, do your VSCode extensions activate successfully?

If you look at the dropdown that in your screenshot reads "Dafny VSCode", is there any interesting information in other channels, such as "Extension Host" ?

@damienstanton
Copy link
Author

There's nothing except a log that the extension is associated with .dfy files (which is correct of course). I have several other extensions running on this machine and have not had any issues. I'll see if I can play with the configuration to discover what's going on.

@damienstanton
Copy link
Author

I figured it out. These values were somehow missing from the default config, highlighted in red with an error "value must be numeric".

Screenshot 2024-10-22 at 20 27 16

Once I set them to 0 and restarted both the extension host and the editor, everything now works.

Screenshot 2024-10-22 at 20 28 22

Given that I am on a beta OS, and that I've not seen this issue at all on my other machines, I'll close this for now.

@keyboardDrummer
Copy link
Member

Reopening since we could try to make the code robust against this issue

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants