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

Guarantee same diagnostics between verify and server commands #3109

Open
keyboardDrummer opened this issue Nov 24, 2022 · 3 comments
Open

Guarantee same diagnostics between verify and server commands #3109

keyboardDrummer opened this issue Nov 24, 2022 · 3 comments
Assignees
@keyboardDrummer
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests misc: tests New tests or tutorials part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Nov 24, 2022 •
edited
Loading

Add a test that verifies dafny server produces the same SMTLib as dafny verify
@keyboardDrummer keyboardDrummer added part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) misc: tests New tests or tutorials labels Nov 24, 2022
@keyboardDrummer keyboardDrummer mentioned this issue Mar 30, 2023
Closed
@keyboardDrummer keyboardDrummer mentioned this issue May 19, 2023
Open
@keyboardDrummer keyboardDrummer self-assigned this Aug 8, 2023
@robin-aws
Copy link
Member

Lots of things

LOL

Is making verification consistent in scope?

@keyboardDrummer
Copy link
Member Author

keyboardDrummer commented Oct 17, 2023 •
edited
Loading

Lots of things

LOL

Fixed 😅

Is making verification consistent in scope?

Was not but is now :)

@keyboardDrummer
Copy link
Member Author

This has mostly been resolved by #4798 and #5008

I wonder what we can further do to guarantee same generated SMT between server and CLI

@keyboardDrummer keyboardDrummer added during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program priority: next Will consider working on this after in progress work is done priority: not yet Will reconsider working on this when we're looking for work kind: language development speed Slows down development of Dafny the language, flaky tests and removed priority: next Will consider working on this after in progress work is done priority: not yet Will reconsider working on this when we're looking for work during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program labels Apr 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@keyboardDrummer keyboardDrummer

Labels
kind: language development speed Slows down development of Dafny the language, flaky tests misc: tests New tests or tutorials part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@keyboardDrummer @robin-aws