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 (GNAT) is needed to translate the source code into a program that can be executed. Other tools are also needed to perform tasks such as testing, static analysis and formal proof of SPARK code.

This extension does not include a compiler nor additional tools. Nonetheless it offers a number of features out of the box and more capabilities can be accessed by installing additional tools.

Getting Additional Tools

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

AdaCore Customers

If you are an AdaCore customer, 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 (Intel and Apple silicon)
• On Windows with msys2 you can install the gcc and gprbuild packages.

Documentation

• Ada Language Server README.md: VS Code Extension
• Tutorial: Using Ada in VS Code
• Supported refactoring tools
• Custom colors for Ada sources
• Usage in a Remote container example
• Code Samples with Build and Debug tasks

Known Issues and Feedback

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