Arend plugin for IntelliJ IDEA
Clone or download

Arend plugin for IntelliJ IDEA

JetBrains incubator project Build Status

Plugin that implements Arend support in IntelliJ IDEA and other IntelliJ-based products. Arend is a theorem prover based on Homotopy Type Theory. See the documentation for more information about the Arend language.


git clone
git clone
cd intellij-arend


We use gradle to build the plugin. It comes with a wrapper script (gradlew or gradlew.bat in the root of the repository) which downloads appropriate version of gradle automatically as long as you have JDK installed.

Common tasks are

  • ./gradlew buildPlugin — fully build plugin and create an archive at build/distributions which can be installed into IntelliJ IDEA via Install plugin from disk action found in File | Settings | Plugins.

  • ./gradlew runIde — run a development IDE with the plugin installed.

  • ./gradlew test — run all tests.


You can get the latest Intellij IDEA Community Edition here.

To import this project in IntelliJ, use File | New | Project from Existing Sources and select build.gradle from the root directory of the plugin.

When hacking on the plugin, you may need the following plugins -

  • Grammar-Kit - BNF Grammars and JFlex lexers editor. Readable parser/PSI code generator.
  • PsiViewer - A Program Structure Interface (PSI) tree viewer.

Travis CI

The project is configured to build and run tests with Travis CI, which you can enable in your forks.