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 https://github.com/JetBrains/Arend
git clone https://github.com/JetBrains/intellij-arend.git
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.

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