← Command reference · CLI overview

lean-pkg public-safety

read-only: scan the package’s tree and git history for private patterns (exit 1 on hits; publish –yes runs it).

Usage

lean-pkg public-safety [--history] [--strict] [--package-only] [--gzip-limit BYTES]
                       [--quiet] [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  
--history, --no-history also scan every blob and commit message reachable from any ref (default: on)
--strict warn-only hits (latex-label, warn: lines) fail the scan too (exit 1)
--package-only scan only the package directory even when it is a subdirectory of its repository (default: the whole repository then, which is what promote publishes; the package directory alone is what release --fresh-repo exports)
--gzip-limit BYTES decode gzip files and blobs (content starting 1f 8b) up to this many decoded bytes each and scan the decoded content (K, M, G suffixes; default: $LEAN_PKG_GZIP_LIMIT, else 512M; 0: no decoding, the compressed bytes are scanned as binary)
--quiet only the summary, patterns, warn-only count and verdict lines; no per-hit line (–json is unchanged)

Details

Form What it does Key flags
public-safety NAME read-only: scan what publishing would expose for private strings. The tree is what git would ship (tracked plus untracked, not ignored, files under the package directory); with --history (the default) also every blob, every commit message, every author and committer identity (commit-identity), every annotated tag (tag-name, tag-identity, tag-message) and every branch and tag name (ref-name) reachable from any ref, as lean-pkg’s own make history does (a blob whose bytes are in the working tree is reported once, as a tree hit). When the package directory is a subdirectory of its git repository, the scan covers the whole repository (tree, every blob, every commit; the summary line ends “scanned the repository root: the package is a subdirectory, and promotion publishes the whole repository”), since promotion makes the whole GitHub repository public; --package-only scans the package directory alone (what repo export exports). Path-scoped lines stay package-relative and never apply to a file outside the package. A symbolic link is scanned as its target string. Text with a UTF-8/16/32 byte-order mark, and BOM-less UTF-16, is decoded; a line longer than 20000 characters is scanned whole, in overlapping chunks; a binary file is scanned through its printable runs of 4+ characters (hits without a line number); a file or blob is read up to 64 MB. Gzip content (a file or blob whose bytes start with 1f 8b, whatever its name; tree and history alike) is stream-decoded and the decoded content is scanned in place of the compressed bytes (as a stream too: an incremental decoder never cuts a multi-byte character split between two reads, and a long line is scanned in its overlapping chunks as it arrives, so memory is bounded by the chunk sizes, not by the length of a line), whose printable runs only matched patterns by chance: hits carry encoding: gzip-decoded and the line number of the decoded text (shown as path (decoded):LINE), and the header’s original file name and comment are scanned too (encoding: gzip-header, path (gzip header)). Concatenated members are decoded in turn; zero padding after the last is allowed. A decoded content that is itself binary (a .tar.gz: the tar is not unpacked) is scanned through its printable runs and listed in skipped[] as binary (gzip-decoded), not blocking. Decoding stops at --gzip-limit BYTES decoded bytes per file or blob (K, M, G are powers of 1024; default $LEAN_PKG_GZIP_LIMIT, else 512M; a malformed env value is refused; --gzip-limit 0 turns decoding off and scans the compressed bytes as binary, as before) and when more than 16 MiB are decoded at more than 500 decoded bytes per compressed byte (a decompression bomb). A decode that does not reach the end (gzip corrupt, a bad CRC included, gzip truncated, gzip over the N-byte decode limit, gzip over the 500:1 compression-ratio guard) keeps the hits of the part decoded so far, scans the compressed bytes as before and is listed in skipped[] with that reason: a blocking unscanned hit unless allowed, like any partial scan. Every decoded file or blob is listed in decoded[] {where, path, commit (history, when it had a hit), compressed_bytes, decoded_bytes, content text/binary, complete} and counted on the summary line (“N gzip file(s)/blob(s) decoded”), and printed as a decoded: line. Every file or blob not scanned in full is listed in skipped[] {where, path, reason, commit (history), unscanned_bytes, allowed} and counted on the summary line (“N file(s)/blob(s) not fully scanned: …”); a binary one is listed only, any other unscanned portion (past the cap, unreadable) is also a blocking unscanned hit unless an allow: line applying to the file matches unscanned in full (allow: GLOB: ^unscanned$). Patterns: the package’s .lean-pkg-private-patterns (one regular expression per line, # comments; a bare line or block: REGEX is blocking, warn: REGEX is warn-only, allow: REGEX lines exempt a matched string; each of the three takes an optional path scope, allow: GLOB: REGEX, block: GLOB: REGEX, warn: GLOB: REGEX, applying only to files whose package-relative path matches GLOB (* and ? within a path segment, ** across directories; a GLOB without / matches the file name at any depth; a trailing / matches everything under that directory) and never to commit messages; GLOB is the text before the first colon followed by a space, has no space, colon, backslash or parenthesis, and has at least one of / * ? ., so a plain allow: https://... stays global; the file lists private strings, so tracked or in history it is itself a hit and a WARN); built-ins /home/<user>/, /Users/<user>/, ~/Dropbox/, approvals/, notes/, *.private, TODO-private, and email addresses other than the declared ones (the repository’s commit and tag addresses that are ordinary mail addresses, consent[] entries, allow: lines, example.com/.org/.net, GitHub noreply, git@ SSH remotes; a host-like commit or tag address, one without a dotted domain, user@hostname, or under a local TLD, lan local localdomain localhost home internal intranet corp private test invalid example, is not declared by being used and is an identity-email hit); user and host names derived at scan time from the record’s own local_path, agent, workspace and lease (its agent, workspace and contact; tokens of 4+ characters; never stored; an allow: line is matched against the token’s whole non-space run and exempts an occurrence only when one of its matches covers it, so allowing a public URL that holds the token leaves the bare token a hit elsewhere); internal files by path (approvals/, notes/, drafts/, scratch/, *.priv, *.private); and the warn-only built-in family latex-label, references to a LaTeX manuscript (cross-reference keys lem: thm: cor: prop: def: eq: sec: rem: ex: fig: tab: conj:; the hyphen form only with a digit, a capital or an inner . in the label and never for eq, def, ex; never inside a longer name such as foo_eq_bar or Nat.eq:; built-in allow list def-eq, defeq, eq-of, eq-iff, ex-falso; main.tex; \ref{ \eqref{ \cite{ \label{ \input{ \include{; Overleaf; arXiv:NNNN.NNNNN). Each hit has a severity: warn for latex-label and warn: lines, block for everything else; warn hits print as WARN lines. Each hit: location (path:line, history adds the introducing commit; commit messages are commit-message), a pattern label (a file pattern is labelled .lean-pkg-private-patterns:LINE, never by its text) and an excerpt of 40 characters of context with every match replaced by […]: the raw private string is never printed. The summary line ends with how many hits came from latex-label. The human report is the summary line, the patterns line and, when there are hits, the verdict line (ok: ... or N blocking hit(s): ...) up front, then any scan warnings, the blocking hits, the warn-only hits under a warn-only hit(s): N (families); they do not block line, and the verdict again as the last line, so a long run of WARN lines never hides it; --json is unchanged. With no hit and no blocking line in .lean-pkg-private-patterns (none, or only warn:/allow: lines), a note: no project-specific patterns: built-ins only line comes before the verdict: 0 hits then means none of the generic patterns matched, not that nothing private is there (see Before freezing a public candidate). Exit 0 with no blocking hit (warn hits only), 1 on a blocking hit; --strict makes every hit blocking. --json: ok, hits[] (every hit) {where, path, line, pattern, kind, severity, excerpt, commit (history), encoding (gzip content only)}, tree_hits, history_hits, block_hits, warn_hits, latex_label_hits, strict, history_scanned, scope (package or repository), package_prefix, skipped[], skipped_blocking, decoded[], gzip_limit, builtins_only (true when the patterns file supplies no blocking line), patterns_source {file, file_patterns, file_warn_patterns, allow, allow_scoped, scoped_patterns, tracked, builtin[], warn_only[], latex_label_allow[], derived[], internal_paths[], public_allow_file, public_allow}, warnings[]. A committed .lean-pkg-public-allow at the package root adds allow: lines (allow: REGEX, allow: GLOB: REGEX) that are public on purpose (a fixture address, a generic CI runner path); any other line there is ignored with a warning; inside that file every allow line applies whatever its path scope, and a line a private block pattern matches is the blocking hit public-allow-private, which no allow line exempts (tree and history). An address under .invalid (or another local TLD) is never declared by being used: it needs an allow line. --quiet: only the summary, patterns, note, warn-only count and verdict lines, no per-hit line (exit code and --json unchanged) [--history\|--no-history] [--strict] [--package-only] [--quiet] [--gzip-limit BYTES]

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

Scan the tree and the history publishing would expose for private patterns; exit 1 on a blocking hit.

lean-pkg public-safety my-proof