[Agda] Agda on raspberry pi 4

Martin Escardo m.escardo at cs.bham.ac.uk
Mon Nov 30 20:41:35 CET 2020


Just for fun.

I managed to install Agda in the raspberry pi 4 (with 4gb of ram).

$ time cabal install Agda
Resolving dependencies...
Build profile: -w ghc-8.8.3 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.1.2 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     Agda-2.6.1.2 (all, legacy fallback)
Building     Agda-2.6.1.2 (all, legacy fallback)
Installing   Agda-2.6.1.2 (all, legacy fallback)
Completed    Agda-2.6.1.2 (all, legacy fallback)
Symlinking 'agda'
Symlinking 'agda-mode'

real	1944m55.766s (this is 1.35 days)
user	381m14.921s  (6.35 hours)
sys	247m33.846s  (4.11 hours)

The above is just the Agda phase of the cabal install. The first cabal
install did everything but failed in the above step for lack of enough
ram and swap (it had 1gb of swap), and it took a couple of days before
failing. But it compiled everything else successfully. I added 26gb of
swap to be able to succeed as above. Moreover, I booted from an ssd
rather than from an sd card.

This is running in Ubuntu 20.10, official release for the raspberry pi
(64 bit). I didn't succeed with previous versions of ubuntu or with
other debian based linux distributions.

If anybody wants the .cabal tree to avoid the recompilation, I can
provide it. Its size is 1.8gb.

I type-checked my repository TypeTopology. It took 29min, and half of
the total amount of ram was used (so no swap). For comparison, this
takes 10 minutes in a core i3, 5 minutes in a core i5, and 3.5 minutes
in a core i7.

Martin



More information about the Agda mailing list