Skip to content

Athena Installation Instructions

Jump to bottom
Tak edited this page Jun 25, 2024 · 1 revision

For simplicity, this documentation will assume the use of bash, and assume that the dotfile, .bashrc is located in your $HOME directory. The instructions should be more or less the same regardless of the specific shell you use. If you use zsh (such as MacOS users) then replace .bashrc with .zshrc wherever .bashrc appears in the instructions below.

To download Athena, simply navigate to the directory of your choice and run this in your terminal:

curl -L https://github.com/AthenaFoundation/athena/releases/download/v1.4.2/athena-$(uname)-v1.4.2.zip > athena.zip && unzip athena.zip; mv athena-* athena

You can also download the latest Athena release manually from GitHub. Releases for Linux and MacOS are available. If you're running a Windows operating system, the recommended method for using Athena is to use WSL and install Athena within that Linux subsystem. There is, however, a build for Windows for Athena v1.4.1 for those who do not want to run WSL. Athena v1.4.1 is also the version that is guaranteed to be compatible with the material in the Athena textbook.

After downloading Athena, and assuming you are still in the parent directory of the athena folder, you should update your .bashrc:

echo "export PATH=$(pwd)/athena:$PATH" >> ~/.bashrc
echo "export PATH=$(pwd)/athena/util:$PATH" >> ~/.bashrc
echo "export ATHENA_HOME=$(pwd)/athena" >> ~/.bashrc

For these changes to take effect in your terminal, run source ~/.bashrc. Then, in your terminal, type athena and press enter. If everything worked, you should see Athena's REPL starting. To exit the REPL, type quit and press enter.

Apple Silicon Caveats

If you're using an Apple Silicon based machine, Athena will not work simply by following the above steps as there are a couple additional steps to take. If you're not sure whether you're on an Apple Silicon machine, you might be if you got the following error when you executed the athena command:

Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib

You can also check by writing uname -m in the terminal; if the output is arm64 then you're on Apple Silicon. Before proceeding with the below installation instructions, jump over to Additional Installation Steps for Apple Silicon. Once finished, you can resume following the instructions below.

Using athena-run

To run a specific Athena file, you can use the athena-run command as well. This will evaluate an Athena source file and then exit, rather than starting the REPL. To test that this is working:

echo "domain N" > example.ath && athena-run example

Note that when using athena-run, you do not include the .ath file extension in the filename passed as an argument to that command.

The final lines of output should read:

New domain N introduced.
>
Exiting Athena...

External Tools

If you're on Apple Silicon

For automated theorem provers, we suggest using an x86_64 build of Vampire. You will have to build from source and then move the resulting vampire binary to the $ATHENA_HOME directory.

To use Vampire in Athena, replace appearances of !prove with !vprove-from.

If you're not on Apple Silicon

Athena includes built-in methods to invoke external automated theorem provers (ATPs). If you want to use them, you at least need to have the SPASS prover. If you're on a unix-based operating system, or you're on Windows and you're using WSL, then the following should work:

sudo apt-get -y install spass; cp /usr/bin/SPASS $ATHENA_HOME

Verifying ATP Integrations are Working

You can verify it works by checking if the usage of the !prove method produces a theorem during evaluation. For convenience, you can simply copy and paste the below snippet into your terminal and run it.

echo 'module AutomatedProofExample {
      (print "-------Automated Proof Example----------")
      declare A,B,C,D: Boolean
      assume h1 := (A & B)
      assume h2 := (~C ==> ~B)
      (!prove C [h1 h2])
}' > new_test.ath && athena-run new_test && rm ./new_test.ath

If Athena's output includes the following, it means that Athena is invoking SPASS successfully:

Theorem: (if (and AutomatedProofExample.A AutomatedProofExample.B)
             (if (if (not AutomatedProofExample.C)
                     (not AutomatedProofExample.B))
                 AutomatedProofExample.C))

Module AutomatedProofExample defined.

If you're curious, you can delete SPASS from the $ATHENA_HOME directory and re-run the automated proof example, which should then fail with an error message similar to the following:

Error: Failed application of sprove-from:
Unable to derive the conclusion AutomatedProofExample.C from the given hypotheses.
Module AutomatedProofExample was not successfully defined.

Editor Support

An extension for the Athena language is provided for Visual Studio Code and can be downloaded from the marketplace or from within the VSCode editor. The extension provides syntax highlighting, contextual error messages, and preliminary support for go-to definitions (which can be enabled in the extensions settings after downloading).

Clone this wiki locally