aya-dev

aya-dev copied to clipboard

Download

You may download the latest build of Aya from GitHub Releases. It's updated for per-commit to the main branch, but the release date displayed is very old and is an issue of GitHub.

There are prebuilt binaries for Windows, Linux, and macOS that can be used in Java-free environments as well as fat-jar files which can be invoked via java --enable-preview -jar.

The minimum required version of Java is Java 18.

Aya is under active development, so please expect bugs, usability/performance issues (please file issues or create threads in discussions!). However, we can share some cool stuffs here:

• Dependent types, including pi-types, sigma types, etc. You could write a type-safe interpreter.
• Arend-ish interval type which is used to define the HoTT path type and prove regularity by computation thanks to Arend's type theory. We also have the classic cubical-flavored funExt.
  • We are considering moving to cubical type theory.
• Pattern matching with first-match semantics. We can implement redblack tree (without deletion) elegantly.
• Overlapping and order-independent patterns. Very useful in theorem proving.
• A literate programming mode with inline code fragment support. We already have a prototype, but we plan to revise it before sharing demos.
• Binary operators, with precedence specified by a partial ordering (instead of a number, such as in Haskell or Agda) which is useful for equation reasoning.
• Termination checker inspired from foetus. We adapted some code from Agda's implementation to accept more definitions (which are rejected by, e.g. Arend).
• Inference of type checking order. That is to say, no syntax for forward-declarations is needed for mutual recursions.

See also use as a library.

Build

Since you need Java 18 to set this project up, in case your choice of IDE is IntelliJ IDEA, version 2021.2.1 or higher is required. If you have problems downloading dependencies (like you are in China), check out how to let gradle use a proxy.

# build Aya and its language server as applications to lsp/build/image
# the image is usable in Java-free environments 
./gradlew jlink --rerun-tasks
# build Aya and its language server as executable
# jars to <project>/build/libs/<project>-<version>-fat.jar
./gradlew fatJar
# build a platform-dependent installer for Aya and its language
# server with the jlink artifacts to lsp/build/jpackage
# requires https://wixtoolset.org/releases on Windows
./gradlew jpackage
# run tests and generate coverage report to build/reports
./gradlew testCodeCoverageReport
# (Windows only) show the coverage report in your default browser
./gradlew showCCR

Contributing to Aya

• Questions or concerns are welcomed in the discussion area. We will try our best to answer your questions, but please be nice.
• We welcome nitpicks on error reporting! Please let us know anything not perfect. We have already implemented several user-suggested error messages.
• Before contributing in any form, please read the contribution guideline thoroughly and make sure you understand your responsibilities.
• Please follow the Code of Conduct to ensure an inclusive and welcoming community atmosphere.
• Ask @ice1000 to become an organization member.
  • If you want to contribute, ask before doing anything. We will tell you about our plans.

Use as a library

It's indexed in mvnrepository, and here are some example build configurations:

<!-- Maven -->
<dependency>
    <groupId>org.aya-prover</groupId>
    <artifactId>[project name]</artifactId>
    <version>[latest version]</version>
</dependency>

// Gradle
implementation group: 'org.aya-prover', name: '[project name]', version: '[latest version]'

• [project name] specifies the subproject of Aya you want to use, and the options are pretty, base, cli, parser, etc.
  • The type checker lives in base and parser.
  • The generalized pretty printing framework is in pretty.
  • The generalized binary operator parser, generalized tree builder, generalized mutable graph, and a bunch of other utilities (strings, files, etc.) are in tools.
  • The command and argument parsing framework is in tools-repl. It offers an implementation of ANTLR4-based jline3 parser and relevant facilities.
• [latest version] is what you see on this badge .