← Command reference · CLI overview

lean-pkg gate

validate a lower-tier receipt; gate-pending -> verified-private; records the receipt’s lean_toolchain and mathlib_rev as the package’s pins.

Usage

lean-pkg gate --receipt RECEIPT [--comparator PATH] [--refuse-private] [--refuse-dirty]
              [--refresh-formalization] [--agent AGENT] [--check] [--regate]
              [--reason TEXT] [--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  
--receipt RECEIPT path to receipt JSON. Required.
--comparator PATH optional comparator receipt JSON; required later by promote
--refuse-private refuse (exit 1, nothing copied) when a receipt holds private strings; default is a WARN line and the receipt is kept
--refuse-dirty refuse when tracked files are modified in the checkout; default is a WARN line (receipts are always checked against the bound commit)
--refresh-formalization after the gate, regenerate the package’s formalization.yaml (derived keys, including status.evidence; kept keys survive) and set its registry pointer; refuses when nothing would change
--agent AGENT the agent acting (recorded as the event’s actor); another agent’s live lease then refuses; with –refresh-formalization: the live lease holder (the file write needs it)
--check validate only, against HEAD (with –comparator: both tiers); write nothing, record nothing (works at any status), like comparator --check
--regate re-gate a verified-private (or public) package on a new receipt in one step: event regated {previous_commit, commit, job_id, reason}, status unchanged; the receipt’s commit must descend from the gated commit unless –reason is given
--reason TEXT with –regate: accept a receipt commit that does not descend from the gated commit (recorded with non_descendant: true)
--repo DIR with –check only: validate against the checkout DIR instead of the registered local_path, for this call (never saved; JSON repo_override). DIR must be a git work tree, and when it has remotes one must be the package’s repo. A writing gate refuses it: it binds the registered checkout (move that with update --path)

Details

Form What it does Key flags
gate NAME validate a lower-tier receipt; gate-pending → verified-private; --receipt/--comparator PATH is used as given when it exists (relative to the cwd, or absolute); a relative path missing from the cwd but present under the package checkout (or --check --repo DIR) is resolved there, announced on stderr, as a · receipt R resolved against the package checkout: P line and in JSON resolved_paths[] {what, arg, path, base} (the same relative path, never another matching receipt; comparator NAME too), else refused naming the caller’s cwd, the checkout, both paths tried and the fix; --check takes no lease, so --check --agent is a usage error (exit 2) that names the writing form; HEAD must be the receipt’s commit or an evidence-only descendant of it, or, when the package opted in (docs_descendants: true), a docs-only descendant: no build input under the package directory changed (the rule); the gated commit stays the receipt’s, the text output says ✓ HEAD <c12> is a docs-only descendant of <c12> (N non-build file(s): ...; opted in), and the gate-passed/regated event and --json (also gate --check, and comparator attach/--check) carry descendant_of and docs_paths (up to 50); a refusal under the opt-in names the changed build input(s); without it, a refusal that the docs rule would have admitted adds the hint update NAME --accept-docs-descendants; identical re-gate is a no-op; a gate or re-gate records the receipt’s lean_toolchain and mathlib_rev (first 10 characters) into the package’s lean_toolchain and mathlib_pin only when each agrees with the file committed at the receipt’s commit (lean-toolchain; the mathlib rev in lake-manifest.json, prefix-equal); a receipt whose lean_toolchain differs from lean-toolchain, or whose mathlib_rev is not prefix-equal to the mathlib rev in lake-manifest.json, committed at its commit is refused (mathlib mismatch: ...; --check prints ✓ mathlib_rev R = the mathlib rev in lake-manifest.json committed at <c12>); a package without Mathlib (a readable manifest that lists no mathlib package) has the explicit mathlib_rev none, which is checked (✓ mathlib_rev none: lake-manifest.json committed at <c12> has no mathlib package; none beside a manifest that pins Mathlib is refused) and leaves mathlib_pin null (a recorded pin is cleared); when the manifest is not readable the rev is not checked (· mathlib_rev not checked: ...), the recorded pin is kept, the gate still passes, it prints NAME: pins kept: receipt mathlib_rev X does not match lake-manifest.json at <c12> (unreadable) and JSON carries pins_kept {field: {receipt, manifest}}; a recorded pin that is a prefix of the receipt’s rev, or the reverse, is unchanged; it prints NAME: pins updated from the receipt: lean_toolchain A -> B, mathlib_pin C -> D when either changes, and adds pins {field: {from, to}} to the gate-passed/regated event (JSON pins, {} when unchanged); --check adds · pins: gate would record ... / · pins kept: ... and JSON pins, pins_kept, writing nothing; --check also prints WARN: palomar: not submittable at <c12>: N gap(s) need a new commit (codes); see lean-pkg palomar check NAME --rev <c12> on stderr when palomar check finds error gaps at the receipt’s commit (JSON palomar_check {ready, commit, errors, warns, codes, command}; null without a readable checkout), never a refusal; gate and --check print WARN: toolchain advisory ID: TOOLCHAIN has a known Lean soundness bug, fixed in vX.Y.Z; LINK ... on stderr for each entry of lean-pkg’s toolchain advisories list that names the receipt’s lean_toolchain (JSON toolchain_advisories[] {id, toolchain, summary, fixed_in, links, date_added}, [] when none; toolchain advisories), never a refusal; on a verified-private package plain gate is refused and the message names --regate; when the package tracks its claims file (claims_file, default claims.yaml) at the receipt’s commit, that committed file (never the working tree) must pass the claims/1 schema check claims sync applies, and every claim’s declaration must occur in its file as tracked at that same commit (claims sync’s declaration check), else gate refuses (exit 1, nothing copied or recorded; the message names claims check --file for schema errors or claims sync for missing declarations, and says the fix is a new commit, so a new receipt and a re-gate); the tree at the receipt’s commit must not let the build read sources outside the package directory, which the receipt does not bind (see Path dependencies): a committed symlink whose target is absolute or has a .. component is refused, and so is one that resolves into .lean-receipts/ or to the recorded formalization_yaml (chains and directory symlinks followed; evidence there may change later, so the build would read unbound bytes), and so is a path package in lake-manifest.json committed there whose dir leaves the package directory (absolute, or .. after normalising), or which is, or passes through, a symlink, a submodule (gitlink) or a directory not tracked at that commit (such as .lake/), or which contains a gitlink; each refusal names the entry (a tracked directory inside the package is accepted; a manifest that is not valid JSON is refused; --check prints ✓ lake-manifest.json at <commit12>: no path dependency outside the package directory and ✓ no symlink at <commit12> leaves the package directory or points into .lean-receipts/); report_sha256 must equal the SHA-256 of the redacted verify log <c12>-<job slug>-verify.redacted.log wherever a copy is found (beside the --receipt file, in the package’s .lean-receipts/, tracked there at HEAD), else refused (report_sha256 mismatch: ...); a NAME.gz copy (receipt --compress-log) is stream-decompressed and its uncompressed bytes must hash to report_sha256 (never the .gz hash), the .gz to report_compressed.sha256 and the length equal report_compressed.bytes when recorded, output past that length refused (gzip-bomb guard; 4 GiB without report_compressed); ✓ report_sha256 = sha256 of NAME (where) (where, decompressed from .gz for a .gz) in the text output; none found, or a copy that cannot be read, is refused (report log missing: NAME ..., naming where it looked and the path to restore it to; Restoring preserved evidence), JSON report_log {checked, log, where[], copy[]}; the sealed log found beside --receipt is copied into .lean-receipts/ beside the canonical receipt when no copy is there (copy[]; --check prints · gate would also copy ...), so the stored receipt verifies on its own; every check on both copies (the receipt and, with --comparator, the comparator receipt) runs before either is written, so a refusal writes nothing to .lean-receipts/, and gate/comparator refuse to write when .lean-receipts or the destination file is a symlink; success prints ✓ claims.yaml at <commit12>: schema ok (N claims), declarations found or a neutral · no claims.yaml tracked at <commit12>, and JSON gains claims_schema {checked, commit, file, ok, claims, errors[], declarations {checked, ok, problems[]}} (ok null when checked is false); receipt bytes (keys and values) are scanned for private local paths before the copy into .lean-receipts/ (stderr WARN: receipt field F contains a private local path (kept: ...; --refuse-private refuses such a receipt), worded for what happened to the receipt: kept when it was accepted, nothing copied (--check) under --check, nothing copied: refused for another reason, below only when the gate refused; private_strings in JSON); lean-toolchain is read at the receipt’s commit; modified tracked files print a WARN (dirty in JSON); a checkout off its default branch or detached prints WARN: evaluating branch X, not the default D on stderr, never a refusal; after recording, each evidence file git ignores prints a stderr WARN: PATH is git-ignored (RULE): ... with the remedy (ignored_evidence[] {path, rule} in JSON; see promote) --receipt PATH [--comparator PATH] [--refuse-private] (refuse, exit 1, nothing copied) [--refuse-dirty] [--refresh-formalization [--agent A]] (then regenerate formalization.yaml, derived keys including status.evidence, and set its pointer in one step; another agent’s live lease and a kept key failing the schema refuse before the gate; an identical re-gate whose file is already current is refused with nothing written; --json gains "formalization": {path, written, unchanged, registry_updated, validation, placeholders}) [--regate [--reason TEXT]] (re-gate a verified-private package, or a public one, on a new receipt in one step instead of update --status gate-pending then gate: the same validations as gate (binding, toolchain, sorry, axioms, the claims file at the receipt’s commit, the comparator binding when --comparator is given), status unchanged, one regated event {previous_commit, commit, job_id, checker, receipt, reason, non_descendant?}, so one registry commit and push in committed mode; the receipt’s commit must descend from the commit of the recorded gate receipt (git merge-base --is-ancestor), else refused with nothing copied unless --reason is given, which records non_descendant: true; refused on any other status, or with no recorded gate receipt; --reason without --regate is a usage error, exit 2; prints NAME: <status>, re-gated <prev12> -> <commit12>; JSON event: regated, previous_commit, non_descendant, reason; with --check the same checks write nothing and add a ✓ regate:/✗ regate: line and JSON regate {previous_commit, non_descendant}) [--check] (read-only: every validation gate makes, against HEAD, with --comparator both tiers; prints ✓ lines for binding, the formalization.yaml derived-only rule, toolchain at the bound commit, sorry count and axioms, and the claims file at the receipt’s commit (✓ … schema ok (N claims), ✗ claims.yaml at <commit12>: <first error> with exit 1, or · when none is tracked), or the refusal gate would print; writes nothing, records no event, works at any status, exit 0/1; JSON event: gate-checked, recorded: false, checks[], head, comparator, claims_schema; ok: false on a failing claims file) [--check --repo DIR] (validate against the checkout DIR instead of the registered local_path, for this one call: never written to the registry; a stderr note using --repo DIR instead of the registered local_path ...; JSON repo_override {path, registered_path, remote_match}, null without --repo; DIR must be a git work tree, and when it has remotes and the record names a repository one remote must be it (remote_match: true), otherwise the caller vouches for it; a writing gate refuses --repo (exit 2): a gate binds the registered checkout, which update --path moves). A successful gate (and publish --yes) ends with a results-ledger: line naming lean-pkg status NAME and lean-pkg claims ledger NAME (JSON rl_reminder: true, rl_hint): lean-pkg keeps no results ledger; see Results ledger

Exit codes

0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.

Exit 1 is also a negative answer here:

JSON output

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

Examples

Validate the receipt against HEAD and record nothing; exit 1 when gate would refuse it.

lean-pkg gate my-proof --receipt .lean-receipts/receipt.json --check

Accept the lower-tier receipt and move the package from gate-pending to verified-private.

lean-pkg gate my-proof --receipt .lean-receipts/receipt.json

Re-gate an already verified package on a newer receipt; the status does not change.

lean-pkg gate my-proof --receipt .lean-receipts/receipt.json --regate