• Stars
    star
    230
  • Rank 174,053 (Top 4 %)
  • Language
    Ada
  • License
    GNU General Publi...
  • Created over 7 years ago
  • Updated about 2 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Server implementing the Microsoft Language Protocol for Ada and SPARK

Ada Language Server

Build binaries GitHub tag (latest by date) VS Marketplace Open VSX Registry Gitpod ready-to-code

This repository contains an implementation of the Microsoft Language Server Protocol for Ada/SPARK.

Current features:

  • GNAT project files support.
  • Basic Alire support.
  • Code completion for names, keywords, aggregates, etc.
  • Code navigation, such as Go to Definition/Declaration, Find All References, Call Hierarchies, etc.
  • Code refactoring like insert named associations, auto-add with-clauses, etc.
  • Document/Workspace symbol search.
  • Code folding and formatting.

We also provide Visual Studio Code extension at the VS Marketplace and at the Open VSX Registry.

Table of Contents

Install

You can build language server from sources. To build it from sources install dependencies and run

make

It will build .obj/server/ada_language_server file.

Dependencies

To build the language server you need:

Project files of the libraries must be available via the GPR_PROJECT_PATH environment variable.

If you intend to use VS Code on this workspace, it is recommended to check out these dependencies under subprojects/ or install them under subprojects/prefix. That will make them automatically visible to the VS Code Ada extension in this workspace.

To run the language server you need gnatls (part of GNAT installation) somewhere in the path.

Usage

The ada_language_server doesn't require any command line options, but it understands these options:

  • --tracefile=<FILE> - Full path to a file containing traces configuration
  • --config=<FILE> - Full path to a JSON file containing the server's configuration
  • --help - Display supported command like options and exit.

You can turn some debugging and experimental features through the traces file.

The server also gets configuration via workspace/didChangeConfiguration notification and initializationOptions of initialize request. See more details here. Each LSP client provides its-own way to set such settings. You can use the --config option if you want to provide the configuration directly via a JSON file instead of specifying it via the requests listed just above.

Supported LSP Server Requests

See WiKi page for the list of supported requests.

Protocol Extensions

The Ada Language Server supports some features that are not in the official Language Server Protocol specification. See corresponding document.

VS Code Extension

A VS Code extension based on this Ada Language Server is available on the Visual Studio Marketplace. It provides a full set of features including syntax highlighting, navigation, building and debugging.

Getting Started

Here are some links that will help you get familiar with the VS Code extension for Ada & SPARK:

Configuration

You can configure the extension via the .vscode/settings.json workspace settings file or the multi-root workspace file. See the setting list here.

Here is an example config file:

{
   "ada.projectFile": "gnatcov.gpr",
   "ada.scenarioVariables": {
      "BINUTILS_BUILD_DIR": "/null",
      "BINUTILS_SRC_DIR": "/null"
   },
   "ada.defaultCharset": "utf-8",
   "ada.enableDiagnostics": false,
   "ada.renameInComments": false
}

Refactoring

See a dedicated document with the list of available refactorings.

Tasks

The extension provides the following auto-detected tasks (under /Terminal/Run Task... menu):

  • ada: Build current project - launch gprbuild to build the current GPR project
  • ada: Check current file - launch gprbuild to check errors in the current editor
  • ada: Clean current project - launch gprclean to clean the current GPR project
  • spark: Examine project - launch gnatprove in flow analysis mode on the current GPR project
  • spark: Examine file - launch gnatprove in flow analysis mode on the file in the current editor
  • spark: Examine subprogram - launch gnatprove in flow analysis mode on the current subprogram in the current editor
  • spark: Prove project - launch gnatprove on the current GPR project
  • spark: Prove file - launch gnatprove on the file in the current editor
  • spark: Prove subprogram - launch gnatprove on the current subprogram in the current editor
  • spark: Prove selected region - launch gnatprove on the selected region in the current editor
  • spark: Prove line - launch gnatprove on the cursor line in the current editor
  • spark: Clean project for proof - launch gnatprove on the current GPR project to clean proof artefacts

You can bind keyboard shortcuts to them by adding to the keybindings.json file:

{
  "key": "alt+v",
  "command": "workbench.action.tasks.runTask",
  "args": "ada: Check current file",
  "when": "editorLangId == ada"
}

Task Customization

You can customize auto-detected tasks by providing extra tool command line options via the args property of the configuration object in the tasks.json:

{
   "version": "2.0.0",
   "tasks": [
      {
         "type": "ada",
         "configuration": {
            "kind": "buildProject",
            "projectFile": "${config:ada.projectFile}",
            "args": ["-gargs", "-vh"]
         },
         "problemMatcher": ["$ada"],
         "group": "build",
         "label": "ada: Build current project with custom options"
      }
   ]
}

Commands and Shortcuts

The extension contributes commands and a few default key bindings. Below are a few examples, and other commands can be found by searching for Ada: in the command list.

Ada: Go to other file

This command switches between specification and implementation Ada files. The default shortcut is Alt+O.

Ada: Add subprogram box

This command inserts a comment box before the current subprogram body. The default shortcut is Alt+Shift+B.

Ada: Reload project

This command reloads the current project. The default shortcut is None.

Bug Reporting

You can use the VS Code Issue Reporter to report issues. Just click on the Help -> Report Issue menu, select An extension for the File on entry and Language Support for Ada for the extension name. Put as many information you can in the description, like steps to reproduce, stacktraces or system information (VS Code automatically includes it by default). This will create a GitHub issue in the Ada Language Server repository.

ALS log files can be found under the ~/.als directory (%USERPROFILE%/.als on Windows). Feel free to attach them on the issues, it helps a lot for further investigation, specially when the ALS.IN and ALS.OUT traces are enabled (more info about traces configuration can be found here.)

Limitations and Differences with GNAT Studio

The VS Code extension has a few limitations and some differences compared to GNAT Studio:

  • Indentation/formatting: it does not support automatic indentation when adding a newline and range/document formatting might no succeed on incomplete/illegal code.

  • Tooling support: we currently provide minimal support for SPARK (see Prove/Examine tasks in the Auto-detected tasks section), but there is no support for tools such as CodePeer, GNATcheck, GNATtest or GNATcoverage.

  • Alire support: if the root folder contains an alire.toml file and there is alr executable in the PATH, then the language server fetches the project's search path, environment variables and the project's file name from the crate description.

  • Project support: there is no Scenario view: users should configure scenarios via the ada.scenarioVariables setting (see the settings list available here). You can execute the Ada: Reload project command to reload your project after saving the new scenario values (use the Ctrl+P shortcut to invoke the Command Palette, allowing you to execute commands).

    Source directories from imported projects should be added in a workspace file. If you already have a workspace file, the extension will propose you to automatically add all the source directories coming from imported projects to your workspace automatically at startup.

Integration with other editors and IDEs

Integration with Coc.NVim

If you want to use the Ada Language Server with Vim/Neovim, you can use the Coc.NVim. You'll have to install the Ada Language Server manually somewhere on your computer. Follow installation instructions on Coc.NVim website and then configure the Ada Language Server with :CocConfig:

{
  "languageserver": {
    "ada": {
      "settings": {
        "ada": {
          "projectFile": "gnat/vss_text.gpr"
        }
      },
      "command": "<path>/ada_language_server",
      "filetypes": [
        "ads",
        "adb",
        "ada"
      ]
    }
  }
}

Integration with vim-lsp

If you want to integrate the Ada Language Server into vim, you can use the vim-lsp.

You'll have to install the Ada Language Server manually somewhere on your computer, and then you can add the following line to your .vimrc file:

if executable('ada_language_server')
    au User lsp_setup call lsp#register_server({
        \ 'name': 'ada_language_server',
        \ 'cmd': ['ada_language_server'],
        \ 'allowlist': ['ada'],
        \ 'workspace_config': {'ada': {
        \     'projectFile': "project.gpr",
        \     'scenarioVariables': {"ARCH": "x86_64-pc-linux-gnu"}}},
        \ })
endif

Integration with LanguageClient-Neovim

If you want to integrate the Ada Language Server into Neovim, you can use the LanguageClient-neovim.

You'll have to install the Ada Language Server manually somewhere on your computer, and then you can add the following line to your init.vim file:

" replace the path below with the proper path to the ada_language_server executable
let g:LanguageClient_serverCommands = {
    \ 'ada': ['path/to/ada_language_server'],
    \ }
" if you already have LanguageClient_serverCommands, just add a line for ada.

To configure the Ada Language Server for a specific workspace/project, you can use the .vim/settings.json file. It is mandatory as soon as you want to use a specific .gpr project file.

This is the way to specify a project file, eg. you cannot open a project file another way. See the setting list here.

Here is an example of a settings file:

{
    "ada.projectFile": "project.gpr",
    "ada.scenarioVariables": {
        "GLFW_Version": "3",
        "GLFW_Lib": "-lglfw",
        "Windowing_System": "x11"
    }
}

The location where the .vim folder is located will determine the relative path of the project file (so no need to prefix with ..). When vim is opened in the folder containing this .vim directory, it will use those settings for the language server even for files which might have nothing to do with that specific project, so this needs to be taken into account. Ultimately what this means is that the configuration is determined by where you open vim.

Integration with Neovim's built-in LSP client

Neovim 0.5.0 and later have a built-in LSP client which can be used with the Ada Language Server. In order to use it with minimal effort, follow these steps:

  • Install the ada language server and make sure it's in your $PATH.
  • Use your favorite Neovim plugin manager to add the default set of LSP configuration files to Neovim.
  • Enable the Ada Language Server by adding :lua require('lspconfig').als.setup{} to your init.vim.

If you would rather not have the ada language server in your path, you can give the lsp client an absolute path to the ALS executable:

require('lspconfig').als.setup{ cmd = "/path/to/als/executable" }

Configuring the language server's settings can be achieved like this:

require('nvim_lsp').als.setup{
  settings = {
    ada = {
      projectFile = "project.gpr";
      scenarioVariables = { ... };
    }
  }
}

The Ada Language Server's settings are described here. Configuring neovim to use project-specific settings is described neovim's lspconfig wiki

Integration with emacs lsp-mode

The configuration for each project can be provided using a .dir-locals.el file defined at the root of each project.

The scenario variables should be declared in your .emacs or any loaded Emacs configuration file.

(defgroup project-build nil
  "LSP options for Project"
  :group 'ada-mode)

(defcustom project-build-type "Debug"
  "Controls the type of build of a project.
   Default is Debug, other choices are Release and Coverage."
  :type '(choice
          (const "Debug")
          (const "Coverage")
          (const "Release"))
  :group 'project-build)

Your .dir-locals.el in the project root should be similar to:

((ada-mode .
  ((eval . (lsp-register-custom-settings
      '(("ada.scenarioVariables.BINUTILS_SRC_DIR" project-binutils-dir)
        ("ada.scenarioVariables.BUILD_TYPE" project-build-type "Release"))))
   (lsp-ada-project-file . "/home/username/project/project.gpr"))
  ))

The lsp-mode provides built-in support for the ada_language_server and defines default customizable configuration values in the lsp-ada group that can be edited similarly to lsp-ada-project-file in the example above.

Integration with QtCreator

Starting with version 4.9, QtCreator supports a LSP plugin. Follow the official documentation to configure the Ada Language Server in this plugin. Make sure to set Startup behavior to Start Server per Project, otherwise QtCreator won't provide the project root to the Ada Language Server. QtCreator doesn't send any configuration request to the language server, so the only option to enable project support is to have a single .gpr file in the QtCreator project folder. For a projectless configuration, you could also place all Ada sources in the project root folder, this should work as well.

Refactoring Tools

See corresponding document.

Authors & Contributors

  • Maintained by AdaCore.
  • Original author @MaximReznik.
  • Support for the Visual Studio Code classifier and snippets contributed by @Entomy.

Contribute

Feel free to dive in! Read the developer's guide.

Don't hesitate to open an issue or submit PRs.

License

GPL-3

More Repositories

1

gnatstudio

GNAT Studio is a powerful and lightweight IDE for Ada and SPARK.
Ada
402
star
2

spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
Ada
245
star
3

Ada_Drivers_Library

Ada source code and complete sample GNAT projects for selected bare-board platforms supported by GNAT.
Ada
241
star
4

gnat-llvm

LLVM based GNAT compiler
Ada
182
star
5

libadalang

Ada semantic analysis library.
Ada
146
star
6

aws

AWS is a complete framework to develop Web based applications in Ada.
Ada
127
star
7

gsh

A POSIX shell for Windows.
C
103
star
8

learn

Sources for learn.adacore.com
Ada
93
star
9

gtkada

Ada bindings for the GTK+ graphical library.
Ada
88
star
10

langkit

Language creation framework.
Python
79
star
11

gprbuild

GPRbuild is an advanced build system designed to help automate the construction of multi-language systems.
Ada
65
star
12

svd2ada

An Ada binding generator from SVD descriptions for bare board ARM devices.
Ada
64
star
13

bb-runtimes

Source repository for the GNAT Bare Metal BSPs
Ada
64
star
14

ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63
star
15

VSS

High level string and text processing library
Ada
53
star
16

gnatcoll-core

GNAT Components Collection – Core packages
Ada
45
star
17

gnatcoverage

GNATcoverage: Coverage Analysis Tool
Ada
36
star
18

Certyflie

Ada
32
star
19

ada-traits-containers

Generic Ada Library for Algorithms and Containers
Ada
29
star
20

why3

SPARK 2014 repository for the Why3 verification platform.
OCaml
29
star
21

startup-gen

A startup code generator for embedded projects
Ada
28
star
22

e3-core

Core framework for developing portable automated build systems
Python
26
star
23

git-hooks

Git hooks Python-based scripts
Python
24
star
24

xmlada

The XML/Ada toolkit.
Ada
22
star
25

Ada-IntelliJ

Support for Ada and SPARK languages in IntelliJ IDEA
Java
21
star
26

OPAVES

Open Platform for Autonomous VEhicle Systems
C
21
star
27

training_material

Ada
20
star
28

PolyORB

PolyORB provides a uniform solution to build distributed applications relying either on middleware standards
Ada
20
star
29

Ada-SPARK-Crate-Of-The-Year

19
star
30

gnat_community_install_script

Script to automate the installation of the GNAT Community Installers
Shell
18
star
31

cuda

Ada
18
star
32

win32ada

Ada API to the Windows library
Ada
17
star
33

spawn

Ada
16
star
34

Robotics_with_Ada

Robotics with Ada, ARM, and Lego
Ada
16
star
35

gpr

The framework for analyzing the GNAT Project (GPR) files
Ada
16
star
36

libadalang-tools

Libadalang-based tools
Ada
16
star
37

gnat-gdb-scripts

GDB scripts for Ada programs built with GNAT
Python
16
star
38

gnatcoll-bindings

GNAT Components Collection – Bindings to C libraries
Ada
14
star
39

embedded-runtimes

runtimes that add support for various boards to the GNAT GPL compiler for ARM
Ada
14
star
40

adareducer

Python
13
star
41

qemu

C
12
star
42

gnatcoll-db

GNAT Components Collection – Database packages
C
11
star
43

sparkformal

The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq.
Coq
11
star
44

UnityAdaTetris

Ada
10
star
45

markdown

Markdown parser
Ada
9
star
46

labs-material

Support Libraries for AdaCore University Labs
Ada
7
star
47

templates-parser

AWS templates engine.
Ada
7
star
48

florist

Ada
6
star
49

ada-py-bind

Ada
6
star
50

e3-testsuite

e3 testsuite driver
Python
6
star
51

spdm-recordflux

6
star
52

RC_Car_Demo

An embedded Ada/SPARK demo
Ada
6
star
53

RESSAC_Use_Case

A Collaborative Development Assurance Lab
Ada
6
star
54

aunit

Ada
6
star
55

SPARK_Railway_Simulation_Demo

Ada
5
star
56

Http_Cyclone

C
5
star
57

Compile_And_Prove_Demo

Demo project for new web site: Compile It! / Prove It!
Ada
5
star
58

program_proofs_in_spark

This repository contains some programs from Rustan Leino's book "Program Proofs" verified with SPARK.
Ada
5
star
59

gnat-docker

Python
5
star
60

gnatdashboard

Analyse a project.
Python
4
star
61

AdaSAT

Ada
4
star
62

e3-aws

High level interface for CloudFormation
Python
4
star
63

Platinum_Reusable_Stack

Ada
4
star
64

wposix

Ada Windows POSIX binding
Ada
4
star
65

code_examples_server

prototype server for creating interactive "try SPARK / try Ada" webpages
Python
3
star
66

lmod_manager

lmod based management tool for GNAT and SPARK installations
Python
3
star
67

SPARK_PDI_Demo

Use of SPARK to implement Parameter Data Items
Ada
3
star
68

langkit-query-language

query language for Libadalang and Langkit
Ada
3
star
69

gprconfig_kb

GPR configuration knowledge base
3
star
70

tictactoe

A tictactoe game written and proven in SPARK
Ada
3
star
71

language-examples

Examples of common software engineering constructs written in Ada and SPARK
Ada
3
star
72

ada_coding_standards

Ada
2
star
73

cheri-examples

Ada
2
star
74

style_checker

The AdaCore style checker
C
2
star
75

gpr-unit-provider

GPR2 based unit provider for Libadalang
Ada
2
star
76

gnatdoc

GNAT Documentation Generator
Ada
2
star
77

Lunar_Lander_Rotation_Demo

Demonstration program that interacts with the AdaFruit BNO055 breakout board in order to send orientation data to a host computer
Ada
2
star
78

RecordFlux-parser

Python
2
star
79

training_labs_radar

Ada
2
star
80

RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
2
star
81

uwrap

Ada
1
star
82

z3

SPARK 2014 repository for the Z3 SMT solver.
C++
1
star
83

lal-checkers

Libadalang-based code checking infrastructure
Python
1
star
84

spark_translator

SPARK 2005 to 2014 translator
Python
1
star
85

Lumos_Maxima

Lumos_Maxima repository for VerifyThis challenge
Ada
1
star
86

training_labs_solar_system

Ada
1
star
87

training_labs_standalone

Ada
1
star
88

gnatcoll

GNAT Components Collection (obsolete)
1
star
89

sphinxcontrib-adadomain

Python
1
star
90

alt-ergo

SPARK 2014 repository for the Alt-Ergo SMT solver.
OCaml
1
star
91

lsif-ada

Ada
1
star
92

prettier-ada

Ada
1
star
93

SPARK-to-C_Tetris_Demo

Ada
1
star
94

lal-refactor

Ada
1
star
95

RecordFlux-devutils

1
star