~cypheon/rapid

LLVM Backend and Native Runtime for Idris2
61aec3ca — Johann Rudloff 4 months ago
Turn Data Constructors with constant members into constants
9928b2ee — Johann Rudloff 4 months ago
[refactor] Codegen: use simpler state modification methods
2e88d589 — Johann Rudloff 4 months ago
Ensure static closure objects are properly aligned

refs

main
browse  log 

clone

read-only
https://git.sr.ht/~cypheon/rapid
read/write
git@git.sr.ht:~cypheon/rapid

You can also use your local clone with git send-email.

builds.sr.ht status builds.sr.ht status

#LLVM codegen and native runtime for Idris 2

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.

#Prerequisites

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

#Compilation

Prepare the submodule:

make -C external/llvm-statepoint-utils dist/llvm-statepoint-tablegen.h unified

Compile:

cmake -G Ninja .
ninja

Run tests:

ninja test

#Usage

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

#Limitations

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