Main /
\ Main

MacOSX

To compile and install Agda you must have Xcode Developer Tools, which may have come with your Mac OS X installation CD or can be downloaded from Apple Developer Connection. You need to install only Developer Tools Essentials and UNIX Development Support, and may skip other optional components.

The following should work for a fresh install.

The idea is that you first install the Haskell Platform and then use cabal to install Agda. Then you install Aquamacs and finally the Agda standard library:

  • Install the Haskell Platform
  • Download the latest package list by typing cabal update in a Terminal window.
  • Update your PATH variable (according to the instructions of cabal) in your .bash_profile - file: 
           export PATH=$HOME/Library/Haskell/bin:$PATH
or (depending on your cabal version) 
           export PATH=$HOME/.cabal/bin:$PATH
  • Install happy, alex, and cpphs by calling cabal install happy alex cpphs
    • This page may help if you have trouble here (2018-07-05).
  • Install Agda by calling cabal install Agda . Now you can go and have a cup of coffee (or two).
  • Install Aquamacs
  • Install agda-mode in Aquamacs by typing (in a terminal window): 
          agda-mode setup

Now you can use Agda! Enjoy!

Other methods and trouble shooting

Note (2012-11-13): the following instructions are a bit outdated.

Agda needs GHC to compile. The installation process can be much simplified with the help of Cabal Install.

Stable version of Agda is now available from Hackage (see Agda and, for Agda<=2.3.0.1, Agda-executable). Since Agda is still under active development, it is also a good idea to keep ourselves updated with the latest Agda source using darcs.

You may install these tools either from binary package, or through MacPorts (recommended).

NOTE: some success was obtained (by Messrs Hancock and McBride) by following an opposite path. Instead of relying on MacPorts,

If I am not mistaken, the hackage release of Agda works OK in a ghc 6.12.1 / emacs 22.3.1 environment.

Install using MacPorts

It is recommended (by some) to install these tools through MacPorts, a convenient package management system for open-source software on OS X. Note that if you install Cabal and darcs using MacPorts, you must have installed GHC using MacPorts as well.

  1. Install MacPorts.
    • If you have not installed MacPorts yet, read the download and installation instructions. You may simply download the binary distribution with a Mac-style installer.
    • By default, MacPorts installs its files under the directory /opt/. The installation script takes care of modifying your .profile and add /opt/local/bin to your PATH environment variable.
    • After installation, open Terminal and run sudo port -v selfupdate to keep the database up to date.
  2. Install GHC, if you have not done so:
    • sudo port install ghc.
    • GHC and the packages it depends on may take some time to compile.
  3. Install Cabal:
    • sudo port install hs-cabal
    • sudo cabal update
    • Cabal installs its executables under ~/.cabal/bin. Add it to your PATH varible, for example, by adding a line export PATH=~/.cabal/bin:$PATH to your .profile if you use BASH.
  4. Install darcs, if you want to be in sync with the latest Agda source:
    • sudo port install darcs

Troubleshooting

It may happen, after upgrading GHC, that when you try to upgrade Cabal using either sudo port upgrade hs-cabal or sudo port install hs-cabal, you get the following error message: 

Error: Target org.macports.configure returned: shell command "cd /opt/local/..." returned error 1
Command output: Configuring cabal-install-0.6.2...
Setup: At least the following dependencies are missing:
zlib >=0.4 && <0.6

It might have happened because GHC was upgraded without rebuilding the libraries. It worked for me if I simply sudo port uninstall them all (hs-cabal, hs-HTTP, hs-zib) and install them again.

Install Some of the Tools from Binary

There are some binary distributions of GHC and darcs. However, you still have to compile Cabal from source. You will need both the Cabal library and Cabal-install, and for the latter you will need the HTTP and zlib packages. It is not necessary easier than compiling everything using MacPorts.

Installing Agda

Installing Agda is much easier with Cabal.

  1. To compile Agda, you will need Happy and Alex:
    • sudo cabal install happy
    • sudo cabal install alex
  2. Now you may either:
    1. install from Hackage, for a stable release:
      • sudo cabal install Agda-executable
    2. install from the darcs repository, for the latest source:
      1. Go to the directory where you would like to keep the Agda source, and run:
        • darcs get --partial http://code.haskell.org/Agda
      2. Compile Agda. cd to the directory Agda, and run:
        • sudo cabal install
      3. Compile the Agda executable.
        • cd src/main
        • sudo cabal install
  3. If the previous step succeeds, Agda should have registered itself as a GHC library, and two executables, agda and agda-mode should have been built in ~/.cabal/bin. (Note that agda-mode does not come with Agda 2.2.0, you need a more recent release if you want to use this program.) Run:
    • agda-mode setup
    • It modifies your .emacs file, adding whatever it needs to locate and run the Agda Emacs mode.

Now when you create or open a .agda file in Emacs, it should trigger Agda mode.

Agda is known to work with at least Aquamacs and Carbon Emacs. The latest binaries of them can be downloaded from their websites. After downloading, simply copy the application bundle to any location you like. Usually your /Applications directory.

Edit | History | Recent Changes (all) | Search
Page last modified on July 15, 2018, at 11:56 pm
Powered by PmWiki