Commands

The commands are Leiningen aliases for rainbow.main, defined in project.clj. Run them from the repository root. Each exits with 0 when everything it checked passed and 1 otherwise, and prints a usage line when called without the arguments it needs.

lein verify

lein verify <namespace> ...

Replays the base checkpoint, installs each module through its extend-environment, re-checks each theorem the module names and prints its axioms.

checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed
OK    rainbow.math.finite.rational-argmax (15 theorems: 13 for all inputs, 0 definitional unfoldings, 2 worked instances)
       checked   instance  bool/false-not-true  axiom-free

The theorems come from theorem-ids, or definition-ids when there are none. A module with neither, such as one that installs tactics, is reported as (installed; declares no theorems of its own), and the install is the check. A namespace without extend-environment fails. So does a checkpoint that does not replay, a module that does not install, or a theorem that is not checked. Check your first proof explains the columns.

—checkpoint

lein verify --checkpoint artifacts/<dir>/checkpoint.edn.gz <namespace> ...

Uses another checkpoint as the base. The default is artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz.

—bundle

lein verify --bundle [--reductions N] <bundle-file> ...

Checks proof bundles, in plain EDN, shared EDN or binary, with the kernel alone. For each file it prints OK or FAIL, the path and the time taken, then a line per claim with status, alias and axioms. A failing claim says whether it resolves to a different id, does not check, or has recorded axioms that differ from the kernel’s. All named bundles are checked, even after one fails.

--reductions N raises the reduction budget. The check uses the largest of the kernel default (1,000,000 steps), N and the budget recorded in the bundle. A failure from an exhausted budget says so and suggests a larger value. A larger budget lets the check run longer and cannot make a false proof pass.

lein reproduce

lein reproduce <milestone-namespace> ...
lein reproduce --all

Runs a milestone, the driver that added a result to the corpus, on its recorded input checkpoint and compares the rebuilt checkpoint’s content id with the recorded one. It writes nothing.

lein reproduce rainbow.milestones.ahof-bisection

Each milestone prints SAME with the recorded id, or DIFF with both. A namespace without run, default-input-checkpoint-path or checkpoint-path prints FAIL. The last line counts the matches. --all finds each reproducible milestone under src/rainbow/milestones by reading the source tree.

lein share-bundle

lein share-bundle in.edn out.edn
lein share-bundle --binary in.edn out.bin
lein share-bundle --plain in.edn out.edn

Converts a bundle between encodings: shared EDN by default, --binary for the compact binary format, --plain for every term as a tree. The input can be any of the three, the ids stay the same, and the command prints both file sizes in bytes.

lein show

lein show <alias> [module-namespace ...]

Prints a declaration’s statement for people to read. Name the module that installs the alias unless the default checkpoint has it.

lein show decision/finite-nnrat-argmax-dominates rainbow.math.finite.rational-argmax

The optimality certificate from rainbow.math.rational.signed.lp-duality-on prints as:

optimization/signed-lp-optimality-certificate-on.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (primal-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · x j ≤ b i)
  (dual-feasible : ∀ j ∈ cols, c j ≤ Σ i∈rows, M i j · y i)
  (x-nonnegative : ∀ i ∈ cols, 0 ≤ x i)
  (y-nonnegative : ∀ i ∈ rows, 0 ≤ y i)
  (gap : Σ i∈rows, b i · y i = Σ j∈cols, c j · x j)
  (candidate : B → ℚ)
  (candidate-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · candidate j ≤ b i)
  (candidate-nonnegative : ∀ i ∈ cols, 0 ≤ candidate i)
  → Σ j∈cols, c j · candidate j ≤ Σ j∈cols, c j · x j

Here = is signed/equivalent, equality of rational values. The printout is a view of the term the kernel checks, which has de Bruijn indices and content ids. Check your first proof explains how to read it.

lein test

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

Runs the suite, which takes hours, or the namespaces you name. To run it in chunks, see Install.

Other aliases

project.clj also has aliases that run single milestone drivers, such as bellman or ahof-o12, which built the corpus. To check a milestone’s result, use lein reproduce.