Contributing to Vehicle

Building Vehicle

Getting the source

The main repository is [vehicle-lang/vehicle]. This contains the Vehicle compiler, the the standard library, bindings for Python, Agda and Rocq, 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 vehicle/tests/ subdirectory and use [the Tasty testing framework] as well as a custom driver for golden file tests—see vehicle/tests/golden/Vehicle/Test/Golden.hs.

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 .github/workflows/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 (examples/windController/), 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 vehicle/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 vehicle/tests/golden/, e.g., vehicle/tests/golden/compile/windController/test.json:

[
  {
    "name": "TypeCheck",
    "run": "vehicle typecheck -s spec.vcl",
    "needs": ["spec.vcl"]
  },
  {
    "name": "Marabou",
    "run": "vehicle compile queries -s spec.vcl -f 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 itp -s spec.vcl -t Agda -o Agda.agda",
    "needs": ["spec.vcl"],
    "produces": ["Agda.agda"]
  },
  {
    "name": "Rocq",
    "run": "vehicle compile itp -s spec.vcl -t Rocq -o Rocq.v",
    "needs": ["spec.vcl"],
    "produces": ["Rocq.v"]
  },
  {
    "name": "RocqVerify",
    "run": "vehicle compile itp -s spec.vcl -t Rocq -o Rocq.v && coqc -vok Rocq.v -w none",
    "needs": ["spec.vcl"],
    "produces": ["Rocq.v"],
    "external": ["coqc"],
    "ignore": {"files": [".Rocq.aux", "Rocq.glob", "Rocq.vok"]}
  },
  {
    "name": "DL2Loss",
    "run": "vehicle compile loss -s spec.vcl -l 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 queries -s spec.vcl -f 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 queries -s spec.vcl -f 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 vehicle/tests/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.24.0.

Building the Vehicle Python bindings

Installing from PyPI

If you only need the published Python package (for example to compile queries for verifiers), install it directly from PyPI:

pip install vehicle_lang

Loss backends are optional extras so that you only install the deep-learning frameworks you actually need. Add the extras when syncing an environment or installing on CI:

pip install "vehicle_lang[pytorch]"
pip install "vehicle_lang[tensorflow]"

It is safe to mix extras—pip install "vehicle_lang[test,pytorch]" installs the pytest stack plus the PyTorch backend in one go.

Dependencies

Building the Vehicle Python bindings requires

GHC and Cabal—specifically our preferred version of GHC
uv for Python environment management, locking, and builds (see the official Projects guide)
A supported CPython (3.10–3.13). Feature or pre-release interpreters are not guaranteed to work. We recommend pinning the interpreter with uv python pin so every sync uses the same version (see Installing Python).

Installing uv and bindings

Follow the official uv installation guide or run one of the quick installers:

macOS / Linux: curl -LsSf https://astral.sh/uv/install.sh | sh
Windows (PowerShell): powershell -ExecutionPolicy ByPass -c "irm https://astral.sh/uv/install.ps1 | iex"

Verify your installation with uv --version.

uv sync reads vehicle-python/pyproject.toml, resolves dependencies into uv.lock, and materialises the environment in .venv. The base dependency set is intentionally small; install whichever extras you need with the --extra flag (see Managing dependencies). PyTorch is the recommended backend, so most workflows begin with:

uv sync --extra pytorch

Add TensorFlow only when targeting platforms that ship TensorFlow wheels:

uv sync --extra tensorflow
uv sync --extra pytorch --extra tensorflow
uv sync --all-extras

The deep-learning backends remain optional—install only what you require to keep your local environment minimal.

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 GHC/Cabal plus uv.

Navigate to your local copy of the Vehicle repository.
```
cd path/to/vehicle
```
Navigate to the vehicle-python subdirectory.
```
cd vehicle-python
```
Create (or refresh) the project environment. For example, to install the testing stack plus both deep-learning backends:

uv sync --extra test --extra pytorch --extra tensorflow

Build the Vehicle Python bindings:

uv build

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.24.0-cp311-cp311-macosx_13_0_arm64:

#   Supported
#   Python   _____
#   versions      \
#                  vvvvvvvvvvv
vehicle_lang-0.24.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.

uv build uses the interpreter that was pinned for the project (or the system default if none has been pinned). If you’d prefer to build with a different Python version, run uv python install <version> followed by uv python pin <version> and rebuild. For Linux builds that need delocation, use the helper script:

uv run --extra wheel scripts/build-wheel.sh

scripts/build-wheel.sh mirrors the CI behaviour and may prompt you to install a few additional build-time utilities.

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 live in the vehicle-python/tests/ subdirectory and use [pytest] for discovery and execution; uv provides interpreter and dependency management. The pytest configuration remains in vehicle-python/pyproject.toml under [tool.pytest].

There are three test suites for the Vehicle Python bindings:

The executable tests
The loss function tests
The pygments tests

Running the full suite for one interpreter

After syncing the project (for example via uv sync --extra test --extra pygments --extra pytorch), run every suite for the currently pinned interpreter with:

uv run --extra test --extra pygments python -m pytest

Add --extra tensorflow when running on a platform where TensorFlow wheels are available (Linux x86_64/aarch64, macOS x86_64, or Windows AMD64 with Python < 3.13).

Matrix testing across Python versions

Install the supported interpreters (one-time):

uv python install 3.10 3.11 3.12 3.13

Then iterate across them, letting uv handle the right interpreter each time:

for version in 3.10 3.11 3.12 3.13; do
  echo "==> pytest under Python ${version}"
  UV_PYTHON_PREFERENCE=managed \
    uv run --python "${version}" --extra test --extra pygments python -m pytest "$@"
done

On PowerShell, the equivalent loop is:

$versions = @(3.10, 3.11, 3.12, 3.13)
foreach ($version in $versions) {
  Write-Host "==> pytest under Python $version"
  $env:UV_PYTHON_PREFERENCE = "managed"
  uv run --python $version --extra test --extra pygments python -m pytest $args
}

The loops forward any additional pytest arguments. Add --extra tensorflow when running on a platform where the TensorFlow extra is supported. This replaces the old tox matrix, so CI and local workflows retain multi-version coverage.

Running specific tests

Tests are invoked directly through pytest. Pass a file to focus on just that file:

uv run --extra test --extra pygments python -m pytest tests/test_main.py

Use pytest selectors such as -k to narrow to specific names, e.g.:

uv run --extra test --extra pygments python -m pytest -k 'test_main'

For more information, see [the pytest documentation].

The executable tests

The executable tests verify that the Vehicle compiler is installed as part of the Python package.

Run the following command:

uv run --extra test --extra pygments python -m pytest tests/test_main.py

The loss function tests

The loss function tests cover translating Vehicle specifications into loss functions.

Run the following command:

uv run --extra test --extra pygments python -m pytest tests/test_loss*.py

The pygments tests

The pygments tests verify the integration with [the Pygments syntax highlighter].

Run the following command:

uv run --extra test --extra pygments python -m pytest tests/test_pygments.py

Installing from source

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

Navigate to your local copy of the Vehicle repository.

cd path/to/vehicle

Navigate to the vehicle-python subdirectory.

cd vehicle-python

Build distributable artifacts (wheel + sdist):

uv build

Install the resulting wheel into whichever interpreter you plan to use (outside the uv-managed project):

python -m pip install dist/vehicle_lang-<version>-py3-none-any.whl

Replace <version> with the current version string from dist/.

Check if your installation of the Vehicle compiler was successful.

Run the following command:
```
vehicle --version
```
This should print 0.24.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. Rely on the uv-managed project environment instead of a separate editable install—uv sync automatically installs the local project in editable mode whenever the lockfile changes. After syncing (for example with uv sync --extra test --extra pytorch), you can run pytest directly via uv run:

uv run python -m pytest

You’ll need to re-run uv sync whenever the dependency graph (or the preferred GHC version) changes so that the editable install stays aligned with the lockfile.

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-rocq	Rocq	VsCoq
vehicle-python	Python	Python, Pylance, Black Formatter, isort
vehicle-python	TOML	Even Better TOML