-
Notifications
You must be signed in to change notification settings - Fork 257
/
ServerCommand.cs
87 lines (74 loc) · 2.9 KB
/
ServerCommand.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
using System.Collections.Generic;
using System.CommandLine;
using System.CommandLine.Invocation;
using System.Linq;
using DafnyCore;
using Microsoft.Boogie;
using Microsoft.Dafny.LanguageServer.Workspace;
namespace Microsoft.Dafny.LanguageServer;
public class ServerCommand : ICommandSpec {
public static readonly ServerCommand Instance = new();
private ServerCommand() {
}
static ServerCommand() {
DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u);
DooFile.RegisterNoChecksNeeded(
Verification,
GhostIndicators,
LineVerificationStatus,
VerifySnapshots
);
}
public static readonly Option<bool> GhostIndicators = new("--notify-ghostness",
@"
(experimental, API will change)
Send notifications that indicate which lines are ghost.".TrimStart());
public static readonly Option<VerifyOnMode> Verification = new("--verify-on", () => VerifyOnMode.Change, @"
(experimental)
Determine when to automatically verify the program. Choose from: Never, OnChange or OnSave.".TrimStart()) {
ArgumentHelpName = "event"
};
public static readonly Option<bool> LineVerificationStatus = new("--notify-line-verification-status", @"
(experimental, API will change)
Send notifications about the verification status of each line in the program.
".TrimStart());
public static readonly Option<uint> VerifySnapshots = new("--cache-verification", @"
(experimental)
0 - do not use any verification result caching (default)
1 - use the basic verification result caching
2 - use the more advanced verification result caching
3 - use the more advanced caching and report errors according
to the new source locations for errors and their
related locations
".TrimStart()) {
ArgumentHelpName = "level"
};
public IEnumerable<Option> Options => new Option[] {
BoogieOptionBag.NoVerify,
Verification,
GhostIndicators,
LineVerificationStatus,
VerifySnapshots,
DeveloperOptionBag.BoogiePrint,
CommonOptionBag.EnforceDeterminism,
CommonOptionBag.UseJavadocLikeDocstringRewriterOption
}.Concat(ICommandSpec.VerificationOptions).
Concat(ICommandSpec.ResolverOptions);
public Command Create() {
return new Command("server", "Start the Dafny language server");
}
public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
ConfigureDafnyOptionsForServer(dafnyOptions);
}
public static void ConfigureDafnyOptionsForServer(DafnyOptions dafnyOptions) {
dafnyOptions.RunLanguageServer = true;
dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, true);
dafnyOptions.PrintIncludesMode = DafnyOptions.IncludesModes.None;
dafnyOptions.ProverOptions.AddRange(new List<string>()
{
"O:model_compress=false", // Replaced by "O:model.compact=false" if z3's version is > 4.8.6
"O:model.completion=true",
"O:model_evaluator.completion=true"
});
}
}