Thorin 1.9.0
The Higher ORder INtermediate representation
No Matches

Support Documentation Discord
License License
Tests Linux Windows MacOS Doxygen

Thorin is an extensible compiler intermediate representation that is based upon the Calculus of Constructions (CoC). This means:

In contrast to other CoC-based program representations such as Coq or Lean, Thorin is not a theorem prover but focuses on generating efficient code. For this reason, Thorin explicitly features mutable state and models imperative control flow with continuation-passing style (CPS).

You can use Thorin either via it's C++-API or the command-line utility.


If you have a GitHub account setup with SSH, just do this:

git clone --recurse-submodules

Otherwise, clone via HTTPS:

git clone --recurse-submodules

Then, build with:

cd thorin2
cmake -S . -B build -DCMAKE_BUILD_TYPE=Debug
cmake --build build -j $(nproc)

For a Release build simply use -DCMAKE_BUILD_TYPE=Release.


If you want to install Thorin, specify an install prefix and build the target install:

cmake -S . -B build -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=/my/local/install/prefix
cmake --build build -j $(nproc) -t install

Build Switches

CMake Switch Options Default Comment
CMAKE_BUILD_TYPE Debug | Release | RelWithDebInfo Debug Build type.
CMAKE_INSTALL_PREFIX /usr/local Install prefix.
THORIN_BUILD_DOCS ON | OFF OFF If ON, build the documentation
(requires Doxygen).
THORIN_BUILD_EXAMPLES ON | OFF OFF If ON, build the examples.
THORIN_ENABLE_CHECKS ON | OFF ON If ON, enables expensive runtime checks
(requires CMAKE_BUILD_TYPE=Debug).
BUILD_TESTING ON | OFF OFF If ON, build all unit and lit tests.
THORIN_LIT_TIMEOUT <timeout_in_sec> 10 Timeout for lit tests.
(requires BUILD_TESTING=ON).
THORIN_LIT_WITH_VALGRIND ON | OFF OFF If ON, the Thorin CLI in the lit tests will be run under valgrind.
(requires BUILD_TESTING=ON).


In addition to the provided submodules:

  • Recent version of CMake
  • A C++20-compatible C++ compiler.
  • While Thorin emits LLVM, it does not link against LLVM.

    Simply toss the emitted *.ll file to your system's LLVM toolchain. But technically, you don't need LLVM.