-
Notifications
You must be signed in to change notification settings - Fork 261
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.
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
feat: Plugin support #1739
feat: Plugin support #1739
Conversation
Display the error on the first token of any program.
Can you say how this PR interacts with #1708 ? Does is replace it? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good so far. Is there a reason you didn't create a test for the language server?
} | ||
} | ||
}, new JsonSerializerOptions() { WriteIndented = true }); | ||
await File.WriteAllTextAsync(temp + ".runtimeconfig.json", configuration + Environment.NewLine); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the *.runtimeconfig.json
file necessary for dynamically loaded assemblies?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know, I just copied-pasted the code of @keyboardDrummer . I removed it and it works, thanks for reporting.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perfect. I guess you've copied this from @keyboardDrummer's code that test's the shutdown of the language server if the parent process quits. The difference to his implementation, is that you're creating a DLL that's loaded by a running process while his implementation is used to spawn a new process. However, I'm not sure if the *.runtimeconfig.json
file is required if the application is launched with the dotnet
command; it sure is when calling the executable directly.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this PR also support letting the language server show errors generated by existing backends, such as the error here? https://github.com/dafny-lang/dafny/blob/master/Source/Dafny/Compilers/Compiler-Csharp.cs#L2469
I think we should build one solution that enables error reporting both for existing and custom back-ends. What are your thoughts?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just flagging that I'm especially interested in making sure we're crystal clear on the API here - consider this a ad-hoc mechanism for saying "I'm making myself a required reviewer" :)
No good reason and plenty of good reasons to actually do this. I'm going to work on that. One of the big catch of a plugin is that it can theoretically write to standard output, which messes up the disagnostics for the LSP. For now, I'm thinking of putting a comment on the class that plugins need to extend, because error reporters directly print to the console and we don't want to change that I guess.
I agree. Since the compilers are going to be refactored in #1708, it's better to wait to delegate that mechanism there, and @cpitclaudel and I thought about using generic "plugins" arguments, from which both the Resolver phase and the Compiler phase are going to pull their extra phases; thus, it will be easy to define for every compiler an IRewriter (used in Resolver) that will take care of doing exactly what you want, and nothing will need to be changed on this PR.
Copy that, required reviewer ! Here are the pros and the cons of the current approach:
|
I'm not convinced there should be extra resolver phases. Why don't we only use the |
/// If the plugin defines no Configuration, then Dafny will instantiate every sub-class | ||
/// of Rewriter from the plugin, providing them with an ErrorReporter as the first and only argument. | ||
/// </summary> | ||
public abstract class Rewriter { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
New API looks good :)
@@ -2007,6 +2080,22 @@ class Induction_Visitor : BottomUpVisitor { | |||
} | |||
} | |||
} | |||
|
|||
class PluginRewriter : IRewriter { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How come this class and Plugins.Rewriter
had to be separate classes again?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A Dafny rewriter (IRewriter) can support more phases than a plugin rewriter (which only supports PostResolve)
Therefore, we need to encapsulate any plugin-defined Rewriter into the (more internal) Dafny IRewriter.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would have thought a single abstract class with some virtual methods marked as internal and some as public (the ones we want to expose) would have been sufficient. How come it's not?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would have been sufficient. However, it may not be a good practice for a plugin system because all the "internal" methods would still be in the Plugin namespace, exposed to anyone looking at the source code - which I expect from plugins writers since they need to have their plugin in sync with the Dafny source code.
I prefer to really split what we offer between two things, one for the plugin, and one for internal. That way, if we want to change how the internal work, we are not stuck by a public API that we can always re-route to the new constructs.
await SetUpPlugin(); | ||
} | ||
|
||
protected override string LibraryCode => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure what I prefer, but think we could also put this library code in a separate .cs file that's not included in the build but retrieved as a resource using assembly.GetManifestResourceStream(resourceName)
. That way you would at least get syntax highlighting and parse errors when editing the file.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Implemented.
protected DiagnosticsReceiver DiagnosticReceiver; | ||
protected string LibraryPath; | ||
|
||
private static readonly object PluginSync = new { }; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this used anywhere?
Source/Dafny/Plugin.cs
Outdated
class AutomaticConfiguration : Configuration { | ||
private Plugin(string path, string[] args) { | ||
pluginPath = path; | ||
assembly = Assembly.LoadFrom(pluginPath); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpick: I would even do this work in the Load
method and then pass the assembly to the constructor.
Also, consider using a record to remove the need for a constructor, like so:
public record Plugin(Assembly Assembly, string[] Args) {
public Configuration PluginConfiguration { get; init; } = LoadConfiguration(Assembly, Args);
public static Plugin Load(string pluginPath, string[] args) {
return new Plugin(Assembly.Load(pluginPath), args);
}
private static Configuration LoadConfiguration(Assembly assembly, string[] args) {
var rewriterTypes = CheckPluginForRewriters(assembly);
Configuration configuration = null;
foreach (var configurationType in GetConfigurationsTypes(assembly)) {
if (configuration != null) {
throw new Exception(
$"Only one class should extend Microsoft.Dafny.Plugins.Configuration from {assembly.Location}. Please remove {configurationType}.");
}
configuration = (Configuration)Activator.CreateInstance(configurationType);
if (configuration == null) {
throw new Exception($"Could not instantiate a {configurationType} from {assembly.Location}");
}
configuration.ParseArguments(args);
}
configuration ??= new AutomaticConfiguration(
rewriterTypes.Select(rewriterType =>
(ErrorReporter errorReporter) =>
Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray());
return configuration;
}
private static System.Type[] CheckPluginForRewriters(Assembly assembly) {
System.Type[] rewriterTpes = assembly.GetTypes().Where(t =>
t.IsAssignableTo(typeof(Rewriter))).ToArray();
// Checks about the plugin to be well-behaved.
if (!rewriterTpes.Any()) {
throw new Exception($"Plugin {assembly.Location} does not contain any Microsoft.Dafny.Plugins.Rewriter");
}
return rewriterTpes;
}
public static IEnumerable<System.Type> GetConfigurationsTypes(Assembly assembly) {
return assembly.GetTypes()
.Where(t => t.IsAssignableTo(typeof(Configuration)));
}
class AutomaticConfiguration : Configuration {
private Func<ErrorReporter, Rewriter>[] rewriters;
public AutomaticConfiguration(Func<ErrorReporter, Rewriter>[] rewriters) {
this.rewriters = rewriters;
}
public override Rewriter[] GetRewriters(ErrorReporter errorReporter) {
return rewriters.Select(funcErrorReporterRewriter =>
funcErrorReporterRewriter(errorReporter)).ToArray();
}
}
}
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great alternative. I like to put arguments to the class too. Note that it's Assembly.LoadFrom
, not Assembly.Load
.
…ang/dafny into resolving-plugin-support
…ang/dafny into resolving-plugin-support
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A bit more nitpicking from my side.
Source/Dafny/Plugin.cs
Outdated
/// The configuration provides the methods to parse command-line arguments and obtain Rewriters | ||
/// </summary> | ||
public record Plugin(Assembly Assembly, string[] Args) { | ||
public PluginConfiguration PluginConfiguration { get; init; } = LoadConfiguration(Assembly, Args); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note: init
is only necessary if you want that the default initializer can be replaced when creating a new Plugin
instance (using the object initializer syntax). For example, it allows doing this:
var plugin = new Plugin(assembly, args) {
PluginConfiguration = /* some custom configuration */
};
If that's not needed, you can remove the init
modifier.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the tip ! I did not know what this init was doing, so your explanation was very useful.
Source/Dafny/Plugin.cs
Outdated
|
||
public static IEnumerable<System.Type> GetConfigurationsTypes(Assembly assembly) { | ||
return assembly.GetTypes() | ||
.Where(t => t.IsAssignableTo(typeof(PluginConfiguration))); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For the sake of consistency within the same class (single letter identifiers), I'd use type
instead of t
as the identifier name.
Source/Dafny/Plugin.cs
Outdated
} | ||
|
||
private static System.Type[] CheckPluginForRewriters(Assembly assembly) { | ||
System.Type[] rewriterTpes = assembly.GetTypes().Where(t => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For the sake of consistency within the same class (single letter identifiers), I'd use type
instead of t
as the identifier name.
Source/Dafny/Plugin.cs
Outdated
} | ||
|
||
private static System.Type[] CheckPluginForRewriters(Assembly assembly) { | ||
System.Type[] rewriterTpes = assembly.GetTypes().Where(t => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it necessary to specify System.Type[]
explicitly here?
Source/Dafny/Plugin.cs
Outdated
pluginConfiguration ??= new AutomaticPluginConfiguration( | ||
rewriterTypes.Select<System.Type, Func<ErrorReporter, Rewriter>>((System.Type rewriterType) => | ||
(ErrorReporter errorReporter) => | ||
Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use (Rewriter)Activator.CreateInstance(rewriterType, new object[] { errorReporter })
instead. Alternatively, the LINQ statement .Cast<Rewriter>()
might be handy too.
|
||
namespace Microsoft.Dafny.LanguageServer { | ||
public static class DafnyLanguageServer { | ||
public static List<string> LoadErrors = new(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Expose this list as a property of type IReadOnlyList<string>
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Then I have to assign the whole property at once in LoadPlugins
, which mean I can't make LoadErrors
readonly. Is that ok?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can implement the property so it uses a backing field. Making the external API readonly, but the internal mutable. For example you can do this:
private static List<string> loadErrors = new();
public static IReadOnlyList<string> LoadErrors => loadErrors;
Source/Dafny/Plugin.cs
Outdated
} | ||
|
||
pluginConfiguration ??= new AutomaticPluginConfiguration( | ||
rewriterTypes.Select<System.Type, Func<ErrorReporter, Rewriter>>((System.Type rewriterType) => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the type arguments to Select
can be left out.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried to remove it several times (because the IDE suggests it to me), but every time I do, dotnet compiler says it needs that type.
…ang/dafny into resolving-plugin-support
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some nitpicking from my side
Source/Dafny/Plugin.cs
Outdated
|
||
pluginConfiguration ??= new AutomaticPluginConfiguration { | ||
Rewriters = | ||
rewriterTypes.Select<System.Type, Func<ErrorReporter, Rewriter>>((System.Type rewriterType) => |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The explicitly typed lambda expressions should be redundant due to the type arguments to Select
.
However, the requirement for the explicit type arguments might be a good sign that it's best to extract the projection into a separate method in terms of readability:
pluginConfiguration ??= new AutomaticPluginConfiguration {
Rewriters = rewriterTypes.Select(CreateRewriterFactory).ToArray()
};
return pluginConfiguration;
}
private static Func<ErrorReporter, Rewriter> CreateRewriterFactory(System.Type rewriterType) {
return errorReporter => (Rewriter)Activator.CreateInstance(rewriterType, new object[] { errorReporter });
}
I leave it up to you if you want to apply this change.
|
||
namespace Microsoft.Dafny.LanguageServer { | ||
public static class DafnyLanguageServer { | ||
public static IReadOnlyList<string> LoadErrors = new List<string>(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just to make sure that you didn't miss a small detail in my suggestion. The implementation I proposed was an expression-bodied getter-only property:
private static List<string> loadErrors = new();
public static IReadOnlyList<string> LoadErrors => loadErrors; // Mind the arrow here
This will effectively compile into something like this:
private static List<string> loadErrors = new();
public static IReadOnlyList<string> LoadErrors {
get {
return loadErrors;
}
}
The current implementation allows changing the value of LoadErrors
from outside the DafnyLanguageServer
class which I'd like to avoid.
Alternatively, to not change too much of your current implementation, you could also change the field into a property with a private setter:
public static IReadOnlyList<string> LoadErrors { get; private set; } = new List<string>();
|
||
namespace Microsoft.Dafny.LanguageServer { | ||
public static class DafnyLanguageServer { | ||
public static IReadOnlyList<string> LoadErrors = new List<string>(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpicking as of now, but I'd like to avoid (mutable) static fields within the language server as much as possible.
However, we may want to consider introducing a global state object for the language server in the future for such cases.
I just enabled auto-squash-and-merge. @camrein let me know if there is anything else I should change, else you can approve this PR. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fantastic work!
@@ -71,7 +71,7 @@ public class ShutdownTest { | |||
|
|||
// Wait for the language server to kill itself by waiting until it closes the output stream. | |||
await process.StandardOutput.ReadToEndAsync(); | |||
Thread.Sleep(300); // Give the process some time to die | |||
await Task.Delay(400); // Give the process some time to die |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not WaitForExitAsync
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know what this does but sometimes a test fail because the process did not die.
@keyboardDrummer ?
} | ||
|
||
protected void CleanupPlugin() { | ||
DafnyOptions.O.Plugins.RemoveAt(0); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does this part do?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When testing a plugin, it adds it to the DafnyOptions.
I remove it from the DafnyOptions after the a test class is finished.
This PR creates an extensible plugin structure, which is primarily used to provide Dafny with extra
Rewriter
s .It will discharge Dafny core developers by letting any Dafny developer to experiment with their own pipelines and rewritings without the need to modify Dafny core.
Namely:
Dafny pipeline
PluginRewriter
that extendsIRewriter
Plugin\Rewriter
that is wrapped by aPluginRewriter
.Plugin\Rewriter
is a class that plugins are going to extend.Microsoft.Dafny.Plugin
that takes care of loading assemblies and supply them with command-line arguments.Microsoft.Dafny.Plugins.Configuration
that plugins should extend, so that they can optionally handle command-line arguments, and especially override methods such asGetRewriters
.DafnyOptions
the optionplugin
, which consists of the path to a dll + optionally, after a comma, a list of space-separated arguments. I modified the help accordingly. This option can be repeatedly provided.DafnyOptions.O.Plugins
, or fail immediately if plugins cannot be loaded, or if their initialization fail. It will instantiate a single instance of typeMicrosoft.Dafny.Plugins.Configuration
which will be responsible for handling command-line arguments and providing the extraRewriter
s. If noConfiguration
is provided, Dafny will just try to instantiate all the Rewriters it will find. Kind of a lightweight plugin mechanism.Resolver
, when it gather all internalRewrite
classes, it now goes through all the plugins fromDafnyOptions.O.Plugins
and recover every plugin-defined Rewriter wrapped in PluginRewriter by calling GetRewriters on the plugin, and add them to the listrewriters
It does not check for correct version though, I'm not sure how we should approach that, except to add a mention in the README.mdPluginsTest.cs
in DafnyPipeline.Test that verifies it can load a dummyRewriter
(credits to @keyboardDrummer for the code to do so with the CSharpCompiler which I heavily copied) and it is correctly called during resolution. It also tests plugins without Configuration (automatically loaded)Dafny language server
Token.NoToken
DafnyLanguageServer
, namely--dafny:plugin:0=
which serves the same purpose as the/plugins:
option of Dafny above. This option can be launched in VSCode by adding"dafny.languageServerLaunchArgs": ["--dafny:plugins=absolute_path_to_plugin.dll"]
to thesettings.json
Note: We will be able to build on top of this PR to use the same option to recover compilers, by adding a method
GetCompiler
orGetCompilers
to the classConfiguration
.Things to know when reviewing this PR
PostResolve
was renamedPostResolveIntermediate
because many things happen after the originalPostResolve
in the resolver. A newPostResolve
hook now really happens at the end of the resolverPlugin\Rewriter.cs
andPlugin\Configuration.cs
clearly describe what API we would provide to customers (@robin-aws it should be crystal clear)PluginsTest
, one in DafnyPipeline.Test and two other in DafnyLanguageServer.Test. I did not find where I could merge the library loading mechanism because they don't have a test project in common, so these methods are duplicated. I think this is fine, we might want to do other experiments with external resolvers tied to DanfyLanguageServer.PR that fixes the plugin argument parsing so that it's simple: #1817