One Way of Installing the Agda Development Version

These notes grew out of my “cheat sheet” for installing the development version of Agda into a dedicated subdirectory of /usr/local/packages (on Linux systems), and continue to serve that purpose.

I have taken to install a dedicated version of GHC alongside any new Agda installations, to avoid package conflicts with other Haskell projects, and to have the correct GHC easily available for eventual MAlonzo compilation.

For general background on package management in GHC, see Albert Lai's useful piece:

Storage and Identification of Cabalized Packages

Warning: Don't follow these instructions if you don't understand them!

Setting up Shell Variables and Directories

I tend to do the whole process as root; on many systems, the easiest way to get a root shell is “sudo bash”.

V=Agda-2.4.3.3
P=/usr/local/packages/$V

For creating the installation directories (usually as root), make sure you have an appropriate umask:

umask
umask 022

mkdir -p $P/bin
mkdir $P/lib
mkdir $P/man
mkdir $P/man/man1
mkdir $P/src
mkdir $P/build
cd $P/build

Adapt to the GHC version you want to use, and to the place where you downloaded it to:

tar xjf /var/tmp/GHC/ghc-7.8.4-src.tar.bz2

Optional:

tar xjf /var/tmp/GHC/ghc-7.8.4-testsuite.tar.bz2

Prepare GHC installation:

cd ghc-7.8.4
cp mk/build.mk.sample mk/build.mk

Edit mk/build.mk to uncoment your choice of BuildFlavour, e.g:

BuildFlavour = perf

BuildFlavour = perf-llvm

If you choose LLVM (I have not yet succesfully done that), you may run into the following error message at build time:

You are using a new version of LLVM that hasn't been tested yet!

In that case, make distclean, and retract to a non-LLVM build, or possibly install an appropriate version of LLVM into $P.

For local Haskell documentation, you could add the following to the block corresponding to your chosen BuildFlavour:

HADDOCK_DOCS       = YES
BUILD_DOCBOOK_HTML = YES

Build GHC with your settings:

./configure --prefix=$P --help
./configure --prefix=$P
time make

This may take about 90 minutes.

If you unpacked the test suite:

time make test

This may take about 20 minutes.

make install

This may take about 1 minute.

If you don't make clean, you can come back here to make install again in case you mess up your GHC package database.

Preparing the Agda Installation

Now make sure the freshly installed GHC is in your PATH for the current shell (I use addtopath from bashutils-PATH):

addtopath $P
type ghc

For Agda, I keep the source separate from the build:

cd $P/src

For getting the Agda source:

Either unpack a stable version:

curl -o agda-2.4.2.2.tar.gz https://github.com/agda/agda/archive/2.4.2.2.tar.gz
tar xzf agda-2.4.2.2.tar.gz
mv agda-2.4.2.2 agda # for uniformity below
cd agda

Or download the Agda development version:

git clone https://github.com/agda/agda.git
cd agda

Or download the Agda maintenance version:

git clone https://github.com/agda/agda.git --branch maint-2.4.2 --single-branch
cd agda

Edit $P/src/agda/Agda.cabal:

(Not needed for stable versions) Make sure all Agda version numbers agree with your $V set at the beginning of this page.
Add -threaded to the options for linking calls to GHC.
(Curently, parallelisation within Agda is limited to the GHC runtime garbage collector, but still saves elapsed time on larger and more complex developments.)

version:         2.4.3.2

executable agda
   [...]
  build-depends:  Agda == 2.4.3.2,
   [...]
    ghc-options:  -rtsopts -threaded

Edit $P/src/agda/src/data/emacs-mode/agda2-mode.el:

(Not needed for stable versions) Make sure all Agda version numbers agree with your $V set at the beginning of this page.
If you are used to the Emacs-default “paste” behaviour of mouse-2, you may want to bind agda2-goto-definition-mouse to something else than just mouse-2. My wireless Logitech trackball has some otherwise unused mouse buttons; I also add some bindings for those.

(defvar agda2-version "2.4.3.2"
  
[...]

    (agda2-goto-definition-mouse [S-mouse-2])
    (agda2-goto-definition-mouse [mouse-9])
    (agda2-go-back               [mouse-8])

Set up a separate build directory for Agda:

cd $P/build
mkdir agda
cd agda
lndir ../../src/agda

(lndir originally was part of the X11 build system; it may now be available in its own package on your distribution.)

Wait until GHC is installed!

Make sure you are picking up the right GHC:

type ghc

If you do

ghc --make Setup
./Setup configure --prefix=$P -p -f uhc -f epic

now, it gives you a list of Haskell packages as missing dependencies.

For installation of the required Haskell packages, start in a separate terminal (tab), after setting $P as before:

mkdir $P/build/H
cd $P/build/H
addtopath $P

I use the ./Setup wrapper shell script hpack, and frequently re-use my previous package list:

packages-2.4.1.1 (2014-07-13)
packages-2.4.1.2 (2014-07-21)
packages-2.4.2.2 (2014-12-28)
packages-2.4.3.1 (2014-12-28)
packages-2.4.3.2 (2015-03-11)
packages-2.4.3.3 (2015-03-13) — with GHC-7.10RC2, this build needs a bump to base < 4.9in split.cabal and haskeline.cabal and template-haskell < 2.11 in geniplate.cabal
packages-2.4.3.4 (2015-03-28)
packages-2.4.3.6 (2015-03-31)

(Each package is installed by itself, so the list needs to be in bottom-up order.)

I am using a packages file like that via the following command:

time hpack $(grep -v '^#' packages-2.4.3.2)

This might take about 13 minutes.

If I hit a snag in the middle, for example when a bound in some .cabal file needs to be bumped, I restart processing from, e.g., line 16 of the packages file using the following command:

time hpack $(tail -n +16 packages-2.4.3.3 | grep -v '^#')

Do a sanity check on the resulting state of the GHC package collection:

ghc-pkg check

For the UHC backend, we need, according to the Install UHC Backend page:

    cd $P/src
    git clone https://github.com/UU-ComputerScience/uhc.git
    cd uhc
    git checkout 0dec07e9cb60e78bbca63fc101f8fec6e249269f
    cd $P/build
    mkdir uhc
    cd uhc
    lndir ../../src/uhc .
    cd EHC
    ./configure --prefix=$P

Carefully read the “Installation/build summary” this configure run produces, as it might point out problems that will make the build fail!

    time make
    time make install

Now you can actually build Agda — if you didn't get Epic installed, omit “-f epic”:

cd $P/build/agda/
ghc --make Setup
./Setup configure --prefix=$P -p -f uhc -f epic
time ./Setup build -v

This might take about 10 minutes.

./Setup install -v

For a profiling version agda_prof of the executable:

./Setup configure --prefix=$P -p -f uhc -f epic --enable-executable-profiling --program-suffix=_prof --disable-executable-stripping 
./Setup build -v
./Setup install -v

(Instructions for installing also a debugging version of the Agda executable are still missing.)

Installing the Agda Standard Library

Get the library source — the Agda source files need to be part of the final installation; for ease of installation we make the whole library build directory part of the installation.

For a stable version:

cd $P/src
wget https://github.com/agda/agda-stdlib/archive/v0.9.tar.gz
cd $P/lib
tar xzf ../src/v0.9.tar.gz
cd agda-stdlib-0.9

For the current development version:

cd $P/lib
git clone https://github.com/agda/agda-stdlib.git
cd agda-stdlib

For the current maintenance version:

cd $P/lib
git clone https://github.com/agda/agda-stdlib.git --branch 2.4.2.3 --single-branch
cd agda-stdlib

For the current development version with UHC support:

  cd $P/lib
  git clone https://github.com/phile314/agda-stdlib
  cd agda-stdlib
  git checkout uhc-support

Install a script for locating the standard library:

echo "echo $(pwd)/src" > $P/bin/agdalib
chmod 755 $P/bin/agdalib
agdalib

Install the Haskell components of the standard library:

cd ffi
ghc --make Setup
./Setup configure --prefix=$P -p

If this fails, it may be sufficient to bump some upper bounds in the .cabal file.

./Setup build -v
./Setup install -v

Install the Haskell utilities used by the standard library installation:

cd ..
ghc --make Setup
./Setup configure --prefix=$P -p
./Setup build -v
./Setup install -v

Typecheck the Agda components:

$P/bin/GenerateEverything
ls -latr
type agda
time agda +RTS -S -N1 -H2G -M2G -RTS -i src -i . Everything.agda

(Omit -N1 if you omitted -threaded, or adapt it according to your number of cores. Parallelising the garbage collection on four cores during type-checking the standard library saves about 5 seconds of elapsed time (except with GHC-7.8.4, where it produces a significant slow-down)).

This may take around 4 minutes.

Now you can call Agda with, e.g.:

agda +RTS -S -N4 -K64M -H4G -M4G -RTS -i . -i $(agdalib) MyModule.lagda

Don't forget to update your Emacs settings:

M-x customize-group RET agda2

You will need to update at least the Agda2 Include Dirs setting to include the output of agdalib.

My Agda2 Program Args on a 16G 8-core machine (these need to be individual arguments!):

+RTS
-N1
-K256M
-H5G
-M10G
-RTS

Don't use these unless you know what they are doing!

Restart your Emacs with your PATH including $P/bin so that it picks up the matching agda-mode.

I also have some useful shell functions for bash in bashutils-Agda.

Wolfram Kahl