Skip to content

Latest commit

 

History

History
216 lines (144 loc) · 9.13 KB

CONTRIBUTING.md

File metadata and controls

216 lines (144 loc) · 9.13 KB
Raw

All forms of contribution are highly welcome! Feel free to file bugs, propose improvements, ask questions, send other feedback.

For those, who want to write some code, here's a short guide.

Getting started

Prerequisites

  1. Since this is a VS Code extension, you'll need VS Code to check your fixes and improvements.
  2. The extension requires NodeJS runtime (12.12 at the moment).
  3. It's written mostly in TypeScript, so you'll need to install it too.

Clone, Build, Test, Package

Clone the repository:

git clone https://github.com/tlaplus/vscode-tlaplus.git
cd vscode-tlaplus

Download dependencies:

npm install

Build, check and test:

Warning! VS Code must not be open when you run tests from command line.

npm run vscode:prepublish
npm run lint
npm test
npm run test:tlaplus-grammar

Run and Debug

To run the extension in debug mode:

  1. Open the project directory in VS Code.
  2. Switch to the Debug and Run panel.
  3. Select the "Extension" config.
  4. Press "Start Debugging".

Or just use a hotkey for the Start Debugging command if the "Extension" configuration is already selected.

Using Dev Container

This project has a devcontainer (https://code.visualstudio.com/docs/devcontainers/containers) configuration with all the setup required to develop and test the extension.

When running the extension in debug mode you only have access to the project folder. If you wish to mount more folders you can add them in the mounts section of the devcontainer.json file.

Test from VS Code

To run unit tests from VS Code:

  1. Open the project directory in VS Code.
  2. Switch to the Debug and Run panel.
  3. Select the "Run Extension Tests" config.
  4. Press "Start Debugging".

Or just use a hotkey for the Start Debugging command if the "Run Extension Tests" configuration is already selected.

TLA+ Grammar Tests

To run the TLA+ grammar tests from VS Code:

  1. Open the project directory in VS Code.
  2. Switch to the Debug and Run panel.
  3. Select the "Run TLA+ Grammar Tests" config.

The output of the tests will be who under the DEBUG CONSOLE in VS Code.

Test from Github Codespaces / Dev Container

To run unit tests from within a Codespace:

  1. Switch to the Debug and Run panel.
  2. Select the "Run Extension Tests" config.
  3. The output of the tests will be who under the DEBUG CONSOLE in VS Code.

You can also run them directly from the terminal using a virtual display:

xvfb-run --auto-servernum npm test --silent

Package

To package the extension and create the .vsix file:

npm install -g @vscode/vsce
vsce package

# View files packaged in the vsix
unzip -l *.vsix

Test extension in a web environment

The extension has support for web environments such as vscode.dev but with only a limited set of features is enabled (different entrypoint from the main extension).

Further read: https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension

Using @vscode/test-web

This is the simplest method, however, at time of writing, it does not work in a Codespaces environment.

To test the extension using @vscode/test-web run:

# Optional: get some example files
git clone https://github.com/tlaplus/Examples.git ~/Examples

# Compile extension
npm install
npm run compile

# Start a local vscode.dev with the tla+ extension
npm install -g @vscode/test-web
vscode-test-web  --extensionDevelopmentPath=. --headless=true ~/Examples
# Open http://localhost:3000/ in a browser

Using vscode.dev

For updated instructions see: https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension-in-on-vscode.dev

To run the extension in the actual vscode.dev environment run:

# From the extension root path, start a http server
npx serve --cors -l 5000

# In another terminal start a localtunnel to the previous http server
npx localtunnel -p 5000

# Open the generated url and click the "Click to Continue" button
# Copy the generated url

# Go to vscode.dev (suggestion to open in tlaplus examples folder: https://vscode.dev/github/tlaplus/Examples)
# Ctrl+Shift+P > Developer: Install Extension from Location.. > Paste the generated url

# Open devtools (F12) to check for errors
# Ctrl+Shift+P > Developer: Show Running Extensions

Overview

The extension consists of the following components:

  1. Language definitions for:
    • TLA+ specifications (the tlaplus language),
    • PlusCal code (the pluscal language),
    • TLA+ model definitions (the tlaplus_cfg language),
    • TLC output files (the tlaplus_out language), which is used for simple highlighting.
  2. The main extension code that runs under the hood, handles user commands and reacts to various events.
  3. The implementation of the Check Result View panel that visualizes TLC output and allows to analyze it easily.
  4. The tla2tools.jar file from the official TLA+ project. All the specification syntax verifications, PlusCal translations and TLC checks are actually performed by this Java library.

The extension also requires a Java Virtual Machine (JVM) to be installed. More information.

Project Layout

Manifest

The package.json file is both the npm-package definition and the extension manifest. It defines the extension metadata, its dependencies, contributions to VS Code, build commands etc.

Main Source Code

Most of the extension main code is located in the src directory. The only exception is the file resources/check-result-view.js which contains JavaScript code that empowers the Check Result View panel (more details below).

Names of files and subdirectories are usually self-descriptive. Here're the most interesting ones:

  • src/main.ts — This is the starting point of the extension. It sets things up when the extension is loaded.
  • src/main.browser.ts — Starting point for the extension in a browser environment.
  • src/tla2tools.ts — All calls to tla2tools.jar go through methods from this file.
  • src/panels/checkResultView.ts — The main functions that are responsible for interaction between the main extension code and the Check Result View panel.
  • src/commands/ — This directory contains implementation of all the VS Code commands that the extension provides.
  • src/completions/ — The code completion providers.
  • src/formatters/ — Classes that provide auto-formatting functionality.
  • src/model/ — The classes that describe model check results. Objects of these classes are used by the Check Result View panel.
  • src/parsers/ — Set of classes that parse output of the various TLA+ tools.
  • src/symbols/ — The classes that extract symbol information from files (constants, variables, operators etc.)
  • src/webview/check-result-view.tsx implement the Check Result View panel using Webview API.

Tests

Tests are good!

They are placed in the tests directory. Files runTest.ts and suite/index.ts are used to setup the Mocha testing framework. Other files and subdirectories use the same layout as the main source code.

Other

There're some other useful stuff in the project:

  • .vscode/ — VS Code configuration files that make working with the project easier.
  • languages/ — Languages definition files.
  • tools/ — Additional artifacts that are used by the extension.

Source Code Style

Yeah, there are some rules about how the code should look, but they are not hard to follow.

ESLint is responsible for checking it as a part of building process. It uses the .eslintrc.json file as its config.

With the ESLint extension installed, VS Code will check your code automaticaly.

Useful Resources