Ada & SPARK for Visual Studio Code
This extension provides support for the Ada and SPARK programming languages in VS Code via the Ada Language Server based on the Libadalang library.
Ada and SPARK are compiled languages which means that a compiler is needed to translate the source code into a program that can be executed.
Additionally if your source code uses the SPARK subset of Ada, you can perform formal proof on it using GNATprove.
Even though this extension does not include a compiler nor a proof tool, a number of features are available without those tools, and it is easy to obtain them if needed.
Ada Compiler & GNATprove
(except standard runtime)
(except standard runtime)
Getting an Ada Compiler or GNATprove
For a fully operational development environment you can obtain a compiler and/or GNATprove from the following channels.
If you are an AdaCore customer, you can log into your account on GNAT Tracker to download the tools available in your subscription.
The Ada & SPARK tools are available to the community through different channels:
- ALIRE: The Ada LIbrary Repository provides the means to install compiler toolchains.
gnatprove crate provides GNATprove.
Both tools are available for Linux, Windows and macOS.
- On Linux distributions you can use your package manager to install GCC which includes the GNAT Ada compiler.
You also need to install the
- On Windows with msys2 you can install the
- On macOS you can find GCC releases including GNAT for Intel and Apple silicon at this project on GitHub courtesy of Simon Wright.
The following environment variables influence the operation of the Ada extension:
PATH should include the path to the GNAT compiler installation in order to benefit from auto-completion and navigation into the standard runtime.
Without it, auto-completion and navigation will work only on the sources visible in the project closure, but not on the packages of the standard library
GPR_PROJECT_PATH provides paths to other
.gpr Ada projects that your project depends on.
When running VS Code locally, you can provide these environment variables by exporting them in a terminal, and starting VS Code from that same terminal with the
Alternatively, you can set environment variables through the VS Code Workspace or User setting
terminal.integrated.env.[linux|windows|osx] depending on your platform.
Note that after changes to this VS Code setting, you must run the
Developer: Reload Window command to apply the changes.
This extension can be configured with a set of
ada.* settings documented here.
The most prominent one is
ada.projectFile where you can provide the path to the
.gpr project file.
If no project is provided and if your workspace contains a single project file at the root, then that one will be automatically used.
VS Code Remote
The Ada extension can be used on a remote workspace over SSH thanks to the Visual Studio Code Remote - SSH extension, however there are known pitfalls regarding the environment setup.
The recommended method for environment setup in a remote configuration is to set the
terminal.integrated.env.* settings as described in the Environment Setup section.
In addition to Workspace and User settings, the Remote settings file can also be used to set the
terminal.integrated.env.* settings, with standard precedence rules applying between the different setting scopes.
With this method, changes to the environment can be applied simply with the
Developer: Reload Window command.
Another method for environment setup is possible.
According to VS Code documentation the environment of the remote extension host is based on the default shell configuration scripts such as
~/.bashrc so it is possible to provide your toolchain and project environment setup in your default shell configuration script.
However to make changes to that environment the typical
Developer: Reload Window command is not enough and it is necessary to fully restart the VS Code server.
To do that you must close all VS Code Remote windows, and kill all VS Code server processes on the server (e.g.
killall node if no other
node processes are used on the server).
macOS and Apple Silicon
On macOS with Apple silicon it is possible to use either the native
aarch64 version of the GNAT compiler or the
x86_64 version running seamlessly with Rosetta.
If you are using the
aarch64 version, as this is still a relatively new platform for Ada tools, it is necessary to set the following attribute in your main project file to obtain navigation and auto-completion functionalities on the standard runtime:
for Target use "aarch64-darwin";
If you encounter issues with the compiler on macOS, it is recommended to consult known issues at Simon Wright's GitHub project and discussions on the comp.lang.ada group.
Known Issues and Feedback
You can browse known issues and report bugs at the Ada Language Server GitHub project.