Download

You need to have JRE 11 installed on your computer to use Arend. You are free to choose any alternative JRE distributions such as the Liberica JRE, as long as the version fits the requirement.

Arend is available either as an IntelliJ IDEA plugin or as a console application.

IntelliJ Arend

IntelliJ Arend is a plugin for IntelliJ IDEA. To install it, follow the instructions below.

  • Download (either community or ultimate version of) IntelliJ IDEA.
  • Run Intellij IDEA, choose either Configure | Plugins if you are on a Welcome screen or File | Settings from the main menu if a project is open, go to Plugins tab, search for Arend plugin and install it, restart Intellij IDEA.
  • Another way to get the latest version of the plugin is by following instructions on GitHub.

You can read more about IntelliJ IDEA here. To create an Arend project, follow instructions here.

Console Application

To install the console application, follow the instructions below.

  • Download the Arend jar file. You can also get the latest version of the application by following instructions on GitHub.
  • Run java -jar Arend.jar to check that everything is alright. You should see an output similar to the following:
$ java -jar Arend.jar
[INFO] Loading library prelude
[INFO] Loaded library prelude (233ms)
Nothing to load

To see command line options, run java -jar Arend.jar --help.

To create an Arend project, follow instructions here.

Standard Library

The standard library contains a number of essential definitions and proofs, in particular, in constructive algebra and homotopy theory. It can be downloaded from GitHub (if you are using the IntelliJ plugin, it can be downloaded from the IDE). This file should be put in some specific directory libs in which all Arend libraries are stored. The path to libs can be specified either with command line option -L in the console application or in module settings in IntelliJ IDEA.