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

Clone

git clone https://github.com/JetBrains/Arend
git clone https://github.com/JetBrains/intellij-arend.git
cd intellij-arend

Building

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 (version >= 11) 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.

Developing

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 the root directory of the plugin source code.

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.