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 withms
for miliseconds,s
for seconds,m
for minutes, orh
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-plan
s, 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 thanvehicle
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 thetest.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, inVehicle.Compile.Descope.descopeNormExpr
there is some disabled code that attaches that information toprettyVerbose
.
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.11.1
.
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.11.1-cp311-cp311-macosx_13_0_arm64
:
# Supported
# Python _____
# versions \
# vvvvvvvvvvv
vehicle_lang-0.11.1-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 invehicle-python/scripts
. This script may ask you to install additional dependencies viapip
. 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 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.11.1
.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.
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 |
|
any |
Haskell |
|
any |
Cabal |
|
any |
Markdown |
|
vehicle-agda |
Agda |
|
vehicle-python |
Python |
|
vehicle-python |
TOML |