How to Install Athena

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.

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:$PATH" >> ~/.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.

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

The final lines of output should read:

New domain N introduced.
>
Exiting Athena...

External Tools

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

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).

Back to top