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.

Sign up for GitHub

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

Jump to bottom

[Regression] Show counterexamples failing with "Counterexample request failed: TypeError: Cannot convert undefined or null to object" #492

Open
AlgorithmsAreCool opened this issue Sep 2, 2024 · 2 comments · May be fixed by dafny-lang/dafny#5847
Open

[Regression] Show counterexamples failing with "Counterexample request failed: TypeError: Cannot convert undefined or null to object" #492

AlgorithmsAreCool opened this issue Sep 2, 2024 · 2 comments · May be fixed by dafny-lang/dafny#5847

Comments

@AlgorithmsAreCool
Copy link

Dafny Extension v3.3.1

Version: 1.92.2
Commit: fee1edb8d6d72a0ddff41e5f71a671c23ed924b9
Date: 2024-08-14T17:29:30.058Z
Electron: 30.1.2
ElectronBuildId: 9870757
Chromium: 124.0.6367.243
Node.js: 20.14.0
V8: 12.4.254.20-electron.0
OS: Windows_NT x64 10.0.19045

Thank you all for this incredible tool!

When attempting to show counterexamples in VSCode, it now fails with an error popup that says Counterexample request failed: TypeError: Cannot convert undefined or null to object

I've confirmed that reinstalling extension v3.3.0 fixes the issue.

The output window only displays the following.

Language server: {"command":"C:\\Program Files\\dotnet\\dotnet.EXE","args":["c:\\Users\\alfred\\scoop\\apps\\vscode\\1.92.2\\data\\extensions\\dafny-lang.ide-vscode-3.3.1\\out\\resources\\4.7.0\\github\\dafny\\Dafny.dll","server","--verify-on:Change","--verification-time-limit:0","--cache-verification=0","--cores:9","--notify-ghostness:true","--notify-line-verification-status:true"]}
Dafny is ready

Unsure how to collect additional info but happy to help however i can.
@AlgorithmsAreCool
Copy link
Author

This seems to still be happening in v3.4.1 of the extension

@keyboardDrummer
Copy link
Member

This was broken by dafny-lang/dafny#5013, which changes the counterexample API provided by dafny server. I'm not sure why that API was updated. There were internal changes in that PR made to enable the dafny verify --extract-counterexample option, that possibly made it difficult not to update the dafny server API as well, I'm not sure.

We should consider reverting the dafny server counterexample API to what it was, or otherwise think about how we could visually display the new API.

@Dargones Dargones linked a pull request Oct 21, 2024 that will close this issue
Open
@keyboardDrummer keyboardDrummer mentioned this issue Oct 24, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Dafny server API for counterexamples Dargones/dafny
3 participants
@keyboardDrummer @AlgorithmsAreCool and others