Skip to content

Latest commit

 

History

History
119 lines (82 loc) · 9.16 KB

README.md

File metadata and controls

119 lines (82 loc) · 9.16 KB
Raw

Ada & SPARK for Visual Studio Code

Repository  |  Issues  |  Documentation  |  Code Samples  |  Tutorial

Build binaries GitHub tag (latest by date) VS Marketplace Open VSX Registry Gitpod ready-to-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.

Features

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.

Without
Additional Tools		 With
Ada Compiler		 With
Ada Compiler & GNATprove
Syntax Highlighting ✅ ✅ ✅
Navigation ✅
(except standard runtime)		 ✅ ✅
Auto-completion ✅
(except standard runtime)		 ✅ ✅
Refactoring ✅ ✅ ✅
Build ✅ ✅
Debug ✅ ✅
Formal Proof ✅

Getting an Ada Compiler or GNATprove

For a fully operational development environment you can obtain a compiler and/or GNATprove from the following channels.

AdaCore Customers

If you are an AdaCore customer, you can log into your account on GNAT Tracker to download the tools available in your subscription.

Community Users

The Ada & SPARK tools are available to the community through different channels:

  • ALIRE: The Ada LIbrary Repository provides the means to install compiler toolchains. The 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 gprbuild package.
  • On Windows with msys2 you can install the gcc and gprbuild packages.
  • On macOS you can find GCC releases including GNAT for Intel and Apple silicon at this project on GitHub courtesy of Simon Wright.

Environment Setup

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 Ada.*.

  • 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 code command.

Alternatively, you can set environment variables through the VS Code Workspace or User setting terminal.integrated.env.[linux|windows|osx] depending on your platform. For example:

{
  "terminal.integrated.env.linux": {
    "PATH": "/path/to/my/gnat/installation/bin:${env:PATH}",
    "GPR_PROJECT_PATH": "/path/to/some-lib-1:/path/to/some-lib-2"
  }
}

Note that after changes to this VS Code setting, you must run the Developer: Reload Window command to apply the changes.

Settings

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.

Documentation

Known Issues and Feedback

You can browse known issues and report bugs at the Ada Language Server GitHub project.