search

xaviripo / bachelor-thesis

Bachelor's Thesis (Mathematics / Computer Science and Software Engineering @ University of Barcelona). See Releases for final version.
0 stars 0 forks source link

Improve Agda installation UX #3

Open xaviripo opened 4 years ago

xaviripo commented 4 years ago

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:

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 commented 4 years ago

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

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 commented 4 years ago

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.