UP | HOME

Compiling Idris programs on ARM

1 Preface

ARM is currently a "tier 2" GHC platform, and apparently it's tricky to make it work; and even if it would, it might be better to compile on a desktop, rather than on RPi.

There's also somewhat similar situation with low-memory swapless OpenVZ VPS: even cabal update requires too much memory.

The obvious solution is to compile Idris into C on a desktop, and then compile the resulting program on RPi/VPS.

This is tested on Idris version 0.9.17.1-git:dcdfd85, with raspbian on RPi 2. The date is [2015-05-16 Sat].

2 Installing dependencies

There's nothing uncommon, so everything should be in system repositories, if not installed already.

3 Compiling the C runtime system

Goes like this:

  1. mkdir idris on a target machine
  2. scp -r Idris-dev/rts/ raspberry@pi:idris
  3. scp Idris-dev/config.mk raspberry@pi:idris
  4. For ARM, edit config.mk on a target machine: remove -msse2 (upd, 2015-05-22: not required anymore, it's not present in newer versions)
  5. cd idris/rts && make
  6. Optionally, TARGET=~/local/ make install (otherwise the rts directory could be used)

4 Compiling an Idris program

  1. Compile it into C on a desktop: idris -S test.idr -o test.c
  2. scp test.c raspberry@pi:idris
  3. gcc -O2 -DHAS_PTHREAD -DIDRIS_ENABLE_STATS -g -fwrapv -lpthread -Irts test.c rts/libidris_rts.a rts/idris_main.c rts/idris_opts.c rts/idris_stats.c -o test

Now, ./test should work.

It would lead to segmentation fault without -DIDRIS_ENABLE_STATS, and not sure why it requires idris_opts.c and idris_stats.c: they are in libidris_rts.a already, but getting those undefined reference errors if not including them. In idris_main.c, heap and stack sizes could be tweaked.