Improve Agda installation UX

[xaviripo]

Agda is a complex project. For my thesis, I only strictly require the 2.5.3 version (the last version supported by the HoTT-Agda library). I'd like, though, to be able to switch between differents versions.

Unfortunately, Agda only officially supports installation through Cabal. Cabal installs packages globally, and although there is now experimental support for sandboxes, these are only compatible with certain versions of GHC, which some versions of Agda are not compatible with.

Ideally, I'd use Stackage, but Agda isn't there. Luckily, they do include stack-*.yaml files which can be used to build Agda with:

stack build --stack-yaml=stack-*.yaml

As it turns out, compiling big Haskell programs is very resource-consuming—this discussion contains useful information and links. This is a known issue when compiling Agda. Due to this, most of the times the compilation process doesn't finish. There is, though, a kind of solution that might or might not work: running Stack with -j1 (one concurrent job). This works because the compilation is very memory-consuming, and by default GHC tries to do multiple concurrent jobs which ends up eating all the RAM. Doing them one by one might still end up eating all the RAM, but there's a far better chance it won't. If you close everything, wait for about 10 minutes, and have 16GB of RAM, you have a big chance of it working.

This generates, in the .stack-work folder, the agda and agda-mode binaries necessary to run Agda from the terminal (good) and from emacs (better), respectively. To use emacs mode, one must further run agda-mode setup, which modifies the user's .emacs file.

So, to sum up, to switch from one Agda version to another, one must:

1. Clone the Agda repo.
2. Check out the appropriate version (e.g. git checkout v2.6.1).
3. Build Agda with stack build -j1 --stack-yaml=$(ls stack-*.yaml | tail -1). Running stack install instead may also do the next step for us, but I haven't tried yet.
4. Copy the generated binaries (agda, agda-mode) under .stack-work/dist/<YOUR ARCH>-<YOUR OS>/Cabal-<CABAL VERSION>/build/agda[-mode] to somewhere in our path (e.g. ~/.local/bin), or directly add this location to our path.
5. Run agda-mode setup in order to add Agda mode to our emacs configuration file.
6. Test Agda by opening an emacs file and loading it (C-c C-l).

The question is: can this process be automated? And, if so, how? The objective is to make installing Agda a task with:

• Minimal dependencies. Asking the user to have, for example, Python installed, is acceptable, but asking them to have Docker (like the current build system does) may not be.
• Minimal effort. The user should be able to install the desired version of Agda with one easy step.
• Minimal time and resource consumption. As we've seen, we can't do much about this one.

This issue aims to track the development of some kind of tool that can help not only those who wish to examine the code in my thesis, but also those who wish to enter the world of Agda smoothly, instead of hitting the ground with their face like I've been doing repeatedly for the last few months.

[xaviripo]

I just successfully installed Agda 2.5.3 with this method. Important notes:

• Due to this bug: Build-tools not detected when not using Stackage snapshot commercialhaskell/stack#595, which is, in theory, solved, the happy and alex build tools are not installed properly during stack build. To circumvent this, one can stack install happy and stack install alex, which installs them in .stack but adds them to the path. As they are build tools and not source code dependencies of Agda, I guess this is not a big deal.
• The oldest YAML file included is not compatible with the current stable version of Stack (2.1.3). One of the other two must be used.

Also, stack install does NOT install the built packages globally nor add them to the path. It just copies them to an install folder inside of .stack-work in the Agda repo.

[xaviripo]

Note on my last comment: apparently the install command DOES add the binaries to the path. Read here: https://docs.haskellstack.org/en/latest/GUIDE/#install-and-copy-bins. Unfortunately, it does state that Stack is not capable of providing the compilation process with a prefix (yet) and so the executables may depend on fixed data file locations. In particular, agda-mode depends on the emacs mode install scripts being in the generated folder inside of .stack-work, and in turn those depend on the agda executable being in there too. What this means is that we need the git repo we build these from to be permanently available afterwards. This doesn't make things any easier.