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: CLI no longer prints helpful message if Z3 not found #5067

Closed
robin-aws opened this issue Feb 8, 2024 · 0 comments · Fixed by #5086
Closed

Regression: CLI no longer prints helpful message if Z3 not found #5067

robin-aws opened this issue Feb 8, 2024 · 0 comments · Fixed by #5086
Assignees
@keyboardDrummer
Labels
release-blocker Must be resolved before the next release

Comments

@robin-aws
Copy link
Member

Attempting to verify source without Z3 installed used to print a big helpful error message: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/DafnyMain.cs#L109

#4798 inadvertently broke this by having dafny verify use more common code with the language server, and as a result BoogieOnce is never actually called.

Discovered while getting #5060 to work, and I may be able to fix it there, but cutting this in case it doesn't fit in that scope.
@robin-aws robin-aws added the release-blocker Must be resolved before the next release label Feb 8, 2024
@keyboardDrummer keyboardDrummer self-assigned this Feb 8, 2024
@keyboardDrummer keyboardDrummer mentioned this issue Feb 14, 2024
Merged
keyboardDrummer added a commit that referenced this issue Feb 20, 2024
@keyboardDrummer
Make the error reporter for checking if Z3 is available, more consist…
3d4277d 
…ent (#5086)

Fixes #5067
### Description
Make the error reporter for checking if Z3 is available, more consistent
between the IDE and various CLI commands

### How has this been tested?
Updated CLI and IDE tests

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@keyboardDrummer keyboardDrummer

Labels
release-blocker Must be resolved before the next release
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Make the error reporter for checking if Z3 is available, more consistent keyboardDrummer/dafny
2 participants
@keyboardDrummer @robin-aws