Introduction

[TOC]

Support
License
Tests

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

• pure type system (PTS)
• higher-order functions
• dependent types

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.

Building

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

git clone --recurse-submodules git@github.com:AnyDSL/thorin2.git

Otherwise, clone via HTTPS:

git clone --recurse-submodules https://github.com/AnyDSL/thorin2.git

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.

Install

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).

Dependencies

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.