← Command reference · lean-pkg receipt · CLI overview
lean-pkg receipt comparator
run the comparator on a Lake project and write the comparator receipt (the comparator-receipt program: the same code and flags).
Also run as the program comparator-receipt: the same code and flags.
Usage
lean-pkg receipt comparator [--project PROJECT] [--check CHECK]
[--mechanism {auto,toolchain,legacy}] [--verify VERIFY]
[--evidence-dir DIR] [--prepare] [--from-prepared DIR]
[--no-resume] [--judges N] [--unit-size K] [--slots SPEC]
[--estimate] [--sample K] [--force-sample]
[--verify-oleans [DIR]] [--attempts [DIR]]
[--seal-sacct RECEIPT] [--sacct-file F] [--user NAME]
[--json] [--host-label LABEL] [--json]
Run comparator-check.sh and write a comparator receipt. The same code and flags as the comparator-receipt program, which stays.
Arguments and flags
| Argument or flag | Description |
|---|---|
--project PROJECT |
Lake project directory (default: cwd). Default: .. |
--check CHECK |
comparator-check.sh to run (env COMPARATOR_CHECK; default: the copy shipped with lean-pkg) |
--mechanism {auto,toolchain,legacy} |
toolchain: lake comparator with the toolchain’s bundled kernels (Lean v4.35.0-rc2+, what Palomar runs); legacy: the pinned comparator/lean4export/nanoda/landrun stack; auto (default): toolchain when available, else legacy. Choices: auto, toolchain, legacy. |
--verify VERIFY |
verify-comparator.sh for the toolchain mechanism (env COMPARATOR_VERIFY; default: the vendored PalomarTemplate copy) |
--evidence-dir DIR |
where the stage logs and stages.json go, kept on failure (default: <project>/.lake/comparator-receipt; its comparator-stages/ subdirectory); outside the project its path is written as <evidence> in every log and receipt |
--prepare |
run only the setup stages (dependency checkout, Mathlib cache, build of the configured modules); idempotent; a later run at the same commit, toolchain and config hash skips them and runs only the comparison |
--from-prepared DIR |
reuse the completed setup recorded in DIR (an evidence directory or its stages.json); refuses when it was prepared for another commit/toolchain/config |
--no-resume |
judge every slot again, ignoring the slots this commit and config hash already accepted (cached under <evidence-dir>/comparator-stages/04-slots/) |
--judges N |
run up to N judge processes at once, each on a contiguous shard of every configuration’s theorem_names (toolchain mechanism; env LEAN_PKG_COMPARATOR_JOBS; default 1); with –unit-size, N is only how many units run at once. The merged verdict is exact; see docs/comparator.md (Runtime) for when it helps |
--unit-size K |
judge each configuration in contiguous units of at most K names (toolchain mechanism; env LEAN_PKG_COMPARATOR_UNIT_SIZE; default: the whole configuration, cut into –judges shards). –unit-size 1 –judges 1 judges each name alone, one at a time, so a capped run resumes per name |
--slots SPEC |
judge only these slots (theorem_names entries): comma-separated names, <config>:<name>, 1-based indices or ranges i-j over all configurations, or sample:K (a namespace-stratified sample). Writes a PARTIAL receipt into the stage directory, marked partial: true: diagnostic only, refused as evidence |
--estimate |
after setup, judge a sample of slots (the heaviest by olean size, then namespace-stratified) one at a time and print an estimate {per_slot_seconds, slots, estimated_seconds, recommended_cap, remaining_estimate_seconds}; writes no receipt (the judged slots are cached for the real run). The JSON is schema comparator-estimate/2; /1 -> /2 added the sample floor, the heaviest-first sample (per-row weight_bytes, weight_module, heavy) and the max cap model; later additions (weights_found, remaining_estimate_seconds, …) are additive and keep /2. See docs/comparator.md (Estimate first) |
--sample K |
–estimate: sample size (default and floor: max(5, ceil(0.25 * slots)), capped at the slots); –slots overrides the sample |
--force-sample |
–estimate: accept a –sample (or –slots) below the floor; the estimate warns and records sample_forced: true |
--verify-oleans [DIR] |
read-only, no host policy: rehash the package’s compiled modules under .lake/build/lib and compare them with the olean manifest the setup recorded in DIR (an evidence directory, its comparator-stages/ or its stages.json; default: the evidence directory); the recorded commit must be HEAD; exit 0 same, 1 different or nothing recorded; writes nothing |
--attempts [DIR] |
read-only, no host policy: list the earlier runs kept under comparator-stages/attempts/NNN/ (verdict, failed stage, commit, times, files, whether every kept file still matches its recorded sha256) in DIR (an evidence directory, its comparator-stages/ or its attempts/; default: the evidence directory); exit 0, or 1 when a kept file changed or went missing; writes nothing |
--seal-sacct RECEIPT |
after the Slurm job finished, no host policy: corroborate RECEIPT’s Slurm claim (job_id from SLURM_JOB_ID, which any shell can set) with the job’s sacct record: COMPLETED, exit 0:0, Start..End containing the run, this account (live sacct, or –user) and the receipt’s node (its h- host label against the node’s); writes <c12>-comparator-sacct.txt beside RECEIPT (the record, normalized; no user or node names) and its sha256 into RECEIPT as slurm_sacct. Only a sealed receipt backs a coverage.yaml compute job. Exit 0 sealed (or already), 1 refused, nothing written |
--sacct-file F |
–seal-sacct on a host without Slurm: the saved output of SLURM_TIME_FORMAT=%Y-%m-%dT%H:%M:%S%z sacct -j J --format=JobID,State,ExitCode,Start,End,Elapsed,User,NodeList -P (with its header line); the account is then checked only with –user |
--user NAME |
–seal-sacct: the account the job must have run under (default with live sacct: this one); compared, never written |
--json |
–estimate, –verify-oleans, –attempts or –seal-sacct: print JSON; stdout is the JSON document alone, the progress goes to stderr |
--host-label LABEL |
name the host LABEL in the receipt (host, host_label, job_id, host_policy) and the output (env COMPARATOR_RECEIPT_HOST_LABEL); default: h- and 12 hex digits of the SHA-256 of the lower-cased host name, the label receipt systemd uses; the host name itself is never written |
Details
lean-pkg receipt comparator [--project DIR] [--check SCRIPT] [--mechanism M] [--evidence-dir DIR] [--prepare | --from-prepared DIR] is the separate console
script that produces comparator receipts; see
The comparator tier. COMPARATOR_RECEIPT_STACK=unlimited|<kB>
raises the soft stack limit of its lake/lean children (never above the hard
limit; recorded as the receipt’s stack_limit); it warns when the soft limit is
8 MiB or less; see Stack limit.
COMPARATOR_RECEIPT_BUILD_SOURCE=TEXT declares where the package’s oleans were
built (a job id or host label; redacted); the receipt’s build_provenance records
whether the build stage compiled anything or found the oleans prebuilt; see
Build provenance.
The setup also records an olean manifest (the package’s own compiled modules,
hashed into comparator-stages/03-build.oleans.sha256; receipt
olean_manifest); a reused setup whose oleans changed is refused, and the
comparator stage fails when they change during the comparison.
lean-pkg receipt comparator --verify-oleans [DIR] [--json] is the read-only check
(exit 0 same, 1 different or not recorded); see
Olean manifest.
A run that replaces an earlier run’s stage files first keeps them, read-only,
as comparator-stages/attempts/NNN/ with an attempt.json (numbers never
reused; lean-pkg never deletes or reads them back);
lean-pkg receipt comparator --attempts [DIR] [--json] lists them; see
Attempts.
lean-pkg receipt comparator --seal-sacct RECEIPT [--sacct-file F] [--user NAME] [--json]
(no host policy, after the Slurm job finished) corroborates the receipt’s Slurm
claim with the job’s sacct record and seals it (slurm_sacct, and
<commit12>-comparator-sacct.txt beside the receipt); only a sealed claim backs a
coverage.yaml compute job; see
Seal the Slurm claim with sacct.
COMPARATOR_RECEIPT_LEAN_THREADS=N sets LEAN_NUM_THREADS=N for those children
(N = 1 serializes the build on a memory-tight host; recorded as the receipt’s
lean_threads; any other value exits 2); see
Serial builds.
--judges N (env LEAN_PKG_COMPARATOR_JOBS) runs up to N judges at once;
--unit-size K (env LEAN_PKG_COMPARATOR_UNIT_SIZE) cuts each configuration
into units of at most K names, making --judges only the pool width
(--unit-size 1 --judges 1 judges each name alone, so a capped run resumes
per name; recorded as the receipt’s unit_size; a value that is not a
positive integer exits 2); see Unit size.
--estimate [--sample K [--force-sample]] [--json] times a sample of slots and
writes no receipt: the sample is at least max(5, ceil(0.25 * slots)) (capped at
the slot count) and starts with the heaviest slots by olean size; a smaller
--sample (or --slots subset) exits 2 unless --force-sample, which warns and
records sample_forced: true; recommended_cap uses the per-slot max model below
half coverage (cap_model); weights_found: false (with a warning) says no slot
had an olean weight; remaining_estimate_seconds covers the unsampled slots only;
the JSON is schema comparator-estimate/2; see
Estimate first.
COMPARATOR_RECEIPT_NO_MATHLIB=1 declares a project that knowingly has no Mathlib
dependency; without it the toolchain mechanism refuses such a project before any
stage, and with it verify-comparator.sh skips lake exe cache get; see
Mechanisms.
Examples
In the package checkout, time a sample of the comparator slots first; no receipt is written.
lean-pkg receipt comparator --estimate
In the package checkout, run the comparator over every configuration and write .lean-receipts/<commit12>-comparator.json (the comparator-receipt program does the same).
lean-pkg receipt comparator
The same for another directory, with up to four judges at once.
lean-pkg receipt comparator --project src/my-proof --judges 4
After the Slurm job finished, seal its sacct record into the receipt so its job can back a compute site.
lean-pkg receipt comparator --seal-sacct .lean-receipts/cb3d68a21454-comparator.json