quint: The core Quint tool

This directory contains the quint CLI providing powerful tools for working with the Quint specification language.

Prerequisites

• Node.js >= 18: Use your package manager or download nodejs.

• Java Development Kit >= 17, if you are going to use quint verify. We recommend version 17 of the Eclipse Temurin or Zulu builds of OpenJDK.

Installation

Install the latest published version from npm:

npm i @informalsystems/quint -g

How to run

Check the quint manual.

How to develop

Development environment

1. Make sure that you have installed npm. This is usually done with your OS-specific package manager.

2. Clone the repository and cd into the quint tool's subdirectory

   git clone [email protected]:informalsystems/quint.git
   cd quint/quint

3. Install dependencies:

   npm install

4. Compile quint:

   npm run compile

5. To run CLI, install the package locally:

   npm link

6. You can run CLI by typing:

   quint

Additionally, if you want to compile the vscode plugin:

1. Install yalc for local package management:

   npm install yalc -g

2. Publish the package locally with yalc:

   yalc publish

Code

Extend the code in src.

Unit tests

Write unit tests in test, add test data to testFixture. To run the tests and check code coverage, run the following commands:

1. Compile and test the parser:

   npm run compile && npm run test

2. Check code coverage with tests:

   npm run coverage

Updating the source map test fixtures

npm run update-fixtures

Integration tests

All development dependencies should be tracked in the package.json and package-lock.json. These will be installed when you run npm install on this project (unless you have explicitly told npm to use production settings).

To add a new dependency for integration tests or other development purposes run

npm install <dep> --save-dev

1. Update tests in cli-tests.md.

2. Run integration tests:

   npm run compile && npm link && npm run integration

Integration with Apalache

We maintain a set of integration tests against the latest release of Apalache. These tests are meant to catch any breaking changes requiring updates to Apalache's support for quint.

Generally, you should not have to run these tests locally, leaving the validation to our CI. But should you need to run these tests locally, you can do so with

npm run apalache-integration

It is required that you have a Java version meeting Apalache's minimum requirements.

Parser

We use the antlr4ts parser generator to compile the BNF like notation specified in ./src/generated/Quint.g4 into a typescript lexer and parser. To regenerate the parser and lexer, run

npm run antlr