overturetool
Support Isabelle code generation
As above, the Server has been enhanced slightly to deal with "unknown" LSP method invocations. These are dispatched via a special RPC handler and directed to the (LSPX) workspace manager. The manager registers additional analysis plugins, as directed by a property called lspx.plugins, and the registry has a new method to identify any registered plugins that can process a given LSP method name. The plugin is then completely responsible for handling the new method - RPCRequest input; RPCResponse(s) output.
That said, the easiest way to integrate Leo's Isabelle translation is probably to add a new languageId to the existing "slsp/translate" method and use that to invoke the ISAPlugin. When the integration is more mature, we can introduce new LSP methods.
I think the "experimental" section of the "initialize" response should probably include a section that is generated by each loaded plugin. That way we add new features and communicate with the Client, without changing the "framework" on the Server.
The experimental section support above is now available in "development". For example, the CTPlugin now has a method like this:
@Override
public JSONObject getExperimentalOptions()
{
return new JSONObject("combinatorialTestProvider", new JSONObject("workDoneProgress", true));
}
So when we know what options we want to add for Isabelle support, they can be added via the plugin, rather than by changing the Server itself.
Do we want the options to be set at startup or should they be changeable between each invocation?
It's useful to allow plugins to set static capabilities. They can always send "registerCapability" messages themselves if we want it to be more dynamic?
A button has been added for translate to Isabelle on the client side (development branch) with the language id: "isabelle"
Done, however the jars are not updated, so you will need to do that manually
Hmm... I've installed the 1.2.2 VSIX, but I'm not seeing any Isabelle options? :-( Is it supposed to be at the folder/project level or the per-file level? All I can see are the translate to LaTeX or Word options.
The good news is that it looks like the annotationPaths and JVMArguments settings give us the Java process settings that we need. So the folder settings.json is like this:
{
"vdm-vscode.debug.experimentalServer": false,
"vdm-vscode.highPrecision": false,
"editor.codeLens": true,
"vdm-vscode.annotationPaths": "/home/nick/.vscode/vdm2isa-4.4.4-SNAPSHOT-211019.jar",
"vdm-vscode.JVMArguments": "-Dlspx.plugins=plugins.ISAPluginSL"
}
is the server sending a translate to isabelle capability as with latex, word, etc.? If not, the button will not show
It's sending:
"experimental":
{
"translateProvider":
{
"languageId":
[
"latex",
"word",
"coverage",
"graphviz",
"isabelle"
],
"workDoneProgress": false
},
"dapServer":
{
"port": 8001
},
"combinatorialTestProvider":
{
"workDoneProgress": true
},
"proofObligationProvider": true
}
Looks like you're not adding Isabelle in this constructor: https://github.com/jonaskrask/vdm-vscode/blob/0b154cceb72a9801a641e2ccad14364accafad12/src/SpecificationLanguageClient.ts#L33
This now seems to work, thanks! By using the settings.json above, and Leo's jar, I was able to translate a simple pair of modules to Isabelle :-)
Can we include the jar from Leo in the extension? In either case, it would be nice if the server discovers if the jar is there and only includes the isabelle translate provider as a capability if it is there. Otherwise, the button will be displayed, but won't function properly.
I'm not sure what state the Isabelle translation is in at the moment, we should check that with Leo. The second problem is that this is a plugin (server capability extension) rather than a library. We were going to come up with a way to both identify plugin jars and set the -Dlspx.plugins property in a friendly way? Lastly, the "isabelle" languageId is currently hard-wired into the Server experimental translateProvider response. Plugins can add their own response entries, but not change existing ones... which might be more flexible. Then Leo's plugin could announce itself, if it was configured.
The ISA plugin currently sets an experimental option called "isabelle" with the value "server-option" :-) Really it ought to somehow edit or add a translateProvider entry.
Ahh yes, that's true, forgot about that. I see, it would be nice though if plugins could contribute to the existing entries. Otherwise, plugins will have to be supported a bit awkwardly if they contribute to the existing features (e.g. a new translation).
Yes. If we pass the "standard" options to the plugins, they can edit/extend them and replace the standard ones. It should be easy enough to implement.
I've just pushed something to do this to "development". If (and only if) the ISAPlugin is on the path and -Dlspx.plugins includes it, then it will edit itself into the translateProvider language list. I've pushed a change to Leo's code to do this... so I'll email him separately to let him know he needs to pull :-)