Commands

The commands are Leiningen aliases defined in project.clj: most run rainbow.main, and explore and lp-view run rainbow.view and rainbow.view.lp. Run them from the repository root. Each exits with 0 when everything it checked passed, 1 on a failed check and 2 on a usage error, which it explains with a usage line. A missing argument is a usage error, and so is an unknown option for verify, reproduce, show and lp-view (CHANGELOG).

lein verify

lein verify <namespace> ...

Replays the base checkpoint and prints its environment id and names id, 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: environment sha256:a41ba35a9f845aa04600620234dd1ccbb86969b09ffb14a44847da82ba4a5d5c names sha256:04959786090003bdfd133d7f4da521566de7ede77813ee1fa8aa3185284d193a
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. A checkpoint that cannot be loaded or replayed is reported with the reason:

FAIL checkpoint /tmp/no-such.edn.gz could not be loaded/replayed: :day54/checkpoint-read-failed -- /tmp/no-such.edn.gz (No such file or directory). Check that the checkpoint path exists and the file is readable and complete.

—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 bundle whose base names differ from its recorded names id is refused; one made before 1.4.4 records none and gets a names not pinned line. 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 that is not a reproducible milestone prints FAIL. A milestone whose input file is missing prints NEEDS and is not rebuilt. On a fresh clone that is finite-nat, nat-distance, nat-distance-core and nat-metric-separation, which also take the Mathlib v4.30.0 catalog that scripts/export-mathlib-catalog.sh makes. The last line counts the matches. The exit code is 1 on any DIFF or FAIL; NEEDS does not fail the command. --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. A missing or truncated input prints FAIL share-bundle ... with what to check, and exits with 1. An output path that is the input, also through a link, is refused instead of written over (CHANGELOG).

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.

A module that cannot be loaded prints FAIL show ... with the reason, and the command exits with 1.

lein explore

lein explore <checkpoint.edn.gz | bundle.edn> [out-dir] [--roots a,b] [--modules ns,...] [--offline]

Writes the Proof Explorer, a static page (index.html with data.json) of the dependency graph, proof trees, axiom closures and kernel-computed example values for natural-number and non-negative-rational equations (CHANGELOG). The data is inline, so the page opens from disk; --offline also inlines the graph libraries. --roots picks the theorems to start from. A bundle is replayed as lein verify --bundle does before anything is drawn. A missing file or bad input prints one FAIL explore ... line saying what to check, and the command exits with 1 (CHANGELOG). See Explore a proof.

lein lp-view

lein lp-view <instance.edn> <certificate.edn> [out-dir]

Runs the LP optimality certificate checker (rainbow.or.lp-certificate/certify) and writes the LP Certificate Viewer, a static page with its data inline. The verdict is the kernel’s check of one instance of optimization/signed-lp-optimality-certificate-on; the page also shows every comparison that proof is built from, each confirmed by its own kernel check, so a refused certificate names the comparison that failed (CHANGELOG). It exits with 0 when the certificate is certified and 1 when it is rejected. For a missing or unreadable file, data that is not an instance or certificate, or data of the wrong shape, it prints one FAIL lp-view ... line saying what to check, writes nothing and exits with 1 (CHANGELOG). --checkpoint without a path is a usage error. See Check an LP certificate.

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.