Download

You need to have JRE 8 installed on your computer to use Arend. 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 the following output:
$ java -jar arend.jar
[INFO] Loading library prelude
[INFO] Loaded library prelude
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. It should be unpacked and the directory arend-lib 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.