Install Aya

At this stage of development, we recommend using the nightly version of Aya. Go to GitHub Release, there will be a plenty of files. It's updated per-commit in the main branch, but the release date displayed is very old and is an issue of GitHub itself.

Checking the section below that fits your platform. After the installation, run aya --help for general instructions and aya -i to start an interactive REPL. If you chose the jlink version, the bin folder contains the executable scripts.

Download from GitHub Release

Aya is available for Windows, Linux, and macOS, as listed below.

	x64	aarch64
Windows	zip	zip
Linux	zip	zip
macOS	zip	zip

Here's a hands-on script I wrote to (re)install Aya to $AYA_PREFIX (define the variable somewhere or replace with your preferred prefix, e.g. /opt/aya) on Linux x64:

#!/bin/bash
sudo mkdir -p ${AYA_PREFIX:-/tmp}
sudo chown $USER ${AYA_PREFIX:-/tmp}
rm -rf ${AYA_PREFIX:-/tmp}/*
cd ${AYA_PREFIX:-/tmp}
wget https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_linux-x64.zip
unzip aya-prover_jlink_linux-x64.zip
rm aya-prover_jlink_linux-x64.zip
cd -

If it's the first time you install Aya, you may want to do (or replace ~/.bashrc with your shell's rc file):

echo 'export PATH="$AYA_PREFIX/bin:$PATH"' >> ~/.bashrc
source ~/.bashrc

Try/Install Aya using Nix package manager

Make sure you have Nix installed with experimental features nix-command flakes.

NOTE: We host our binary cache on Cachix to save you from compilation hell, which can be used by adding the following content in nix.conf:

substituters = https://cache.nixos.org https://aya-prover.cachix.org
trusted-public-keys = aya-prover.cachix.org-1:BNuUD9aNZMDmYISC77aqZfzP4l9XtTHQvYwPhKO+Msg=

or in flake.nix:

nixConfig = {
    extra-substituters = [ "https://aya-prover.cachix.org" ];
    extra-trusted-public-keys = [ "aya-prover.cachix.org-1:BNuUD9aNZMDmYISC77aqZfzP4l9XtTHQvYwPhKO+Msg=" ];
};

or through Nix CLI options:

nix <subcommand> \
    --option extra-substituters "https://aya-prover.cachix.org" \
    --option extra-trusted-public-keys "aya-prover.cachix.org-1:BNuUD9aNZMDmYISC77aqZfzP4l9XtTHQvYwPhKO+Msg="

Nix3 CLI

Activate the devShell containing Aya:

nix shell github:aya-prover/aya-dev#aya

Or Install Aya in user profile:

nix profile install github:aya-prover/aya-dev#aya

Usage in flake.nix

Add flake input in flake.nix:

inputs.aya-dev.url = "github:aya-prover/aya-dev";

Then you can access Aya under inputs.aya-dev.packages.${system}:

• aya : aya (with standard library) + aya-lsp
• aya-minimal: aya (without standard library) + aya-lsp
• aya.withPackages (p: [ p.foo p.bar ]): aya (with libraries foo and bar) + aya-lsp

You may fetch an example flake.nix which provides an Aya devShell with flake-parts:

nix flake init -t github:definfo/dev-templates#aya

# Enter the devShell
nix develop
# OR auto-activate devShell within current directory
direnv allow

Use Aya in GitHub Actions

If you want to use Aya in your GitHub Actions workflow, you can use aya-prover/setup-aya like

- name: Setup Aya
  uses: aya-prover/setup-aya@latest
  with:
    version: 'nightly-build'

The step above will install the latest version of Aya to PATH. You can find the complete example here.

If you already have Java runtime...

Very cool! Now you can try the prebuilt jars (much smaller and platform-independent) or build Aya from source.

We will (hopefully) always be using the latest release of Java, rather than LTS, unless there are breaking changes on the byte code format.

Prebuilt binary

Download the jar version of cli (for using command line) and lsp (for using VSCode) and run it with java --enable-preview -jar [file name].jar.

Build from source

Clone the repository. Then, run build with ./gradlew followed by a task name. 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 `ide-lsp/build/image/current`
# the image is usable in Java-free environments 
./gradlew jlinkAya --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 ide-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

Gradle supports short-handed task names, so you can run ./gradlew fJ to invoke fatJar, tCCR to invoke testCodeCoverageReport, and so on.