Language Server Protocol server for Certora's EVMSpec files (.spec, .cvl).
Installation
Java 11 or later is required.
Features
syntax error, in case of syntax error, only the first error will be marked with red wavy line and will be shown in the problems tab. after fixing the error, the next error will emerge and so on.
syntax highlighting, displays the CVL code in different colors according to the category of terms.
Upcoming features
format which formats the source code based on user configuration
completion, which is a set of file-local hints what should be offered as typing instruction both regardless, and regarding, what is the current scope
goto_definiton, which jumps to the initial declaration of the variable that is currently hovered or highlighted
references, which corresponds to "find usage" functionality within the current file, and the current workspace
signature_help, which gives hints and general information to the user about how some method or function should be completed
folding_range, which commands the logic how folding of .spec files should be done
rename, which comamnds the logic how renaming of .spec files should be done
document_symbol and semantic_tokens_full, which gives extra syntactic information to the client, and thus can be used to achieve syntax highlighting that is more powerful that simple regexes available to be defined on the client's spec.tmLanguage.json file
hover, which provides contextualized information on the data that is shown when hovering an arbitrary location on the .spec files
code_lens which provides inlined text within the file to hint, e.g., to display types of variables after declarations
code_action which provides a selection of actions which the user might be interested in, e.g., information from Solidity side but on the .spec files
