Imandra is both a programming language and a reasoning engine with which you can analyse and verify properties of your programs. This VSCode plugin allows you to develop files which can be analysed by imandra, and incorporates a specific merlin extension which provides information on underlying types and completions.
In order to learn more about imandra, please visit the interactive documentation pages.
## System requirements
It is necessary that you have the executables
ocamlmerlin-imandra installed on your system. All the imandra-specific components required are installed automatically by following the instructions provided here.If installed using opam - the OCaml package manager - the switch detected by VSCode will be the same as if using opam from the directory which corresponds to your workspace root. For example - if you open a directory
~/my_imandra_project/ which has a local switch then the switch in which
ocp-indent is executed will be this local switch. If no local switch exists, then the default global switch will be used.
Alternatively you can use systems such as esy with which you can configure the installation of executables such as
In order for the
refmt commands to work (for example on automatic code-formatting), these must be installed either globally or on the local switch.
This VSCode extension builds on the existing excellent OCaml and Reason IDE for Reason and OCaml files. It provides a mirror of the environment variables for each of the possible commands, and code actions function exactly the same as from this repository.
This extension provides a syntax highlighter is provided for imandra files with extension
.iml, by which the
imandra language is identified, which provides identifiable syntax highlighting for the extra reasoning related keywords in imandra such as
theorem. It also highlights files with a
.ire extension, by which the
imandra-reason language is identified, and provides highlighting for the same reasoning related keywords.
By default, merlin uses specific readers to analyse
At present the
imandra-reason reader extensions for merlin provide:
- basic syntax error highlighting
- type error information
- type information of the underlying
- general syntax completions
All code actions and commands are inherited from the OCaml and Reason IDE extension, but the behaviour of merlin is specific to imandra.