← Command reference · lean-pkg receipt · CLI overview
lean-pkg receipt slurm
a lower-tier receipt from a finished Slurm job, its verify log and its stdout seal (–template: an sbatch wrapper that meets it; –check: preflight the job’s files).
Usage
lean-pkg receipt slurm [--job J] [--log PATH] [--receipt-commit SHA] [--template]
[--check] [--preflight-deps] [--deps-tar PATH] [--deps-dir DIR]
[--entries GLOB] [--fill-plan DONOR] [--plan-out FILE]
[--base-list FILE] [--stdout PATH] [--stderr PATH]
[--redact REGEX] [--sacct-file F] [--artifacts DIR]
[--artifacts-manifest NAME] [--checker TEXT] [--repo DIR]
[--out PATH] [--compress-log] [--append-readme]
[--readme-heading TEXT] [--readme-line TEXT] [--tar-sha256 HEX]
[common flags]
[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.
Arguments and flags
| Argument or flag | Description |
|---|---|
--job J |
the Slurm job id (job_id becomes slurm-J); required unless –template or –check |
--log PATH |
the job’s raw verify log (required unless –template); when it has no checker: line, –checker TEXT is required |
--receipt-commit SHA |
the verified commit; must exist in –repo; required unless –template or –check (old spelling –commit, kept working) |
--template |
print a minimal sbatch wrapper whose .out/.err/log meet every check below (placeholders for the package’s own commands); needs no other flag |
--check |
preflight the files of a finished (trial) job: every seal, stderr and log-line check, each problem named; no sacct (unless –sacct-file), commit checks only with –commit; writes nothing, exit 0/1 |
--preflight-deps |
before submitting: check that the staged dependency cache (–deps-tar or –deps-dir) holds, at the lake-manifest.json pins committed at –commit (default HEAD), the built .olean and .ilean of every external module in the import closure of the entry files the verifier elaborates (–entries); reads the committed tree, builds and writes nothing, exit 0/1 |
--deps-tar PATH |
with –preflight-deps: the DEPS_TAR tarball the job will restore (gzip, bzip2, xz or plain; read in one pass, never extracted) |
--deps-dir DIR |
with –preflight-deps: a directory holding .lake/packages, instead of –deps-tar |
--entries GLOB |
with –preflight-deps: a glob (relative to the package directory; ** = any directories) of the .lean files the verifier elaborates, repeatable; replaces the default Verify/**/*.lean, Audit/**/*.lean, OwnedAudit/**/*.lean, **/AxiomCheck*.lean, **/TypeCheck*.lean, **/Examples*.lean, **/OwnedAudit*.lean |
--fill-plan DONOR |
with –preflight-deps: plan filling the missing modules from DONOR, another directory holding .lake/packages built from the same pins (docs/receipts.md, “Filling missing dependency artifacts from a pinned donor”, steps 1-4), read-only: every missing module (no 500 cap); refuses (exit 1, each refusal with its own code) unless DONOR/lean-toolchain is the commit’s byte for byte, every manifest package is at its rev, the checkouts have no source edits (git status), each candidate .olean’s first 80 bytes equal the base’s, the donor holds every missing module’s .olean and .ilean, and no addition is a base member, under one, under the package’s own .lake/build or in its root namespaces; lists every file the donor has under each module’s path (all artifact families) with size and sha256. It writes no archive: write it yourself, then rerun –preflight-deps on it |
--plan-out FILE |
with –fill-plan, only when the plan is ok: write FILE (the additions, one path relative to the directory holding .lake per line, for tar -T) and FILE.provenance.json (commit, toolchain, manifest revs, donor identity, file hashes, created_utc: collector provenance, never a job seal); an existing file is never overwritten |
--base-list FILE |
with –fill-plan: a member listing of the base archive (tar -tf output), added to the names no addition may replace |
--stdout PATH |
the job’s stdout (.out): verify-log-sha256 = sha256(raw log), pre-manifest-sha256 = post-manifest-sha256 = sha256(lake-manifest.json at the commit); without it the log must carry its own seal |
--stderr PATH |
the job’s stderr (.err); must be empty |
--redact REGEX |
also replace matches with <redacted> (repeatable); the built-in prefixes are always redacted to <USER> instead (/tmp/<USER>-job, /scratch/<USER>/) |
--sacct-file F |
saved output of sacct -j J --format=JobID,State,ExitCode,Elapsed,TotalCPU -P -n (a host without Slurm) |
--artifacts DIR |
the collected copy of the job’s sealed artifact directory (the template’s ARTIFACTS_DIR): the manifest’s sha256 must be the –stdout artifacts-manifest-sha256 line and every file under DIR is rehashed against it (missing, extra, changed files, symlinks, special files, path traversal and duplicate entries refuse); the receipt gains artifacts_manifest_sha256 and the manifest is written beside it. Needs –stdout |
--artifacts-manifest NAME |
the manifest’s file name inside –artifacts DIR (default artifacts.sha256) |
--checker TEXT |
the exact checker command or mode (default: the log’s checker: line) |
--repo DIR |
the package checkout (default: the current directory) |
--out PATH |
receipt path (default <repo>/.lean-receipts/<commit12>-slurm-<J>.json); the redacted log is written beside it as <commit12>-slurm-<J>-verify.redacted.log |
--compress-log |
write the redacted log as deterministic gzip <…>-verify.redacted.log.gz (level 9, mtime 0, no file name) instead of the plain .log; report_sha256 stays the SHA-256 of the uncompressed log and the receipt gains report_compressed {format: gzip, sha256 of the .gz, bytes = decoded length, not the .gz size}; gate decompresses (bounded) and checks report_sha256. Restore: gzip -dc X.log.gz > X.log. Without it, a log over 90 MiB prints a WARN naming this flag |
--append-readme |
append the entry block to README.md beside the receipt (created if absent; an entry already naming the receipt is not repeated) |
--readme-heading TEXT |
the entry heading after the short commit (default: lower-tier receipt, Slurm job J) |
--readme-line TEXT |
an extra line at the end of the entry block (repeatable) |
--tar-sha256 HEX |
the frozen source tarball’s SHA-256, named in the entry block |
Details
| Form | What it does | Key flags |
|---|---|---|
receipt slurm |
a lower-tier receipt from a finished Slurm job, in exactly the shape gate --receipt validates; reads and writes no registry. Checks, all before anything is written (every failure listed, any one refuses: exit 1, nothing written): the main job line of sacct -j J --format=JobID,State,ExitCode,Elapsed,TotalCPU -P -n (or --sacct-file, that output saved on a host with Slurm; three columns suffice; other columns need sacct’s header line, which locates JobID, State and ExitCode by name, else unexpected sacct format) says COMPLETED and 0:0; with --stdout (the job’s .out) its one verify-log-sha256 line equals the SHA-256 of the raw --log, and its pre-manifest-sha256 and post-manifest-sha256 lines are equal and equal the SHA-256 of lake-manifest.json committed at the commit (lines KEY VALUE or KEY: VALUE); without --stdout, the fallback: the log holds exactly one verify-log-sha256: <hex> line equal to the SHA-256 of the log without that line; --stderr (the .err), when given, is empty; lean_toolchain is lean-toolchain at the commit and mathlib_rev the manifest’s mathlib rev there (else the log’s mathlib-rev:), a disagreeing log line refuses; sorry_count is the log’s sorry-count: line (never fewer than the log’s declaration uses 'sorry' lines, else refused), else its declaration uses 'sorry' lines, counted only when the log shows the build finished (Build completed successfully or lake build: ok; neither a count nor a completion line refuses), and must be 0; axioms the log’s axioms: line, else the union of its #print axioms output (neither refuses); checker is --checker, else the log’s checker: line; optional commit:, job-id:, generated-at: lines must agree; a log with no commit: line is refused in the fallback mode (no --stdout), and with --stdout prints the stderr WARN the verify log has no commit: line; it is bound to the commit only through lake-manifest.json (JSON log_commit_bound: false; true with a matching line; the written receipt carries the same log_commit_bound, an additive key gate never reads, and when it is false the README entry gets a - WARN: line saying so); every field but checker is read from the RAW log, and a redaction that removes or alters a line the parser reads (Lean’s sorry warnings, #print axioms output, a build-completion line, any key: line but checker:) refuses; after redacting the /tmp/<account>-job prefix, /scratch/<user>/ and every --redact match, the public-safety scanner finds no blocking hit in the redacted log, the receipt JSON or the README entry (families listed, never the strings; besides the shared families it blocks this machine’s user name and host name, full and short, at a word boundary, and a /home/<x> or /Users/<x> home directory with or without a trailing slash); a committed symlink at the commit that resolves into .lean-receipts/ refuses (gate refuses it too); with --append-readme, a README.md that is not UTF-8 text, or a symlink, refuses before anything is written, and so does a symlinked .lean-receipts/. job_id is slurm-<J> (--job takes J or slurm-J). Writes <c12>-slurm-<J>-verify.redacted.log and <c12>-slurm-<J>.json (default <repo>/.lean-receipts/; report_sha256 is the redacted log’s SHA-256; a differing file already there is refused, except that a re-run differing only in a clock-stamped generated_at (no generated-at: line in the log) keeps the stored one), with --stdout the receipt also carries job_stdout_sha256 and manifest_sha256 (additive keys gate ignores), prints the README entry (state, exit, elapsed, TotalCPU, log name and hashes; with --stdout a - Seal: line with the job stdout and manifest SHA-256) and next: lean-pkg gate NAME --check --receipt PATH; --append-readme appends the entry to README.md beside the receipt (once; --readme-heading, --readme-line, --tar-sha256 fill it; the entry’s heading starts with the commit, so a --readme-heading that repeats this commit’s SHA has it dropped). --compress-log writes the log as deterministic gzip <c12>-slurm-<J>-verify.redacted.log.gz instead (level 9, mtime 0, no file name): report_sha256 stays the uncompressed log’s SHA-256, the receipt gains the additive report_compressed {format: gzip, sha256 of the .gz, bytes uncompressed}, sealed[] lists the .gz (role redacted-log.gz, receipt_key report_compressed.sha256, uncompressed_sha256), restore with gzip -dc X.log.gz > X.log (details); without it a redacted log over 90 MiB prints a stderr WARN naming the flag. --json {ok, receipt, log, report_sha256, raw_log_sha256, job_id, seal, log_commit_bound, report_compressed, sealed[], sacct, redactions, lines_redacted, checks[], readme_block, readme_appended, next, refusals[]}; sealed[] {role, path, sha256, receipt_key} names every file the run wrote and bound (receipt, redacted-log with report_sha256, and for receipt systemd the normalised unit.properties with unit_properties_sha256), empty on a refusal: take a sidecar from it, never by its file name (properties in receipt systemd’s JSON is the raw, unsealed capture); usage errors (a missing --log/--stdout/--stderr file, a bad --redact regex) exit 2. --template (no other flag, no registry) prints a minimal sbatch wrapper whose .out, empty .err and log carry every line the receipt reads (the three seal lines; checker:, sorry-count:, axioms:, lean-toolchain:, commit:, job-id:, generated-at:), with placeholders for the package’s own commands, a node-local work directory and LEAN_NUM_THREADS 3, and an exact-runtime preflight before any tool runs: the C locale (LC_ALL=C LANG=C PYTHONUTF8=1, an #SBATCH --export line and an export; stderr stays strict) and a type -P probe of every executable it needs, which fails the job before the work (details). --check preflights a job’s files (a short trial job before the long one): the seal, stderr, log-line, field and public-safety checks, every problem named, sacct not run (checked only from --sacct-file with --job), commit-side checks only with --commit; writes nothing; exit 0/1; --json {ok, check, written: [], raw_log_sha256, log_commit_bound, checks[], problems[]} (log_commit_bound as in a producing run, null without --commit). --artifacts DIR (needs --stdout; also with --check) checks the job’s artifact seal (the template’s optional ARTIFACTS_DIR): the SHA-256 of the manifest DIR/artifacts.sha256 (--artifacts-manifest NAME for another name) must equal the stdout’s one artifacts-manifest-sha256 line, and every file under DIR is rehashed in 1 MiB chunks against it; a missing, extra or changed file, a symlink, a special file, a path-traversal, duplicate or unsorted entry refuses; the receipt gains the additive artifacts_manifest_sha256 (gate ignores it), the manifest is written beside it as <c12>-slurm-<J>-artifacts.sha256 (sealed[] role artifacts.sha256), --json gains artifacts {ok, dir, files, bytes, manifest, manifest_sha256}; without --artifacts nothing changes (Recollecting a finished job). --preflight-deps --deps-tar T (or --deps-dir D, a directory holding .lake/packages) [--commit SHA] [--entries GLOB]... checks, before submitting, that the staged dependency cache holds what the verifier’s own entry files need: the import closure of the entry files committed at --commit (default HEAD; default entries Verify/**/*.lean, Audit/**/*.lean, OwnedAudit/**/*.lean, **/AxiomCheck*.lean, **/TypeCheck*.lean, **/Examples*.lean, **/OwnedAudit*.lean; --entries replaces them) is followed through the package’s committed modules and the dependencies’ sources in the cache, and every external module in it needs its .olean and .ilean as regular files in exactly one manifest package (import Mathlib needs every module Mathlib.lean imports, transitively); every git package of lake-manifest.json must be in the cache at the manifest’s rev (.git/HEAD, resolved through refs/ or packed-refs); a missing module, a module no package provides (toolchain roots Init, Std, Lean, Lake aside), a module whose source is not in the cache, a missing package, a stripped or other-rev checkout, a path package, no entry file, or an unreadable tarball (gzip, bzip2, xz, plain) is a problem; reads only (the tarball in one pass, never extracted), builds and writes nothing; exit 0/1; --json {ok, preflight_deps, commit, entries[], required_external_modules, missing_count, missing[] {module, package, files, required_by} (first 500), checks[], problems[]}. It adds a check before submission; every check inside the job is unchanged. Details: Receipts and trust |
--job J --log PATH --commit SHA [--stdout PATH] [--stderr PATH] [--checker TEXT] [--repo DIR] [--redact REGEX]... [--sacct-file F] [--artifacts DIR [--artifacts-manifest NAME]] [--out PATH] [--compress-log] [--append-readme [--readme-heading T] [--readme-line T]... [--tar-sha256 HEX]] [--json]; --template; --check --log PATH [--stdout PATH] [--stderr PATH] [--commit SHA] [--job J --sacct-file F] [--artifacts DIR] |
Exit codes
Exit 1 is also a negative answer here:
receipt slurm --check: a problem with the job’s files
Examples
Print a minimal sbatch wrapper whose files pass every check; save it as verify.sbatch and edit its commands.
lean-pkg receipt slurm --template
Preflight the files of a finished job before writing anything; exit 1 names each problem.
lean-pkg receipt slurm --check --commit "$(git rev-parse HEAD)" --log verify-123.log \
--stdout verify-123.out --stderr verify-123.err
Write the lower-tier receipt under .lean-receipts/ in the checkout and add its entry block to the README there.
lean-pkg receipt slurm --job 123 --commit "$(git rev-parse HEAD)" --log verify-123.log \
--stdout verify-123.out --stderr verify-123.err --append-readme