Skip to content

Commit

Permalink
feat: no-verify for language server (#3732)
Browse files Browse the repository at this point in the history
Enable the --no-verify option that is already available for the command
line for the language server, for research
and teaching purposes.

<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>
  • Loading branch information
jtristan committed Mar 13, 2023
1 parent 527d49e commit 265c985
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 0 deletions.
1 change: 1 addition & 0 deletions Source/DafnyLanguageServer/ServerCommand.cs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ related locations
};

public IEnumerable<Option> Options => new Option[] {
BoogieOptionBag.NoVerify,
Verification,
GhostIndicators,
LineVerificationStatus,
Expand Down
3 changes: 3 additions & 0 deletions Source/DafnyLanguageServer/Workspace/Compilation.cs
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,9 @@ private async Task<DocumentAfterParsing> ResolveAsync() {

private async Task<DocumentAfterTranslation> TranslateAsync() {
var parsedCompilation = await ResolvedDocument;
if (!options.Verify) {
throw new OperationCanceledException();
}
if (parsedCompilation is not DocumentAfterResolution resolvedCompilation) {
throw new OperationCanceledException();
}
Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/no-verify-server.feat
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Added option --no-verify for language server

0 comments on commit 265c985

Please sign in to comment.