LSP Plugin Writers Guide

We talked about plugins for VDMJ, so I'm guessing an LSP plugin is the same idea in LSP. So the LSP Plugin Writer's Guide explains that?

Basically, yes. As with VDMJ, plugin here means an "Analysis Plugin".

This was also mentioned in the VDMJ HLD, I think?

Well, that's part of it yes. The idea is that an "analysis" is a separate phase of processing that a VDM specification can be subject to. Some analyses are built-in, like the syntax and type checking; some are written externally and added as plugins in separate jars.

But didn't this have something to do with the class mapping idea in the HLD?

That is true for the main analyses, like syntax, type checking, the interpreter and the PO generator. Those things have specialized AST classes that are mapped from somewhere else (ultimately, from the parser). But an analysis can work with the existing classes.

It might help if you could give me a realistic example?

Okay, so let's say that we have an idea of how to do some sophisticated checking that, say, enables complex VDM expressions to be simplified. That would be a useful thing to have, and it could perhaps provide hints as you were writing a specification.

So you'd package this into a plugin somehow?

Yes.

And it would be an analysis plugin?

Yes, because it's adding some sophisticated checking to your specification. But at the other end of the spectrum, an analysis plugin could just do a spell check of the variables or make recommendations about style.

Okay, so how does this fit with class mapping?

Well, a sophisticated analysis is much more likely to want its own specialized classes, mapped from somewhere else. A simple spell checker would not need to do that. I know it's a strange idea, but it is explained in this guide.

Okay, I'll live with that. So how is this guide structured?

It has four major sections, starting with the usual overview, though this one is important because it explains how plugins fit into the architecture of the language server, and how they process events.

An event here would be... ?

It could be the user typing a key to change a file; or them saving a file; or starting the checking process etc. All of the possible events are listed in an appendix to the guide.

Okay. And what comes after the overview?

Various protocol exchanges are described, for how the IDE and the server/plugins react. The idea is to show people how the system usually works, so that they can see how they could hook into something to do their own processing.

Hook into?

Plugins register to handle various event types. So even if the main type check plugin is handling CheckPrepareEvents, yours can handle it too and use it to prepare for its own checking phase. Event subscribers are invoked in a well defined priority order.

Okay, that sounds useful. What's after that?

Section 3 goes into much more detail about how to write a plugin in Java. There is an example plugin in the "examples/lspplugin" folder of VDMJ, which you can play with to see what happens. The example includes all of the important things that you can do from a plugin, like creating a "code lens" and contributing a command to the interpreter console, as well as reacting to events and raising messages for display on the UI.

So it sounds like a plugin can really do a lot of things, they're not just background processes that you hardly notice.

That's right. And note that all of the language processing is handled by plugins, even if they are built-in ones. They follow the same rules as externally written plugins. So, when you are typing and the UI displays syntax errors as you type, that is coming from the AST Plugin, which subscribes to the event that is sent when you type.

So a user plugin can be at least as powerful as the built-in plugins?

Exactly. In fact you can even replace the built-in plugins if you want to provide (say) an more sophisticated typecheck. That's all described in the guide.

The more you think about this, the more ideas you get!

I know! So I added a few of them to section 4, to try to open people's minds to the awesome possibilities.

So have many people written plugins?

There are three important ones: there is a UML translation plugin, which VDM++ can use to display UML class diagrams; there is a QuickCheck plugin that verifies proof obligations; and there is an Isabelle translation in the works, which will convert a VDM-SL specification to Isabelle in order to do proof work.

I was expecting more?

Well, it's early days. The plugin architecture is still evolving. But it's probably the most exciting area of VDMJ for me, currently.

Because there are so many possibilities?

Exactly. If we make it really easy for researchers to build and share plugins, who knows where it will take us!

Cool. Well, thanks for going through that. I agree, it sounds awesome.