Getting started

Installing Vehicle

To install the latest version of Vehicle, run the following command:

pip install vehicle-lang

To upgrade to a newer version of Vehicle, run the following command:

pip install vehicle-lang --upgrade

Building Vehicle

Getting the source

The main repository is vehicle-lang/vehicle. This contains the Vehicle compiler, the the standard library, the Python bindings, the Agda bindings, and a bunch of examples and tools.

The very first step to work on Vehicle is to clone the repository:

git clone https://github.com/vehicle-lang/vehicle.git
cd vehicle

Building the Vehicle compiler

Dependencies

Building the Vehicle compiler requires the Haskell compiler, called GHC, and the Haskell package manager, called Cabal. The Vehicle compiler can be built with:

at least the latest three major releases of GHC; and
the latest major release of Cabal.

We recommend that you install our preferred version of GHC

Installing GHC and Cabal

We recommend you install GHC and Cabal using GHCup.

Install GHCup following the instruction on the website: https://www.haskell.org/ghcup/

Instal GHC 9.4.8 and the latest version of Cabal.

Run the following commands:

ghcup upgrade
ghcup install ghc 9.4.8
ghcup set ghc 9.4.8
ghcup install cabal latest
ghcup set cabal latest

Check if your installation was successful.

Run the following command:

ghc --version

This should print:

The Glorious Glasgow Haskell Compilation System, version 9.4.8

Run the following command:

cabal --version

This should print:

cabal-install version 3.10.2.1
compiled using version 3.10.2.1 of the Cabal library

If you'd like to use a different version of GHC, you can find the list of versions that we test with in build-vehicle.yml. However, be aware that building the Python bindings requires our preferred version.

The preferred version of GHC

The preferred version of GHC is currently GHC 9.4.8, which is the version of GHC we recommend you use, and which is required to build the Python bindings.

Building

Ensure that you have the source code and that you have installed GHC and Cabal.

Update the list of Haskell packages.

Run the following command:
```
cabal update
```
Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Build the Vehicle compiler:
```
cabal build vehicle:exe:vehicle
```

Testing

Ensure that you can successfully build the Vehicle compiler.

The tests for the Vehicle compiler are in the tests subdirectory and use the Tasty testing framework as well as a custom driver for golden file tests—see Vehicle.Test.Golden.

There are three test suites for the Vehicle compiler:

The unit tests (unit-tests)
The golden tests (golden-tests)

The standard command to test the Vehicle compiler runs the unit and the compiler tests:

cabal test unit-tests golden-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1

This command is run on GitHub Actions whenever changes are pushed to Vehicle the default branch or an open pull request—see build-vehicle.yml.

This command builds the Vehicle compiler, if necessary, and runs the unit and compiler tests. The last lines of output should tell you about the tests, and should look like:

Running 1 test suites...
Test suite unit-tests: RUNNING...
Tests
  DeBruijnIndices
    substUnderLambdaClosed:       OK

  ...

All 18 tests passed (0.00s)
Test suite unit-tests: PASS

Running 1 test suites...
Test suite golden-tests: RUNNING...
Compiler
  compile
    simple-quantifierIn
      TypeCheck:                (0.04s)
      Agda:                     (0.04s)
      Marabou:                  (0.05s)

  ...

All 155 tests passed (12.33s)
Test suite golden-tests: PASS

The option --test-show-details=streaming asks the testing framework to print some live details about the tests it is running, and --test-option=--color=always asks it to use colour. If you omit these options, the output is much less verbose, and looks like:

Running 1 test suites...
Test suite unit-tests: RUNNING...
Test suite unit-tests: PASS
Running 1 test suites...
Test suite golden-tests: RUNNING...
Test suite golden-tests: PASS

The option --test-option=--num-threads=1 asks the testing framework to only run one test at a time. If you omit this option, you may get some failing tests due to #342.

Running specific tests

You can use the option --test-option="-p /X/" to only run tests with X in their name, e.g., if you only want to run the tests for the wind controller example, you can add --test-option="-p /windController/":

Running 1 test suites...
Test suite golden-tests: RUNNING...
Compiler
  compile
    windController
      TypeCheck: OK (0.05s)
      Marabou:   OK (0.06s)
      Agda:      OK (0.05s)

All 3 tests passed (0.15s)

Test suite golden-tests: PASS

If you want to further restrict those to only the test for the Agda backend, you can add --test-option="-p /windController.Agda/":

Running 1 test suites...
Test suite golden-tests: RUNNING...
Compiler
  compile
    windController
      Agda:      OK (0.06s)

All 1 tests passed (0.06s)

Test suite golden-tests: PASS

For more information, see the Tasty documentation on patterns.

The unit tests

The unit tests test properties of the internals of Vehicle, e.g., of the Vehicle library.

Run the following command:

cabal test unit-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1

You can use --test-option="--vehicle-logging X" to set the logging level, where X is one of NoDetail, MinDetail, MidDetail, or MaxDetail. The logging levels can be found by running vehicle --help.

These tests are specified in Haskell in tests/unit.

The golden tests

The golden tests test properties of the compiler as a whole, by running it with various input files and comparing the output to golden files, which have the .golden file extension.

Run the following command:

cabal test golden-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1

These tests are specified in test.json files in tests/golden, e.g., windController/test.json:

[
  {
    "name": "TypeCheck",
    "run": "vehicle check -s spec.vcl",
    "needs": ["spec.vcl"]
  },
  {
    "name": "Marabou",
    "run": "vehicle compile -s spec.vcl -t MarabouQueries -o Marabou.queries/ --network controller:controller.onnx",
    "needs": ["spec.vcl", "controller.onnx"],
    "produces": ["Marabou.queries/*.txt", "Marabou.queries/.vcl-cache-index"],
    "ignore": {
      "lines": ".*\"fileHash\".*"
    }
  },
  {
    "name": "Agda",
    "run": "vehicle compile -s spec.vcl -t Agda -o Agda.agda",
    "needs": ["spec.vcl"],
    "produces": ["Agda.agda"]
  },
  {
    "name": "DL2Loss",
    "run": "vehicle compile -s spec.vcl -t DL2Loss -o DL2Loss.vcl --network controller:controller.onnx",
    "needs": ["spec.vcl"],
    "produces": ["DL2Loss.json"]
  },
  {
    "name": "MarabouVerify",
    "run": "vehicle verify -q Marabou.queries -v Marabou",
    "needs": ["controller.onnx", "Marabou.queries"],
    "external": ["Marabou"]
  }
]

Each test.json file contains a list of test cases. Each test case must have the following fields:

name: The name of the test case.
run: The command to run.

Optionally, each test case can specify the following fields:

needs: A list of input files needed by the command.
produces: A list of output files produced by the command.
external: A list of external programs needed by the command.
enabled: Whether the test case is enabled.
ignore: An object containing settings for the diff algorithm.
- matches: A regular expression, which matches lines that should be ignored by the diff algorithm.
timeout: A timeout after which the test case is considered to have failed. The timeout should be a number suffixes with ms for miliseconds, s for seconds, m for minutes, or h for hours.

The logging level can be changed by changing the command in the test.json file. Changing the logging level changes the output of the command, which breaks the golden test.

Some golden tests require external tools, such as the MarabouVerify test above. To run these tests, add --test-option="--allowlist-externals=<external>" to the test command, where <external> is the name of the external dependency, such as Marabou.

Some golden tests diff extremely large files such as .vcl-plans, for which the diff isn't very meaningful. In order to only display the change in size for a given file type, add --test-option="--sizeOnly=<extension>" to the test command, where <extension> is the extension of the chosen file type.

Adding golden tests

To create a new golden test, you can use the new-golden-test command.

Compose the Vehicle command you'd like to test, e.g.,
```
vehicle compile -s spec.vcl -t MarabouQueries -o Marabou.queries -n controller:controller.onnx
```
Use cabal run vehicle -- rather than vehicle to ensure that you are building and running the current version, rather than an old installation.
Run the Vehicle command, and check that it succeeds.
Run the same Vehicle command, but prefixed with:
```
cabal run new-golden-test --
```
For instance:
```
cabal run new-golden-test -- vehicle compile -s spec.vcl -t MarabouQueries -o Marabou.queries -n controller:controller.onnx
```
This creates or updates the test.json file to add the test.

You can add --test-timeout before the Vehicle command to set a timeout for the test case.

You can add --test-path before the Vehicle command to add the test to a particular directory, which creates or updates the test.json file in that directory and copies any necessary files.

Updating the golden files

If the output of the Vehicle compiler changes, it is necessary to update the golden files for the compiler tests.

Warning: The following is a destructive action! Mistakes may result in faulty tests!

You can use the option --test-option="--accept" to accept the new output of the golden tests, and update the golden files.

The procedure for updating the golden files is:

Ensure that all changes are committed.

Run the following command:

cabal test golden-tests --test-option=--num-threads=1 --test-option="--accept"

Review the changes to the golden files, e.g., by inspecting the output of the following command:
```
git diff
```
The only changes to the golden files.

Debugging

Profiling

There are scripts for profiling the time and memory consumption of the Vehicle compiler:

./scripts/vehicle-profile-time
./scripts/vehicle-profile-heap

For more information, see the comments at the top of these files.

Loops

The compiler tests test the output of a successful run of the Vehicle compiler. If the Vehicle compiler loops, it does not terminate. Consequently, if you suspect there is an infinite loop, it is easier to run Vehicle directly with logging:

cabal run exe:vehicle -- --logging=MaxDetail ...

Extra logging

There is various useful debugging information that can be logged, but is not available even when the max logging level is set because its simply too verbose. This includes:

If you want to see normalisation behaviour, in Vehicle.Compile.Normalise.NBE, there are various disabled logging functions (e.g. showEntry) that can be enabled.
If you want to see the current contexts attached lambda Value constructors, in Vehicle.Compile.Descope.descopeNormExpr there is some disabled code that attaches that information to prettyVerbose.

Installing from source

Ensure that you have the source code and that you have installed GHC and Cabal.

Update the list of Haskell packages.

Run the following command:
```
cabal update
```
Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Install the Vehicle compiler:
```
cabal install vehicle:exe:vehicle --install-method=copy --overwrite-policy=always
```
The last few lines of output should tell you where Cabal installed the Vehicle compiler. By default, this is either ~/.local/bin or ~/.cabal/bin. You can tell Cabal where to install executables by passing --installdir.

Ensure that the directory where Vehicle is installed is on your system PATH.
Check if your installation was successful.

Run the following command:
```
vehicle --version
```
This should print 0.16.0.

Building the Vehicle Python bindings

Dependencies

Building the Vehicle Python bindings requires GHC and Cabal—specifically, our preferred version of GHC—and Python and pipx.

The Vehicle Python bindings can be built with all supported versions of CPython, the standard Python implementation, and the latest version of pipx. Support for feature and prerelease versions of Python is not guaranteed.

Installing Python and pipx

We recommend you install Python using pyenv.

Install pyenv following the instructions on the website: https://github.com/pyenv/pyenv#installation
Install the latest release of each supported Python version.

Run the following command:
```
pyenv install 3.9 3.10 3.11 3.12 3.13
```
Check if your installation was successful.

Run the following command:
```
pyenv versions
```
This should print something that looks like:
```
  system
  3.7.16
  3.8.16
  3.9.16
* 3.10.11 (set by PYENV_VERSION environment variable)
  3.11.3
```
There may be some differences in the exact versions and the default version (marked by the *), and there may or may not be a system version. However, there should be at least one version for each supported Python version, e.g., one version starting with 3.7, one starting with 3.8, etc.

Run the following commands:
```
pyenv shell 3.11
python --version
```
This should print something that looks like:
```
Python 3.11.3
```
There may be some differences in the exact version. However, the printed version should match the argument passed to pyenv shell, e.g., it should start with 3.11.
Install the latest release of pipx following the instructions on the website: https://pypa.github.io/pipx/#install-pipx

We recommend installing pipx globally, e.g., using your system package manager or the package manager for your system installation of Python, rather than using one of the Python versions managed by pyenv.
Check if your installation was successful.

Run the following command:
```
pipx --version
```
This should print something like:
```
1.2.0
```
The exact version may differ. However, the printed version should be greater than or equal to 1.2.0.

If you'd prefer not to use pyenv, you can install the latest release of each supported Python version using, e.g., your system package manager.

Troubleshooting

On Linux

If you get an error that looks like:

The virtual environment was not created successfully because ensurepip is not
available.  On Debian/Ubuntu systems, you need to install the python3-venv
package using the following command.

    apt install python3.10-venv

You may need to use sudo with that command.  After installing the python3-venv
package, recreate your virtual environment.

It means that Vehicle's testing framework is using the system installation of Python, but that the package for creating virtual environments is missing. The solution is to install it using your system package manager, as suggested by the text of the error message.

Building

Ensure that you have the source code and that you have installed both GHC and Cabal and Python and pipx.

Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Navigate to the vehicle-python subdirectory.
```
cd vehicle-python
```
Build the Vehicle Python bindings:
```
pipx run tox
```

This creates the directory dist which contains "wheels", which are the binary distribution format for Python packages. These wheels will have file names such as vehicle_lang-0.16.0-cp311-cp311-macosx_13_0_arm64:

#   Supported
#   Python   _____
#   versions      \
#                  vvvvvvvvvvv
vehicle_lang-0.16.0-cp311-cp311-macosx_13_0_arm64
#                              ^^^^^^^^^^^^^^^^^
#   Supported                /
#   Operating System  ______/
#   and Architecture

On Linux, the operating system will be a manylinux platform tag, such as manylinux2014 or manylinux_2_28. The manylinux_2_28 tag means that the wheel is compatible with any Linux distribution based on libc 2.28 or later. The manylinux2014 tag is an alias for manylinux_2_17.

If you'd prefer to only build wheels for one Python version, you can use one of the following options:

On macOS and Windows

You can use the standard Python build system, build.

Run the following command:
```
pipx run --spec=build pyproject-build --wheel
```
On Linux

You can use the build-wheel.sh script in vehicle-python/scripts. This script may ask you to install additional dependencies via pip. Unfortunately, the Linux wheels cannot be built using just Python's standard build system, as they require delocating, which is the process of finding non-standard shared libraries and bundling them with the wheel.

Warning: The binary distributions built following these instructions are less portable than those that are built by the CI:

The macOS wheels built following these instructions will require at least your version of macOS, whereas the wheels built on CI are backwards compatible to macOS 10.10 (Yosemite).
The Linux wheels built following these instructions will require at least your system version of libc, whereas the wheels built on CI are backwards compatible to libc 2.17 (Ubuntu 18.04).

You can determine your system's libc version via Python by running:
```
python -c 'import platform; print(platform.libc_ver())'
```

Testing

Ensure that you can successfully build the Vehicle Python bindings. The tests for the Vehicle Python bindings are in the tests subdirectory and use tox for Python version and virtual environment management and pytest for test discovery and execution. The configuration for tox and pytest is in pyproject.toml under [tool.tox] and [tool.pytest], respectively.

There are two test suites for the Vehicle Python bindings:

The executable tests
The loss function tests
The pygments tests

The standard command to test the Vehicle compiler runs both:

pipx run tox

This command build the Python bindings and runs all test suites with each supported version of Python.

Running tests for specific versions of Python

You can use the tox option -e to run a specific environment, e.g., to only run tests for Python 3.11 on macOS, run the following command:

pipx run tox run -e py311-mac

The environments are defined in pyproject.toml under [tool.tox], and are combinations of the Python version and the platform (lin, mac, or win).

Running specific tests

The arguments after -- are passed to pytest.

You can pass the path to a test file, which only runs the tests in that file:

pipx run tox -- tests/test_main.py

You can pass -k 'X' to only run tests with X in their name, e.g., if you only want to run the test_main function from tests/test_main.py, you can run:

pipx run tox -- -k 'test_main'

For more information, see the pytest documentation.

The executable tests

The executable tests test whether the Vehicle compiler is installed as part of the Python package.

Run the following command:

pipx run tox -- tests/test_main.py

The loss function tests

The loss function tests test the translation and use of properties from Vehicle specification files as loss functions.

Run the following command:

pipx run tox -- tests/test_loss*.py

The pygments tests

The pygments tests test the integration with the Pygments syntax highlighter.

Run the following command:

pipx run tox -- tests/test_pygments.py

Installing from source

Ensure that you have the source code and that you have installed both GHC and Cabal and Python and pipx.

Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Navigate to the vehicle-python subdirectory.
```
cd vehicle-python
```
Install the Vehicle Python bindings:
```
python -m pip install .
```
This installs the Vehicle compiler and the vehicle_lang Python package.
Check if your installation of the Vehicle compiler was successful.

Run the following command:
```
vehicle --version
```
This should print 0.16.0.
Check if your installation of the vehicle_lang package was successful.

Run the following command:
```
python -c 'import vehicle_lang; print(vehicle_lang.VERSION)'
```
This should print the same version as above.

Installing in editable mode

If you are developing the Python bindings it can be cumbersome to rebuild the Vehicle compiler from source on every test run. To avoid this, you can install the Python bindings in editable mode.

Run the following command from the vehicle-python subdirectory:

python -m pip install -e .[test]

This installs the Python bindings in editable mode, which directly adds the files in the development directory are added to Python's import path. Note that you must have the preferred version of GHC (see above) active in order to run this command otherwise you'll get a Error: cabal: Could not resolve dependencies error message.

When the Python bindings are installed in editable mode, you can run pytest directly:

python -m pytest

You'll have to reinstall the Python bindings when the metadata in pyproject.toml or the Haskell source changes.

Pre-commit hooks

The Vehicle repository has a variety of pre-commit hooks that check and ensure code quality, managed by pre-commit. The pre-commit hooks require pre-commit, cabal-fmt and ormolu.

We recommend that you install these hooks.

Ensure that you have installed GHC and Cabal.
Install pre-commit following the instruction on the website: https://pre-commit.com/#install

Install cabal-fmt.

Run the following command:

cabal install cabal-fmt --ignore-project --overwrite-policy=always

Install ormolu.

Run the following command:

cabal install ormolu --ignore-project --overwrite-policy=always

Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Install the pre-commit hooks.

Run the following command:
```
pre-commit install
```
This should print:
```
pre-commit installed at .git/hooks/pre-commit
```
If you ever clone a fresh copy of the Vehicle repository, you'll have to rerun this command.
Test the pre-commit hooks.

Run the following command:
```
pre-commit run --all-files
```

The hooks run every time you run git commit. You can skip the hooks by adding the --no-verify flag to your Git command.

Editor support

You can use whatever development environment you prefer.

We recommend using VSCode with the following extensions, based on what parts of Vehicle intend to work on:

Project	Language	Extension
any	Vehicle	Vehicle Syntax Highlighting
any	Haskell	Haskell, Haskell Syntax Highlighting
any	Cabal	cabal-fmt
any	Markdown	MyST-Markdown
vehicle-agda	Agda	agda-mode
vehicle-python	Python	Python, Pylance, Black Formatter, isort
vehicle-python	TOML	Even Better TOML

Publishing a release

Vehicle is released via PyPI, the Python Package Index.

Ensure that you have the source code and that you have installed both GHC and Cabal and Python and pipx.

To publish new releases to PyPI, you need a PyPI account that is authorised as a collaborator on the vehicle_lang project, and you need to create a PyPI API token for that account and add it to your .pypirc file.

Finally, you need access to a machine running macOS with an M1/M2 chipset.

The procedure to create a new release is:

Navigate to your local copy of the Vehicle repository.
Ensure that you are on the default branch dev.
Ensure that all changes are committed and pushed.
Ensure that the tests are passing on CI: https://github.com/vehicle-lang/vehicle/actions/workflows/ci.yml?query=branch%3Adev
Run all tests and fix any errors.

Vehicle compiler tests

Run the following command from the root of the repository:
```
cabal test all --test-option=--num-threads=1
```
Vehicle Python bindings tests

Run the following command from vehicle-python:
```
pipx run tox
```
Vehicle documentation tests

Run the following command from docs:
```
pipx run tox
```
If any errors occur, fix them, and restart from step 1.
Choose the appropriate version number to increase.
- If you're increasing the major version, run this command:
```
pipx run bumpver update --major --dry
```
- If you're increasing the minor version, run this command:
```
pipx run bumpver update --minor --dry
```
- If you're increasing the patch version, run this command:
```
pipx run bumpver update --patch --dry
```
The output will contain a diff of the changes to be made.

If the diff looks reasonable, rerun the command without the --dry flag.

This will update the version, create a Git tag, and push it to GitHub.
Ensure that the CI successfully builds and publishes Vehicle to PyPI: https://github.com/vehicle-lang/vehicle/actions/workflows/ci.yml?query=branch%3Adev

Add identifiers for the new version to CITATION.cff at the top of the list under the identifiers key.

You can use the following as a template:

- type: url
 value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.13.0"
 description: "The GitHub release URL of tag v0.13.0."
- type: url
   value: "https://gpypi.org/project/vehicle-lang/0.13.0/"
   description: "The PyPI release URL of version 0.13.0."

On a macOS machine with an M1/M2 chipset

There are no GitHub Actions runners with an M1/M2 chipset, so the binary distributions for this platform must be built and published manually from an appropriate machine.

Run the following command from vehicle-python:
```
pipx run tox
```
This creates the directory dist which contains "wheels", which are the binary distribution format for Python packages. If you're on macOS with an M1/M2 chipset, these look like:
```
vehicle_lang-0.16.0-cp310-cp310-macosx_13_0_arm64.whl
vehicle_lang-0.16.0-cp37-cp37m-macosx_13_0_arm64.whl
vehicle_lang-0.16.0-cp39-cp39-macosx_13_0_arm64.whl
vehicle_lang-0.16.0-cp311-cp311-macosx_13_0_arm64.whl
vehicle_lang-0.16.0-cp38-cp38-macosx_13_0_arm64.whl
```
Run the following command to check each wheel's metadata:
```
pipx run twine check --strict dist/*.whl
```
Warning: The following is a destructive action! Published versions cannot be changed!

Run the following command to upload each wheel to PyPI:
```
pipx run twine upload dist/*.whl
```
Edit the release on GitHub and add the wheel files in dist/.

The release will be at a URL like:

https://github.com/vehicle-lang/vehicle/releases/tag/v0.16.0

Files

CONTRIBUTING.md

Latest commit

History

CONTRIBUTING.md

File metadata and controls

Table of contents

Getting started

Installing Vehicle

Building Vehicle

Getting the source

Building the Vehicle compiler

Dependencies

Installing GHC and Cabal

The preferred version of GHC

Building

Testing

Running specific tests

The unit tests

The golden tests

Adding golden tests

Updating the golden files

Debugging

Profiling

Loops

Extra logging

Installing from source

Building the Vehicle Python bindings

Dependencies

Installing Python and pipx

Troubleshooting

On Linux

Building

Testing

Running tests for specific versions of Python

Running specific tests

The executable tests

The loss function tests

The pygments tests

Installing from source

Installing in editable mode

Pre-commit hooks

Editor support

Publishing a release