History

README.md

This directory contains thequint CLI providing powerful tools for workingwiththe Quint specification language.

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

• Java Development Kit >= 17, if you are going to usequint verify. Werecommend version 17 of theEclipse Temurin orZulubuilds of OpenJDK.

Install thelatest published version from npm:

npm i @informalsystems/quint -g

Check thequint manual.

1. Make sure that you have installednpm. This is usually done with yourOS-specific package manager.

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

   git clone git@github.com:informalsystems/quint.gitcd quint/quint

3. Install dependencies:

   npm install

4. Compilequint:

   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. Installyalc for local package management:

   npm install yalc -g

2. Publish the package locally with yalc:

   yalc publish

Extend the code insrc.

Write unit tests intest, add test data totestFixture. To run the tests and check code coverage, run thefollowing commands:

1. Compile and test the parser:

   npm run compile&& npm runtest

2. Check code coverage with tests:

   npm run coverage

npm run update-fixtures

All development dependencies should be tracked in thepackage.json andpackage-lock.json. These will be installed when you runnpm install onthis project (unless you haveexplicitly toldnpm to useproduction settings).

Toadd a new dependency for integration tests or other developmentpurposesrun

npm install<dep> --save-dev

1. Update tests incli-tests.md.

2. Run integration tests:

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

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

Generally, you should not have to run these tests locally, leaving thevalidation to our CI. But should you need to run these tests locally, you can doso with

npm run apalache-integration

It is required that you have a Java version meetingApalache's minimumrequirements.

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

npm run antlr