• Building
  • Common Gradle Tasks
  • Developing in IntelliJ IDEA
• Project Structure

Building

We use gradle to build the compiler. 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 Gradle Tasks

All gradle tasks are case-insensitive.

Command	Description
./gradlew :cli:jarDep	build a jar file which includes all the dependencies which can be found at cli/build/libs. A short-hand version of this task is ./gradlew jarDep.
./gradlew :cli:copyJarDep	build jarDep and copy it to the current directory. A short-hand version of this task is ./gradlew copyJarDep.
./gradlew :api:assemble	build Arend extension API jar which can be found at api/build/libs.
./gradlew test	run all tests.

On Windows, you may replace ./gradlew with gradlew.

To see the command line options of the application, run java -jar cli-[version]-full.jar --help after running the jarDep task.

Developing in IntelliJ IDEA

Here's an instruction on how to work with gradle projects in IntelliJ IDEA.

You may also need the following plugins:

• Gradle and Groovy -- bundled plugins, needed for building the project
• ANTLR v4 grammar for editing the parser
• Protobuf for editing the serialized protobuf
• Kotlin for editing the build scripts
• Arend for editing Arend code

Project Structure

Arend is split into several subprojects:

Subproject	Description
buildSrc	built before the project is built. This subproject runs the ANTLR parser generator.
parser	the generated ANTLR parser (the generation is done in buildSrc)
proto	generated protobuf classes.
api	open API for writing Arend extensions.
base	the Arend typechecker. It depends on api, proto.
cli	the CLI frontend of Arend with the ANTLR parser. It depends on base, parser, api, proto.

The purpose of parser is to avoid introducing the dependency of the ANTLR generator to other subprojects which only requires the generated parser along with a small ANTLR runtime (since it's a dependency of buildSrc instead of parser).

The root project contains all the tests, and it depends on project cli. The tests are based on JUnit 4. If you want to move tests to a separate subproject, we wish you good luck.