Skip to content

Latest commit

 

History

History
84 lines (66 loc) · 2.48 KB

README.md

File metadata and controls

84 lines (66 loc) · 2.48 KB
Raw

TLA+/PlusCal support for NeoVim

tla.nvim is a Lua plugin built to provide IDE-like experience while developing TLA+ and PlusCal specifications. Powered by official TLA tooling.

Features

  • TLA tools installation
  • PlusCal to TLA+ translation
  • TLC model-checking
  • TLC output parsing and displaying
  • state graph dump to dot-formatted file
  • code snippets
  • diagnostics via LSP mechanisms
  • worksheets and REPL
  • PDF generation

Prerequisites

  • Neovim >= v0.5.0. While tla.nvim will aim to always work with the latest stable version of Neovim, there is no guarantee of compatibility with older versions.
  • Java >= 8. If you have the JAVA_HOME environment variable, plugin will work from the start. Otherwise you should specify the location of Java installation.
  • plenary.nvim. Make sure to have this installed

Installation

Lazy

return {
  "susliko/tla.nvim",
  config = function ()
    require("tla") .setup()
  end
}

Packer

use({"susliko/tla.nvim", requires = { "nvim-lua/plenary.nvim" }})

-- init.lua
require("tla").setup()

Configuration

require("tla").setup()

is equivalent to:

require("tla").setup{
  -- Path to java binary directory. $JAVA_HOME by default
  java_executable = "path/to/java/bin",

  -- Options passed to the jvm when running tla2tools
  java_opts = { '-XX:+UseParallelGC' },

  -- Only needed if you don't wont automatic tla2tools installation
  tla2tools = "path/to/tla2tools.jar", 
}

Commands

Command Lua API Description
TlaInstall require"tla.install".install_tla2tools() Downloads latest tla2tools release. Rewrites existing
TlaTranslate require"tla".translate() Translates PlusCal code in the current buffer into TLA+ code
TlaCheck require"tla".check() Model-checks TLA+ code in the current buffer and displays results

Demo

TODO gifs

Integrations

Syntax Highlighting

tree-sitter usage for syntax highlighting is encouraged; a tree-sitter grammar exists for TLA+ and PlusCal.