Developer - overturetool/vdm-vscode GitHub Wiki

This page is used to write down things to remember when developing the code base for VDM VS Code. The idea is to make sure that the development style stays consistent with time as other collaborators are included in the development. This is not set in stone and you are more than welcome to suggest changes, the important part is that everyone is aware of the changes.

License

For the VDM VS Code project, we use the GNU General Public License v3.0. Thus, when creating a new file remember to include the SPDX License Identifier at the top of the file, like:

// SPDX-License-Identifier: GPL-3.0-or-later

Formatting

When developing on the extension please use the Prettier - Code formatted with the settings from .vscode/settings.json. This will ensure a consistent format across all the source files of the project.

Other handy extensions to use while developing for the extension are:

Repository Management

When developing the project please create a new branch from the development branch. When you are finished with the changes, create a pull request with a description of the changes. Furthermore, all commits should be bound to an issue, to keep track of the changes and the reason for them, this is done by adding the issue number to the commit message, e.g.:

git commit -m "#94 Changed client log to console output"

When creating an issue please use the labels, as this helps organize them.

The milestones are assigned according to the priority of an issue

  • Soon: Scheduled for the next release
  • Soonish: Scheduled for an upcoming release
  • Backlog: Not currently scheduled for any release

SLSP Development

The Specification Language Server Protocol (SLSP) protocol is meant to extend the Language Server Protocol (LSP), this means that we follow the same goal and format as they use. Therefore, protocol types and messages should be independent of the language, such that they can apply to multiple languages. Here is a link to the documentation from Microsoft on how to contribute to the LSP protocol, which we try to adhere to.

It takes careful consideration to not make the protocol VDM specific, but this is important as the SLSP protocol is meant as a step towards a unified protocol for all specification languages. More information on this can be found in our papers: Visual Studio Code VDM Support and The Specification Language Server Protocol: A Proposal for Standardised LSP Extensions.

When adding new client features that use the SLSP protocol, please follow the software design described in the design section.

Release Checklist

  1. Update VDMJ jars based on the master and highprecision branches. Write to Nick to make sure that everything has been merged.
  2. Check that the wiki is up-to-date (remember to update Usage GIFs and Settings)
  3. Bump version number in package.json
  4. Update CHANGELOG.md
    1. Add changes to the client from closed issues/developments
    2. Add changes from VDMJ (Ask Nick...)
  5. Close fixed issues
  6. Create a new .vsix file with the extension and delete the old one
    1. Run npm install -g vsce
    2. Run npm run enableWebpack
    3. Run vsce package
    4. Run npm run disableWebpack
  7. Merge all changes that should be included in the release to the main branch
  8. Create a release specific milestone and move the related issues
  9. Create a new release on Github
    1. Create a new tag with the format vX.Y.Z, e.g. v1.3.0
    2. Target: main
    3. Write a description that links to the milestone and shows the highlights of that release
    4. Attach the .vsix file containing the extension
  10. Upload the .vsix file to the VS Code marketplace

Feature Matrix

Feature Overture VDMJ/VDM VSCode
Syntax highlighting X X
Syntax check X X
Type check X X
Evaluation X X
Debugging X X
POG X X
Combinatorial Testing X X
Translate to LaTex X X
Translate to Word X
Extract VDM from Word X X
Code completion (x) (x)
Template expansion X X
Standard library import X X
Go-to definition (x) X
Coverage display X X
VDM to Java X (x)
VDM to XMI (UML) X
Dependency graph generation X X
VDM to Isabelle (x)
VDM Example Import X X
Real-time log viewer for VDM-RT X X
Launch in VDMTools X X
FMU wrapper X
VDM to C (x)
VDM to LLVM
VDM to Python