Installation

At the moment, the only way to install Vehicle is from source. We aim to make it available as both an executable and a Python package in the near future.

Building from source

On Linux

Vehicle is written in Haskell. The first task is to install Haskell itself:

  1. Install GHCUp following the instructions from https://www.haskell.org/ghcup/.

  2. Close and reopen your terminal.

  3. Run ghcup tui and use it to install and set:

  • GHC 9.0.X (for some version of X)

  • Cabal 3.X (for some version of X)

  1. Run cabal update to update your list of packages.

Now we can install Vehicle itself.

  1. Clone the Vehicle github repository to your local computer and navigate to the directory.

  2. Run git checkout v0.2.0 to check out the latest version (change the version as required).

  3. Run cabal install exe:vehicle to install the Vehicle executable on your system.

  4. Run vehicle -h to check that Vehicle has been installed.

(If this doesn’t work then check that check that ~/.cabal/bin has

been added to your system path.)

Troubleshooting

  • Check if you’re using the right versions of GHC and Cabal.

  • Check if you have any other installations of GHC and Cabal not managed by GHCUp. Either remove those installations or make sure that GHCUp is earlier in the PATH environment variable.

Updating Vehicle

To update an existing Vehicle installation:

  1. Navigate to the existing Vehicle repository.

  2. Run git checkout vX to check out the latest version (choose the version as required).

3. Run cabal install exe:vehicle --overwrite-policy=always to re-install the new Vehicle executable on your system.

On Windows

The easiest way is:

  • Install the Windows Subsystem for Linux (WSL) from the Microsoft Store.

  • Follow the instructions for Linux above in a WSL terminal.

Warning

Although Vehicle itself supports and is tested on Windows, that does not mean that all backends will work on Windows. For example Marabou does not currently support Windows.

Troubleshooting

  • If you have problems with the WSL check if you’re using the latest version.

  • If you get the error: Missing (or bad) C libraries: icuuc, icuin, icudt

Go to https://github.com/microsoft/vcpkg#quick-start-windows and follow the instructions.

Setting Vehicle to work with Agda

If you want to enable Vehicle to work with Agda, run:

  1. Run cabal run vehicle-build-system init-agda

This command will add the Vehicle Agda library to the Agda libraries file and add the vehicle executable to the Agda executables file.

The command does not install the vehicle library in your Agda defaults file. Before using an Agda file generated by Vehicle you will need to add vehicle to either your library’s .agda-lib file or to your Agda defaults file.

See the Agda documentation on Library Management for more details.

Syntax highlighting

The syntax highlighting can be installed in VSCode by going to the “Extensions” tab and searching for “Vehicle Syntax Highlighting”.

Contributions adding syntax highlighting to other IDEs would be welcome. The source code for the VSCode extension is available here.