I’ve recently been Last year, I was working on adding some new features to a Visual Studio Code Extension. I had previously done work to add similar functionality to a Visual Studio Extension. In the time since then, the project hasn’t really moved forwards, and I’ve decided to try and organise my thoughts on the matter.
What extensions?
The extensions I’ve worked with are designed to enable support for the Dafny language. Specifically, I am enabling support for Tactics (developed by a team from my university) and also Shorty (developed by one of the other students on the CS course I took).
Dafny is a verification-aware programming language, one where you can embed a mathematical proof of the program in the source code via annotations like ensures x > 0. Tactics allow you to more easily write the proof, by embedding commonly re-used, well… “tactics”. Shorty is a separate tool that analyses the source code of programs to check if the proof annotations are actually needed. The Dafny proof checker is good enough to handle certain logical leaps, so there’s no sense in littering the source code with unneeded annotations.
Visual Studio vs Code
One of the major problems I have with Visual Studio and Visual Studio Code is the branding. I get that Microsoft have this “brand” of Visual Studio as a development environment, but Code is so very different to Studio.
Microsoft seem to do this consistently: They have the opportunity to make a new brand, but refuse to. Remember Microsoft Edge being originally codenamed “spartan” – something bare, fast and to the point, which they then messed up by giving it the same branding as Internet Explorer. Eugh. To make it clearer, for the duration of this post, I’ll refer to Visual Studio as VS, and Visual Studio Code as Code.
What am I adding
There are two main features that need to be implemented, one for each of these two components:
- The ability to view tactics as they are expanded inside methods
- The ability to quickly check for unneeded annotations
Both of these, within the IDE, without firing up an external tool.
Extending VS Code
Prior to going into this I had no idea how to write with TypeScript, or really any understanding of what TS was. I also had no clue, beyond knowing it used the Electron framework, how the insides of Code worked.
The Structure
There already exists an extension that supports the Dafny language, sans my additions, so I took that as my starting point. The structure of how this all fits together is quite interesting:
- The Code extension component is largely event-driven
- Code also has a client-server interaction between the extension itself, and a backend for managing the language.
- This Language Server also has a client-server interaction between Code and the .NET process that runs the Dafny Server
- The Dafny Server responds to verbs like “Verify”
Getting Started
My methodology for getting to grips with something I’m not terribly sure about is a mix of reading the documentation and just jumping right into it. Having done this, I ended up with a strategy of trying to bootstrap the new functionality.
That is to say, hijack the original communication channels so they do something else (like transmit information about tactics), and once I get that going, slowly refactor these communications out into their own specialised components.
I find this gives me a better understanding of the architecture in use, as in a way it mixes the learning, prototyping and the development all in one.
Typescript
I really like typescript. It’s the nice syntax of javascript, but with far more structure and sense to it, like typing, classes and more. Thanks to the structure, I can use auto-completion in Code while typing. I find that this kind of auto-completion isn’t terribly useful for speeding up typing, but it is great at showing off the API structure in one go without having to trawl through documentation.
Development in Code
Code is nice. It has a sense of familiarity from VS, but without the need to set up annoying “solutions”, instead focusing on folders. It even has features which are paywalled in VS, like “peeking” at code references.
It does have some issues in its design though, like how I can’t get both a PowerShell and WSL prompt at one time, which is a great pity.
It is however, faster than VS and just easier to use, while at the same time not compromising on how much you can customise the way it works.
Code’s Extension API
This API is quite nicely prepared. The event driven nature makes it easy to start adding things in. Compared to the extension I developed in VS, I think I much prefer doing it the Code way.
The structure of the project in the VS extension seemed quite convoluted, and makes more sense with Code’s Language Server separation. The additional separation, by language, of the Dafny Server also has a great advantage in making me think about the “correct” way of doing things, with a much clearer separation of concern.
Debugging
I think the one flaw in Code it the somewhat poor debugging tools when in comparison with VS. The basics are there (breakpoints, stack, variable inspection), but the interface sucks as it’s all stuck inside a sidebar.
That being said, at least Code is faster. I find that VS can get very sluggish when it needs to debug something with lots of moving parts. That’s the payoff of debugging, though.
Of course, all of the debugging isn’t helped by the fact that Code is aimed at debugging Java- and Type-Script languages whereas VS is better suited to debugging .NET processes. Despite trying to do it all in one, I found it easier to just debug each part separately and put up with the finnicky bits, and so ended up with Code and VS both running at once.
The Original Extension
The extension which I’m adding functionality to is pretty nicely built internally, though it seems to somewhat suffer from maintenance, with a few things that didn’t entirely seem to work.
This blog article up until this point was in a draft state since last year. Here’s what I think now.
What next?
With the project at somewhat of a standstill, I’ve left the code available on GitHub if anyone wants to pick up where I left off. Dafny, and Tactics more so, is a pretty niche language so I don’t imagine many people will have a use for it.
VS Code is a constantly evolving codebase. I’m quite glad of that, as its a shift from the Microsoft of the past who typically wouldn’t update their products all that often. However, a consequence of this is that I imagine the extension will fall into disrepair (if it isn’t already, I havent even checked).
Still, for anyone interested: https://github.com/LonMcGregor/VS-Code-Language-Server-for-Dafny
