LLVM codegen and native runtime for Idris 2

Rapid is a backend to generate native executables from Idris code, machine code is generated via LLVM IR. Rapid is still in active development, but can already compile itself successfully and reproducibly.

Full Power of Idris

Rapid embeds Idris 2 as library, and thus supports all Idris 2 language features. Existing code can be recompiled without any modifications.

Standalone binaries

Binaries created by Rapid are self-contained and can run without a language-specific runtime environment.

Rapid is Open Source

Rapid source code is available as Open Source under the terms of the 3-clause BSD license (same license as Idris2 itself).

Getting started

To get started using Rapid, please check out the README.md file in the source code repo. To learn more about the internal implementation details, please take a look at the developer documentation.

Documentation

Check out the developer documentation to learn more about Rapid’s internals. An introduction into the CPS-based intermediate representation is given by this presentation:

A CPS-based IR for the LLVM Backend, Idris Developers’ Meeting, May 2022