This is a (work in progress) backend to generate native executables from Idris code, using the LLVM compiler infrastructure. Code is generated via LLVM IR.
The source folder rts/
contains a primitive runtime system with a relocating
semi-space garbage collector.
LLVM 11 needs to be installed and the binaries available in your $PATH
. To
check if that is the case, try the following command:
$ opt --version
LLVM (http://llvm.org/):
LLVM version 11.1.0
Optimized build.
Default target: x86_64-pc-linux-gnu
Host CPU: znver2
GMP needs to be installed (libgmp-dev
on Debian).
You need CMake (>= 3.18) and Ninja, building with make
is not supported.
Make sure you have checked out the Git submodule as well:
git submodule update --init --recursive
Prepare the submodule:
make -C external/llvm-statepoint-utils dist/llvm-statepoint-tablegen.h unified
Compile:
cmake -G Ninja .
ninja
Run tests:
ninja test
The "support files" (precompiled platform code and runtime system, as well as a
custom LLVM pass) need to be available in a directory in the $IDRIS2_DATA
path. You can achieve that by running (from within the source dir):
export IDRIS2_DATA=$PWD/support
(most useful during development) or by running make install
.
# compile the included "Hello world" example
./build/exec/rapidc --cg llvm -o hello samples/Hello.idr
# run the compiled binary
./build/exec/hello
Differences from mainline Idris 2:
Int
is 63-bits only and overflow is handled differently
Currently not implemented:
- FFI (the FFI functions from prelude and base are hardcoded & handwritten specifically for the RTS)
- Concurrency
- Network primitives are stubbed and not functional
- Some support functions are completely missing