Standard lib support in dafny server
#4770
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…into standardLibServer
MikaelMayer
reviewed
Nov 15, 2023
Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
Outdated
Show resolved
Hide resolved
| RootFiles = DetermineRootFiles(); | ||
| var diagnosticsCopy = staticDiagnostics.ToImmutableDictionary(k => k.Key, | ||
| kv => kv.Value.Select(d => d.ToLspDiagnostic()).ToImmutableList()); | ||
| updates.OnNext(new FoundFiles(Project, RootFiles!, diagnosticsCopy)); |
There was a problem hiding this comment.
Can you please explain me in a few sentences why these lines? Or add a comment?
MikaelMayer
approved these changes
Nov 17, 2023
| @@ -4,7 +4,9 @@ Dafny program verifier finished with 1 verified, 0 errors | |||
| Dafny program verifier finished with 1 verified, 0 errors | |||
| StandardLibraries_Errors.dfy(20,29): Error: module DafnyStdLibs does not exist (position 0 in path DafnyStdLibs.Wrappers) | |||
| 1 resolution/type errors detected in StandardLibraries_Errors.dfy | |||
| *** Error: Cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True | |||
| CLI: Error: cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True | |||
There was a problem hiding this comment.
Any way to remove the ":" between "CLI" and "Error" to avoid colon repetition?
There was a problem hiding this comment.
There's an existing method:
public string ErrorToString(ErrorLevel header, IToken tok, string msg) {
return $"{tok.TokenToString(Options)}: {header.ToString()}: {msg}";
}
that creates the double colon. We could remove the first one.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
dafny serverlibrary = [..]indfyconfig.tomltodafny serverdafny serverand other commands.dafny serveronly publishes notifications for Uris owned by a particular project. A project owns a Uri if it is the closest project to that Uri and it includes it.new DafnytoDafnyFile.CreateAndValidate, so it's more clear that it contains logic.DafnyFileso it reports errors using anErrorReporterinstead of stdio, which makes it reusable for the language server.IllegalDafnyFileto handle common scenarios.Lazy<IdeState>inProjectManagerwithIdeStateHow has this been tested?
dafny serverdafny serverdafny serverBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.