Contributing to Vehicle

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.14.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. Currently, those are 3.7, 3.8, 3.9, 3.10, and 3.11.

Run the following command:
```
pyenv install 3.7 3.8 3.9 3.10 3.11
```
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.14.0-cp311-cp311-macosx_13_0_arm64:

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