[Enhancement]: Make the Ada Language Server automatically SPARK‑aware

[berkeleynerd]

Enhancement Request

Explanation

When source code is in SPARK_Mode => On (via aspect, pragma, or project configuration), ALS should restrict all LSP features (completion, diagnostics, signature help, etc.) to the SPARK subset of Ada. The goal is to prevent non‑SPARK constructs from being suggested or silently accepted and to make SPARK development smoother and more accurate.

Expected behavior

In SPARK mode, completions should exclude disallowed features (e.g., tasking, unrestricted general access types, etc.) and actively propose SPARK contracts and idioms (Pre, Post, Global, Depends, use of 'Old, etc.). Diagnostics should flag use of non‑SPARK constructs immediately; hovers/definition lookups should prioritize or clearly mark SPARK‑valid entities; and refactorings/code actions should preserve SPARK compliance. Non‑SPARK units continue to receive full Ada behavior.

Activation & Scope

Behavior should be automatic based on SPARK_Mode, with granularity matching where it applies (per unit/spec/body or subprogram) and respecting project‑wide configuration pragmas. A manual override setting (e.g., auto/on/off) is acceptable but optional. This request targets LSP‑level semantics only (not GNATprove integration), though SPARK‑oriented completion and diagnostics are in scope.

[berkeleynerd]

I've added this enhancement request at the encouragement of developers in the Matrix channel who responded to my inquiry regarding availability of this feature in ALS. Thanks for considering it!

[AnthonyLeonardoGracio]

Hello @berkeleynerd,

That's a very interesting idea but not trivial (at all) to implement. We'll discuss about it internally.

Regards,

[berkeleynerd]

Thanks for considering the request and for all the great work you're doing to modernize access to the language.