Skip to content
Rainbow docs menu

Getting started

Install

You need a JDK (CI uses Temurin JDK 21), Leiningen and git. Leiningen fetches the one dependency, Clojure 1.12.2, on the first run. Run every command from the repository root.

Get the repository

git clone https://github.com/Flexiana/rainbow && cd rainbow
git checkout v1.4.1

The clone includes artifacts/ with the recorded checkpoints, their reports and the declaration store (artifacts/store/declarations.edn.gz). Commands read checkpoints from there, so there is nothing to build.

Check that it works

lein verify rainbow.math.finite.rational-argmax

The first line should say the default checkpoint replayed, and the next should start with OK. Check your first proof explains the output.

CI runs the same command on three modules and checks that the four kernel files are still 1,364 lines:

lein verify rainbow.math.rational.nnrat.identities rainbow.math.finite.rational-argmax rainbow.math.finite.markov-ergodic-uniqueness
cat src/rainbow/kernel.clj src/rainbow/term.clj src/rainbow/environment.clj src/rainbow/canonical.clj | wc -l

Running the tests

lein test runs the whole suite, about 2,000 tests and 44,000 assertions. Many tests replay large checkpoints, so it takes hours. Run one namespace instead:

lein test rainbow.math.rational.nnrat.ring-test

If the suite does not fit in one JVM, scripts/run-suite-chunked.sh runs it in fresh JVMs, a fixed number of namespaces at a time, and writes a summary line per chunk:

scripts/run-suite-chunked.sh 40

A chunk that dies without writing its line is reported as terminated, apart from test failures. Set RAINBOW_START_CHUNK to resume from a given chunk. The script’s failure controls have their own test, which needs no JVM:

python3 scripts/test-suite-runner.py