The Imandra CLI,
imandra, allows you to use Imandra's cloud APIs to create instances of Imandra Core in the cloud, submit IPL jobs, and more. The CLI is
python based (it requires
python3), and can be used from Unix, MacOS and Windows.
Install the Imandra CLI
imandra on MacOS or Unix systems running the command below in a terminal:
sh <(curl -s "https://storage.googleapis.com/imandra-do/install.sh")
On Windows, you can use the command below from a powershell terminal:
(Invoke-WebRequest https://storage.googleapis.com/imandra-do/install.ps1).Content | powershell -
Installation of Imandra Core¶
Imandra Core is based on OCaml, and is supported natively on MacOS and Unix. On Windows you'll need to use WSL.
If this installation process is not an option for you, you can still use Imandra by spawning an Imandra Core instance in our cloud using the Imandra CLI.
In order to use Imandra Core tools such as our Imandra REPL, you additionally need a local OCaml environment to be setup. The installer will set up a new OCaml environment (using the
opam installer), and then install Imandra. Invoke the installer by running:
imandra core install
The installer will:
- Check for the presence of the opam package manager
- If not present it will install version 2 for the current user
- If present it will upgrade the current installation to version 2, if necessary
- Setup an OCaml 4.12.1 environment for Imandra
- Download, setup and install Imandra into its OCaml environment in
/usr/local/var/imandra/(documentation for Imandra modules can be found in
- Install system-level binaries for the Imandra repl and its utilities
The entire setup process will take a while. The process is almost entirely automatic but you might be prompted for input a couple of times, either to authenticate using
sudo or for setting installation paths (we recommend using the default options).
After the installation is finished, you should have the following binaries installed in your installation path (
/usr/local/bin unless you specified a custom one):
imandra: this is the main Imandra entrypoint
imandra-repl: this is the Imandra repl
imandra-http-server: an http api around core Imandra features, with endpoints for evaluation, verification, instance generation etc. For more information, hit the
/specendpoint when the server is running for a full specification of endpoints and request/response formats for the version you have installed.
imandra-jupyter-kernel: an Imandra kernel for Jupyter notebooks. See Jupyter installation instructions for further details.
imandra-extract: a utility to transpile files from IML syntax into either OCaml or Reason syntax
The following tooling utilities will also be installed alongside the main binaries, they are used to provide merlin integration for IDEs while writing or editing Imandra code: