← Command reference · lean-pkg palomar · CLI overview

lean-pkg palomar check

read-only, offline: every gap to Palomar’s mechanical rules at one commit (module headers, toolchain floor, comparator configs, formalization.yaml, licence, repository); exit 0 ready / 1 gaps.

Usage

lean-pkg palomar check [--rev REV] [--config PATH] [--rules FILE] [--repo DIR]
                       [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag Description
NAME  
--rev REV the commit to judge (default: the gate-bound commit, else HEAD)
--config PATH judge only this comparator configuration (Palomar verifies the one a submission names); default: every configuration tracked at the commit
--rules FILE a newer PalomarSubmission browser-preflight-policy.json (schema 1) downloaded by hand; default: the rules pinned at PalomarSubmission d4e41c1d5b0d (read 2026-10-16)
--repo DIR judge the checkout DIR instead of the registered local_path (never saved)

Details

Form What it does Key flags
palomar check NAME read-only and offline (no network, nothing written, no event): every gap between the package at one commit (--rev REV, else the gate-bound commit, else HEAD; git objects, never the working tree) and Palomar’s mechanical rules, pinned at PalomarSubmission d4e41c1d5b0d (read 2026-10-16; --rules FILE takes a newer browser-preflight-policy.json): a module header in every tracked .lean file of the repository (exact list of the files without one), at most 10,000 lines, no symlinks; the toolchain floor v4.35.0-rc2; a Lake configuration, no submodules; each comparator configuration (--config PATH: only that one) with the required keys, no other keys (judged_as, lean_pkg_scaffold are refused), standard axioms, tracked module sources, a Challenge within 1,000 lines and 100 KiB; the headline configuration, when declared: the same checks, plus comparator.headline_uncovered (error) or comparator.headline_unjudged (warn) from the subset rule (JSON headline {config, source, judged, covered} or null); formalization.yaml tracked, v0.4-valid, no placeholders, Palomar’s metadata minimum; one root licence file matching license_spdx; a GitHub repository, public, the commit pushed (these two warn). Each gap {code, severity error\|warn, paths, detail, fix}; verdict first and last; a lean-toolchain on lean-pkg’s toolchain advisories list adds one WARN: toolchain advisory ... line per entry after the verdict, never a gap (JSON toolchain_advisories[]; toolchain advisories); --repo DIR judges another checkout; exit 0 no error gap, 1 error gaps, 2 usage (rules, source and date) [--rev REV] [--config PATH] [--rules FILE] [--repo DIR]

JSON output

Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):