Getting Started

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 (see IntelliJ Arend for the installation instructions) or as a console application (see Console Application for the installation instructions).

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.

Let’s create our first Arend project.

  • Run Intellij IDEA and choose either Create New Project if you are on a Welcome screen or File | New | Project from the main menu if a project is open.
  • Choose Arend in the list on the left. If you want to use external libraries, for example, the standard library, you can set up the path to a directory with these libraries in the field Path to libraries. Available libraries will be displayed in the list on the right. To add them to the project, move them to the left list. The standard library arend-lib is always available; it will be downloaded if the file is missing.
  • Click Next. In the successive step set up the name of the project and the path to it and click Finish.

You should get a new project which contains (among other files) a file arend.yaml and an empty source directory (src by default). The yaml file contains a description of the project. You can read more about this configuration file here.

Now, let us write some code. Create a new file Example.ard in the source directory. Add the following line to this file:

\func f => 0

You should see a green gutter icon next to the declaration of f, which indicates that f was successfully typechecked. Modify the file as follows:

\func f : Nat -> Nat => 0

The gutter icon should become red. To go to the next error, press F2. You should see the following error message:

Type mismatch
  Expected type: Nat -> Nat
    Actual type: Nat

You can read more about IntelliJ IDEA here. To learn more about Arend, see the language reference. Also, check out the tutorial on interactive theorem proving with IntelliJ Arend.

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.

Let’s create our first Arend project. Create a directory for your project:

$ mkdir testProject
$ cd testProject

Create file arend.yaml inside this directory. This file contains the description of your project. Minimally, we just need to specify the location of source files of your project. Add the following line to arend.yaml:

sourcesDir: src

Create directory src which will contain source files for this project. Create a file Example.ard inside src with the following content:

\func f => 0

Run java -jar $arend $myProject, where $arend is the path to arend.jar, $myProject is the path to arend.yaml or the directory containing it, and you can optionally pass -L$libs where $libs is the path to the directory with Arend libraries (if the project does not have dependencies, this option can be omitted). When $myProject equals ., it can be omitted. You should see the following output:

[INFO] Loading library prelude
[INFO] Loaded library prelude
[INFO] Loading library myProject
[INFO] Loaded library myProject
--- Typechecking myProject ---
[ ] Example
--- Done ---

This means that module Example was successfully typechecked. Modify file Example.ard as follows:

\func f : Nat -> Nat => 0

If you run java -jar $arend $myProject again, it should produce the following error message:

[INFO] Loading library prelude
[INFO] Loaded library prelude
[INFO] Loading library myProject
[INFO] Loaded library myProject
--- Typechecking myProject ---
[ERROR] Example:1:25: Type mismatch
  Expected type: Nat -> Nat
    Actual type: Nat
  In: 0
  While processing: f
[✗] Example
Number of modules with errors: 1
--- Done ---

To learn more about Arend, see the language reference.

Standard Library

In case you would also like to use the standard library, download it as described here (if you are using the IntelliJ plugin, it can be downloaded from the IDE) and add the following line to arend.yaml:

dependencies: [arend-lib]

You can read more about this configuration file here.