[TOC]
Support |
|
License |
|
Tests |
|
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 [email protected]: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
.
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
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: