forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 1
/
LanguageServer.cs
122 lines (108 loc) · 4.74 KB
/
LanguageServer.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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
using Microsoft.Extensions.Configuration;
using Microsoft.Extensions.Logging;
using OmniSharp.Extensions.LanguageServer.Server;
using Serilog;
using System;
using System.Collections.Generic;
using System.CommandLine;
using System.IO;
using System.Reflection;
using System.Text;
using System.Threading.Tasks;
using Microsoft.Dafny.LanguageServer.Language;
using Microsoft.Dafny.LanguageServer.Language.Symbols;
using Microsoft.Dafny.LanguageServer.Workspace;
using Microsoft.Extensions.DependencyInjection;
using OmniSharpLanguageServer = OmniSharp.Extensions.LanguageServer.Server.LanguageServer;
namespace Microsoft.Dafny.LanguageServer {
public class LanguageServer {
public static IEnumerable<Option> Options => new Option[] {
BoogieOptionBag.NoVerify,
ProjectManager.Verification,
GhostStateDiagnosticCollector.GhostIndicators,
GutterIconAndHoverVerificationDetailsManager.LineVerificationStatus,
LanguageServer.VerifySnapshots,
DafnyLangSymbolResolver.UseCaching,
ProjectManager.UpdateThrottling,
DeveloperOptionBag.BoogiePrint,
CommonOptionBag.EnforceDeterminism,
CommonOptionBag.UseJavadocLikeDocstringRewriterOption,
LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
}.Concat(DafnyCommands.VerificationOptions).
Concat(DafnyCommands.ResolverOptions);
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 static void ConfigureDafnyOptionsForServer(DafnyOptions dafnyOptions) {
dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, true);
dafnyOptions.PrintIncludesMode = DafnyOptions.IncludesModes.None;
// TODO This may be subject to change. See Microsoft.Boogie.Counterexample
// A dash means write to the textwriter instead of a file.
// https://github.com/boogie-org/boogie/blob/b03dd2e4d5170757006eef94cbb07739ba50dddb/Source/VCGeneration/Couterexample.cs#L217
dafnyOptions.ModelViewFile = "-";
}
public static async Task Start(DafnyOptions dafnyOptions) {
var configuration = CreateConfiguration();
InitializeLogger(configuration);
dafnyOptions = new DafnyOptions(dafnyOptions, true);
try {
Action? shutdownServer = null;
var server = await OmniSharpLanguageServer.From(
options => options.WithServices(s => s.AddSingleton(dafnyOptions))
.WithInput(Console.OpenStandardInput())
.WithOutput(Console.OpenStandardOutput())
.ConfigureConfiguration(builder => builder.AddConfiguration(configuration))
.ConfigureLogging(SetupLogging)
.WithUnhandledExceptionHandler(LogException)
// ReSharper disable once AccessToModifiedClosure
.WithDafnyLanguageServer(() => shutdownServer!())
);
// Prevent any other parts of the language server to actually write to standard output.
await using var logWriter = new LogWriter();
Console.SetOut(logWriter);
shutdownServer = () => server.ForcefulShutdown();
await server.WaitForExit;
}
finally {
Log.CloseAndFlush();
}
}
private static IConfiguration CreateConfiguration() {
return new ConfigurationBuilder()
.AddJsonFile("DafnyLanguageServer.appsettings.json", optional: true)
.Build();
}
private static void InitializeLogger(IConfiguration configuration) {
// The environment variable is used so a log file can be explicitly created in the application dir.
Environment.SetEnvironmentVariable("DAFNYLS_APP_DIR", Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location));
Log.Logger = new LoggerConfiguration()
.ReadFrom.Configuration(configuration)
.CreateLogger();
}
private static void LogException(Exception exception) {
Log.Logger.Error(exception, "captured unhandled exception");
}
private static void SetupLogging(ILoggingBuilder builder) {
builder
.ClearProviders()
.AddSerilog(Log.Logger);
}
private class LogWriter : TextWriter {
public override void Write(char value) {
Log.Logger.Verbose("Unexpected console output: {value}", value);
}
public override void Write(string? value) {
Log.Logger.Verbose("Unexpected console output: {value}", value);
}
public override Encoding Encoding { get; } = Encoding.ASCII;
}
}
}