24 releases (12 stable)

new 1.2.4 Apr 4, 2024
1.2.1 Mar 26, 2024
1.0.8 Dec 21, 2023
1.0.7 Nov 19, 2023
0.3.0 Oct 6, 2021

#43 in Text editors

Download history 1/week @ 2023-12-18 5/week @ 2024-02-19 29/week @ 2024-02-26 140/week @ 2024-03-11 9/week @ 2024-03-18 213/week @ 2024-03-25 750/week @ 2024-04-01

1,112 downloads per month
Used in tlauc

MIT license

37MB
1M SLoC

C 1M SLoC // 0.0% comments JavaScript 1K SLoC // 0.2% comments Scheme 271 SLoC // 0.1% comments Rust 32 SLoC // 0.1% comments

tree-sitter-tlaplus

Build & Test npm crates.io

Overview

This is a tree-sitter grammar for the formal specification language TLA⁺ and its embedded variant PlusCal. Tree-sitter is an incremental error-tolerant parser generator primarily aimed at language tooling such as highlighting, code folding, symbol finding, and other tasks making use of its fully-featured syntax tree query API. This grammar is intended to function gracefully while parsing a source file mid-edit, when the syntax isn't fully correct. It is also fast enough to re-parse the file on every keystroke. You can take the parser for a spin at https://tlaplus-community.github.io/tree-sitter-tlaplus/

The most important files in this repo are grammar.js and src/scanner.cc. The former is the source of truth for parser code generation and the latter contains logic for parsing the context-sensitive parts of TLA⁺ like nested proofs and conjunction/disjunction lists. This grammar is published as both a Rust crate and Node.js package, although most tree-sitter grammar consumers download this repo directly. A WASM build is included in the Node.js package.

A blog post detailing the development process of this parser can be found here. This repo is mirrored on sourcehut.

Aims & Capabilities

The aim of this project is to facilitate creation of modern user-assistive language tooling for TLA⁺. To that end, the project provides two main capabilities:

  1. Provide an approximately-correct parse tree for TLA⁺ specifications in standardized form, for easy integration with general projects designed to consume the tree-sitter grammars of many languages.
  2. Provide a tree query API for efficiently querying the TLA⁺ parse tree, in addition to an API for arbitrary programmatic exploration of same, with bindings in multiple languages for easy integration with projects specifically targeting TLA⁺.

The correctness criterion of this parser is as follows: if the TLA⁺ specification being parsed constitutes valid TLA⁺ (both syntactically and semantically), the parse tree will be correct. If the spec is not valid TLA⁺, the parse tree will be approximately correct - perhaps permissively allowing illegal syntax, or interpreting erroneous syntax in strange ways. This permissive behavior makes it excellent for user-assistive language tooling, but probably a poor choice as the backbone for an interpreter or model-checker. Application possibilities include:

If you really want to use this project to write an interpreter, nobody's stopping you from trying. You could first use SANY to check spec validity, then use this parser to extract & interact with the actual parse tree. For a REPL, you might want to wait until the multiple entry points feature is added to tree-sitter so you can parse standalone TLA⁺ expressions without an encapsulating module.

Use & Notable Integrations

There are a number of avenues available for consuming & using the parser in a project of your own; see the tlaplus-tool-dev-examples repo.

Notable projects currently using or integrating this grammar include:

  • nvim-treesitter for TLA⁺ syntax highlighting & code folding in Neovim
  • tla-web for a web-based TLA⁺ interpreter and trace explorer
  • GitHub for syntax highlighting of TLA⁺ files and snippets
  • tlauc for translating between ASCII and Unicode TLA⁺ symbols
  • tla-mode for TLA⁺ syntax highlighting in Emacs

As applicable, query files for integrations live in the integrations directory.

Build & Test

  1. Install Node.js and npm
  2. Install a C compiler
  3. Clone the repo with the --recurse-submodules parameter, or run git submodule update --init --recursive if you already cloned it without that parameter
  4. Open a terminal in the repo root and run npm install to download packages & build the project
  5. Run npm test to run Tree-sitter unit tests

Corpus Tests

This test ensures the grammar can parse all modules in the tlaplus/examples repo, which is included as a git submodule. To run:

  1. If this is the first time running tree-sitter on your machine, run npx tree-sitter init-config
  2. For Unix-type OSs, run ./test/run-corpus.sh; for Windows, run .\test\run-corpus.ps1
  3. The scripts exit with error code 0 if successful

WASM Build

  1. Install Emscripten 2.0.17 or earlier (why?)
  2. Run npx tree-sitter build-wasm

The Playground

The playground enables you to easily try out the parser in your browser. You can use the playground online (serving the latest release) or run it locally by building the WASM (see instructions above) then running npx tree-sitter playground.

The playground consists of a pane containing an editable TLA⁺ spec, and another pane containing the parse tree for that spec. The parse tree is updated in real time as you edit the TLA⁺ spec. You can click parse tree nodes to highlight the corresponding snippet of TLA⁺, and move the cursor around the spec to show the corresponding parse tree node. You can click the "log" checkbox and open your browser's development console to see the parser's debug output as it attempts to parse the TLA⁺ spec. You can also click the "query" checkbox to open a third pane for testing tree queries; for example, enter the following to match all operator names in a capture named @operator (indicated by the names becoming highlighted):

(operator_definition name: (identifier) @operator)

Fuzzing

You can fuzz the grammar if you're running Linux with a recent version of Clang installed. Do so as follows:

  1. Clone the repo with the --recurse-submodules parameter
  2. From repo root, run the bash script test/fuzzing/build-for-fuzzing.sh
  3. From repo root, run test/fuzzing/out/tree_sitter_tlaplus_fuzzer

Contributions

One easy way to contribute is to add your TLA⁺ specifications to the tlaplus/examples repo, which this grammar uses as a valuable test corpus!

Pull requests are welcome. If you modify grammar.js, make sure you run npx tree-sitter generate before committing & pushing. Generated files are (unfortunately) currently present in the repo but will hopefully be removed in the future. Their correspondence is enforced during CI.

You can also contribute by running the fuzzer and reporting bugs it finds, as described above.

Dependencies

~2.7–4MB
~71K SLoC