VS Code

If you use VS Code, you can also install the Imandra IDE Extension plugin to help with development, providing things like completion and syntax highlighting as well as full asynchronous proof checking and semantic editing, meaning you can see proved theorems, counterexamples and instances within the IDE as you type.

In order to install the standard extension, first follow the instructions above for installing Imandra. Then in VSCode itself VSCode go to the extensions view by following the instructions about the Extension Marketplace and searching for Imandra IDE.

The extension will open automatically when a file with extension .iml or .ire is opened. The extension will look for the correct version of ocamlmerlin on the opam switch associated with the folder in which the opened .iml or .ire file resides (defaulting to the current global switch). We recommend that the current global switch is that produced by the recommended installation of Imandra, as that contains all the artifacts to facilitate correct Imandra type inference, asynchronous proof checking and other language server features. Below are example images of the type information the Imandra IDE provides in VSCode.

With Simple Installation

If you have used the Simple installation instructions for Imandra then the VSCode extension should work automatically. If you're on Windows and have installed Imandra under WSL, you need to enable the extension to work under WSL

With Manual Installation

If you have used the Manual installation instructions for Imandra then it is necessary to modify some of the settings in VSCode by hand.

Pressing CMD+, takes you to the settings section of VSCode. It is necessary to alter the following settings:

  • Search for the setting imandra_merlin and enter here the result of typing which imandra-merlin in a terminal where you installed Imandra. So for example if you had installed Imandra in ~/imandra you would add for this setting:
Ready!
~/imandra/imandra-merlin
  • Search for the setting imandra-vscode-server and enter here the result of typing which imandra-vscode-server then -server then which imandra_network_client in a terminal where you installed Imandra. So for example if you had installed Imandra in ~/imandra you would add for this setting:
Ready!
~/imandra/imandra-vscode-server -server ~/imandra/imandra_network_client

As is shown in the following screen shot.

Example settings screen