Skip to content

Latest commit

 

History

History
84 lines (63 loc) · 2.2 KB

agda-installation.md

File metadata and controls

84 lines (63 loc) · 2.2 KB
layout permalink title
page
/agda-installation/
Agda Installation

Installation instructions for Linux

Install the latest versions of cabal-install and of emacs via your package manager, then open a terminal and run the commands

cabal update
cabal install alex happy Agda
agda-mode setup

Note that even if your Linux distribution has an agda package available it might not be recent enough, so you should use the instructions above (in particular Debian, Ubuntu, and Fedora all seem to have outdated versions of Agda in their repositories).

Installation instructions for Mac OS X

Homebrew provides prebuilt packages for OS X. Install Homebrew and then run

brew install agda
agda-mode setup

Hopefully this should be all that is needed.

Installation instructions for Windows

Download emacs from [http://ftpmirror.gnu.org/emacs/windows/emacs-26/emacs-26.2-x86_64.zip] and unzip it somewhere (preserving the directory structure). You can now run emacs with the bin\runemacs.exe executable. Feel free to create a desktop shortcut to it.

Download and install the Haskell Platform from [https://www.haskell.org/platform/windows].

Open the Windows command prompt and run the following two commands. The second command will take a rather long time as it will compile Agda from scratch together will all of its dependencies.

cabal update
cabal install Agda

Create a file called .emacs (with the leading period) in the directory C:\Users\##yourusername##\AppData\Roaming containing the following two lines

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

Testing

You can test your installation as follows.

Open Emacs and create a new file (File > Visit New File…) that you name test.agda. You should see (Agda) on the bottom of the window.

Type the text below in the file (type! do not copy-paste!).

postulate \bN : Set

As you type, the \bN should automatically change to a blackboard bold N. If it turns to a box or to something weird, there is something wrong with your fonts. Type Ctrl-C followed by Ctrl-L, it should now show (Agda:Checked) at the bottom of the buffer.